contributions.tex

\paragraph{Contributions}
In this paper, we make the following technical contributions.
%
\begin{compactenum}
\item We present a novel program analysis technique that 
lifts the CDCL algorithm to relational numerical abstract domains.   
We have implemented our technique in the 2LS verification tool.  

\item We present an abstract model search algorithm 
%that strictly 
%generalises the Boolean Constraint Propagation (BCP) procedure 
that computes a fixed-point over a relational domain.  We propose 
domain-specific decision heuristics that exploit the expressivity 
of the underlying abstract domain to make effective decisions. 

\item We sketch a lifting of the conflict analysis procedure 
to relational abstract domains in order to learn a generalised reason 
for conflicts.  
 
\item  Experiments indicate a two order of magnitude reduction 
in the number of decisions, propagations, and conflicts compared 
to a SAT solver while being more precise than an abstract interpreter.  
\Omit {
set of benchmarks drawn from the bitvector regression category in 
SV-COMP, bit-precise software models auto-generated from hardware 
circuits domain and some hand crafted example show that 
}
\end{compactenum}