paper.tex

\documentclass[a4paper]{llncs}

\usepackage{import}
\usepackage{times}
\usepackage{microtype}
\usepackage{array}
\usepackage{graphicx,wrapfig}
\usepackage{cite}
\usepackage{tikz}
\usetikzlibrary{plotmarks}
\usepackage{pgfplotstable}
\usepackage{filecontents}
\usepackage{pgfplots}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{stmaryrd}
%\usepackage{mathptm}
\usepackage{color}
\usepackage{listings}
\usepackage{verbatim}
\usepackage{comment}
\usepackage{alltt}
\usepackage{psfrag}
\usepackage{epsfig}
\usepackage{wasysym} 
%\usepackage{subfigure}
\usepackage{paralist}
\usepackage{dingbat}
\usepackage[algo2e,linesnumbered,ruled,lined]{algorithm2e}
\usepackage{hyperref}
\usepackage[subnum]{cases}
\makeatother

\newcommand{\extendedonly}[1]{}
\newcommand{\paperonly}[1]{#1}

\newcommand{\tool}[1]{\textsc{#1}\xspace}
\newcommand{\cbmcv}{\tool{cbmc 5.0}}
\newcommand{\Omit}[1]{}
\newcommand{\mydef}[1]{\begin{definition}#1\end{definition}}
\newcommand{\rmcmt}[1]{{\color{magenta}{#1}}}%#1
\newcommand{\pscmt}[1]{{\color{blue}{#1}}}%#1
\newcommand{\dkcmt}[1]{{\color{red!70!black}{#1}}}%#1

\input{symbols}

\begin{document}

\title{Model Search in Relational Domains}

\author{Rajdeep Mukherjee\inst{1} \and Peter Schrammel\inst{2} \and
Daniel Kroening\inst{1} \and Tom Melham\inst{1}}

\institute{University of Oxford, UK \and University of Sussex, UK \\
%\email{\{rajdeep.mukherjee,kroening,tom.melham\}@cs.ox.ac.uk},
%\email{p.schrammel@sussex.ac.uk}
}

\maketitle

%===============================================================================
\begin{abstract}
%===============================================================================
%
\emph{Abstract Conflict-Driven Clause Learning} (ACDCL) is a generalisation
of the well-known CDCL algorithm used in SAT solvers.
%
\Omit {  ACDCL alternates between a model search, which
performs over-approximate deduction with constraint propagation, and a
conflict analysis, which performs under-approximate abduction with heuristic
choice.
}
%
It has been successfully used with non-relational abstract domains, such
as intervals, to improve the performance of a floating-point decision
procedure.  Whereas the propositional reasoning of SAT 
solvers can be lifted easily from the Boolean lattice to other 
non-relational domains, application to relational domains is 
challenging because of the relational properties of deductions.
%
In this paper, we present non-trivial liftings of the model search and
conflict analysis algorithms of SAT solvers to relational abstract domains.  We have
implemented these algorithms inside the 2LS verification tool and
instantiated our analyser with a template polyhedra domain to check safety
properties of C programs.  We~evaluate the performance of our analyser 
compared to a program verifier that uses propositional solvers and
an abstract interpretation tool.
%static analyser based on abstract interpretation.
%
\Omit {
on a set of benchmarks drawn from bit-vector regression 
in SV-COMP'16, bit-precise software models of hardware 
circuits auto-generated from v2c tool, and several 
bounds checking benchmarks 
}
We observe a reduction of two orders of magnitude in the number of 
decisions, propagations, and conflicts compared to a SAT 
solver and higher precision compared to an abstract interpreter. 
\Omit{
along with stronger deductions and learnt clauses aided by the richer
abstract domains.
}
%
\end{abstract}

%===============================================================================
\input{introduction}
%===============================================================================

%===============================================================================
\input{contributions}
%===============================================================================

%===============================================================================
\input{example}
%===============================================================================

%===============================================================================
\input{domains}
%===============================================================================

%===============================================================================
\input{algorithm}
%===============================================================================

%===============================================================================
\input{deductions}
%===============================================================================

%===============================================================================
\input{decision}
%===============================================================================

%===============================================================================
\input{learning}
%===============================================================================

%===============================================================================
\input{experiments}
%===============================================================================

%===============================================================================
\input{background}
%===============================================================================

%===============================================================================
\input{conclusion}
%===============================================================================
\newpage
\bibliographystyle{splncs03}
\bibliography{biblio.bib}

\extendedonly{
\input{appendix}
}

\end{document}