Abstract Conflict Driven Clause Learning for Safety

The success of Conflict Driven Clause Learning (CDCL) for Boolean satisfiability has inspired its adoption in other domains. We present a novel lifting of the CDCL to program analysis called Abstract Conflict Driven Learning for Safety ACDLS. ACDLS alternates between model search, which performs over-approximate deduction with constraint propagation, and conflict analysis, which performs under-approximate abduction with heuristic choice. We instantiate the model search and conflict analysis algorithms to an abstract domain of template polyhedra, strictly generalizing CDCL from the Boolean lattice to richer lattice structures. Our domain of template polyhedra can express intervals, octagons, and certain restricted polyhedral constraints over program variables. We have implemented ACDLS for automatic bounded safety verification of C programs.

ACDLS is integrated into 2LS verification framework. 2LS provides implementation of various template polyhedra domains such as Intervals, Octagons, Zones, Template Polyhedra and Equality.

Contact Rajdeep Mukherjee or Peter Schrammel or send an email here with questions about ACDLS or feedback.

Installation

Download the latest tarball of ACDLS. Extract its content and type ./install for installing the tool. The tarball also contains several benchmark files in C that can be used for property verification.

Installation Steps
======================
Step 1: cd tool
Step 2: type "./install"
Step 3: A directory named "2LS" is created inside tool/
Step 4: cd tool/2ls/src/2ls/
Step 4: run "./2ls --help" to check that the executable is created

The following command is used to run ACDLS.

2ls --acdl {FILENAME} --decision {D} --propagate {P} --learning {L} --{domain} --inline

Decision heuristics {D} = ordered, longest-range, berkmin, random
Propagation heuristics {P} = forward, chaotic
Learning heuristi {L} = first-uip
Domain {domain} = intervals, octagons, equalities

Program Analysis using Abstract DPLL

Program Analysis using Abstract CDCL

Trace Partitioning in ACDLS

Tutorial on ACDLS

A brief tutorial on Abstract Conflict Driven Clause Learning for Safety is available here.

---