conclusion.tex

\section{Conclusions}
In this paper, we present a procedure for lifting the model search 
and conflict analysis procedures in satisfiability solvers for 
relational abstract domains.  
%We explain specific properties of abstract domain elements that are necessary to infer domain-specific deductions.  
We present a parameterised abstract transformer that allows us to
%flexibly implement various propagation heuristics while taking care of
flexibly guide the deductions in the abstract domain while performing lazy 
closure operations in the relational domains for efficiency reasons.
%
Our decision heuristics take into account the high-level structure of
programs and the underlying expressivity of the abstract domains.  Our
conflict analysis procedure learns abstract transformers following a
UIP computation over relational domain elements.  We instantiate our
algorithms as a program analyser to determine safety of C programs.
%
Experimental evaluation shows that ACDCL is able to suitably exploit the
expressivity of richer abstract domains as well as the precision of the 
CDCL architecture.

\Omit{
Generalisations of conflict reasons for relational domains 
and non-relational domain such as trace-based abstract domains is a 
possible direction of future work.  We believe that domain refinement 
in ACDCL will also help to dynamically adjust the precision of the 
deduction in an effective manner. 

Experimental evaluation on different benchmark sets shows that
ACDCL is able to suitably exploit the expressivity of richer
abstract domains as well as precision of CDCL architecture.
This is attributed to the intelligent decision heuristics
which exploits the high-level structure of the problem
combined with stronger deductions and clause learning
mechanism aided by the richer abstract domains.
Future work -- domain refinement, incremental solving, 
invariant inference, intelligent $\gamma$-completeness check. 
Implement dedicated abstract domains to exploit full performance.
generalization for relational domain, instantiate acdl with trace-based domains.
}