Interpolant Tree Automata and their Application in Horn Clause Verification
Extracted source text ยท arXiv 1601.06521
%\documentclass[11pt]{article}
\documentclass[submission,copyright]{eptcs}
\usepackage{graphicx}
\usepackage{amsmath}
%\usepackage{algorithm2e}
\usepackage{algorithmicx}
\usepackage{algpseudocode}
\usepackage{alltt}
\usepackage{tikz}
\usepackage{adjustbox}
\pagenumbering{arabic}
\usepackage{hyperref}
\usepackage{fancyvrb}
\usepackage{alltt}
\usepackage{csvsimple}
%\usepackage[draft]{commenting}
%\declareauthor{jg}{John}{blue}
%\declareauthor{pg}{Pierre}{orange!50}
%\declareauthor{bk}{Bish}{red}
\title{Interpolant Tree Automata and their Application in Horn Clause Verification \thanks{The research leading to these results
has been supported by the EU
FP7 project 318337, \emph{ENTRA - Whole-Systems Energy Transparency} and the EU FP7 project 611004, coordination and support action ICT-Energy.}}
\author{Bishoksan Kafle \institute{Roskilde University, Denmark} \email{kafle@ruc.dk}
\and
John P. Gallagher \institute{Roskilde University, Denmark}
\institute{IMDEA Software Institute, Spain}
\email{jpg@ruc.dk}
}
\def\titlerunning{Interpolant Tree Automata and their Application in Horn Clause Verification}
\def\authorrunning{Kafle \& Gallagher}
\begin{document}
\maketitle
\begin{abstract}
This paper investigates the combination of abstract interpretation over the domain of convex polyhedra with interpolant tree automata, in an abstraction-refinement scheme for Horn clause verification. These techniques have been previously applied separately, but are combined in a new way in this paper. The role of an interpolant tree automaton is to provide a generalisation of a spurious counterexample during refinement, capturing a possibly infinite set of spurious counterexample traces. In our approach these traces are then eliminated using a transformation of the Horn clauses. We compare this approach with two other methods; one of them uses interpolant tree automata in an algorithm for trace abstraction and refinement, while the other uses abstract interpretation over the domain of convex polyhedra without the generalisation step. Evaluation of the results of experiments on a number of Horn clause verification problems indicates that the combination of interpolant tree automaton with abstract interpretation gives some increase in the power of the verification tool, while sometimes incurring a performance overhead.
%In this paper, we study the role of \emph{interpolant tree automata} in Horn clause verification. In an \emph{abstraction-refinement} scheme for Horn clause verification, an interpolant tree automaton serves as a generalisation of a spurious counterexample during refinement. We apply them to verify Horn clauses with respect to some integrity constraints and present some experimental results on some software verification benchmarks. The results show some improvements over the previous approaches.
\noindent
{\bf Keywords:} Interpolant tree automata, Horn clauses, abstraction-refinement, trace abstraction.
%
%\textbf{TODO}
%fix solved/unsolved, also same term is used when a problem cannot be solved because of the timeout
\end{abstract}
\input{localdefs}
\input{introduction}
\input{prelim}
\input{interpolant_automata}
\input{application}
\input{abstract_automata}
\input{experiments}
\input{related}
\input{conclusion}
\bibliographystyle{eptcs}
\bibliography{refs}
\end{document}
\pagestyle{plain}
\pagestyle{myheadings}
\newcommand{\rahft}{{\sf \textsc{Rahft}}}
\newcommand{\rahit}{{\sf \textsc{Rahit}}}
\newcommand{\integ}{{\sf int}}
\newcommand{\listint}{{\sf listint}}
\newcommand{\other}{{\sf other}}
\newcommand{\true}{\mathsf {true}}
\newcommand{\false}{\mathsf {false}}
\newcommand{\Bin}{{\sf Bin}}
\newcommand{\Dep}{{\sf Dep}}
\newcommand{\g}{{\sf g}}
\newcommand{\nong}{{\sf ng}}
\newcommand{\OL}{{\cal O}}
%\newcommand{\mgu}{{\sf mgu}}
\newcommand{\M}{{\sf M}}
\newcommand{\R}{{\cal R}}
\newcommand{\A}{\mathcal{A}}
\newcommand{\body}{\mathcal{B}}
\newcommand{\B}{{\cal B}}
\newcommand{\C}{{\cal C}}
\newcommand{\D}{{\cal D}}
\newcommand{\X}{{\cal X}}
\newcommand{\V}{{\cal V}}
\newcommand{\Q}{{\cal Q}}
\newcommand{\F}{{\sf F}}
\newcommand{\N}{{\cal N}}
\newcommand{\Lang}{{\cal L}}
\newcommand{\powerset}{{\cal P}}
\newcommand{\FTA}{{\cal FT\!A}}
\newcommand{\Term}{{\sf Term}}
\newcommand{\Empty}{{\sf empty}}
\newcommand{\nonEmpty}{{\sf nonempty}}
\newcommand{\compl}{{\sf complement}}
\newcommand{\args}{{\sf args}}
\newcommand{\preds}{{\sf preds}}
\newcommand{\gnd}{{\sf gnd}}
\newcommand{\lfp}{{\sf lfp}}
\newcommand{\psharp}{P^{\sharp}}
\newcommand{\minimize}{{\sf minimize}}
\newcommand{\headterms}{\mathsf{headterms}}
\newcommand{\solvebody}{\mathsf{solvebody}}
\newcommand{\solve}{\mathsf{solve}}
\newcommand{\fail}{\mathsf{fail}}
\newcommand{\member}{\mathsf{memb}}
\newcommand{\ground}{\mathsf{ground}}
\newcommand{\raf}{{\sf raf}}
\newcommand{\qa}{{\sf qa}}
\newcommand{\spl}{{\sf split}}
\newcommand{\transitions}{\mathsf{transitions}}
\newcommand{\nonempty}{\mathsf{nonempty}}
\newcommand{\dom}{\mathsf{dom}}
\newcommand{\Args}{\mathsf{Args}}
\newcommand{\id}{\mathsf{id}}
\newcommand{\type}{\tau}
\newcommand{\restrict}{\mathsf{restrict}}
%\newcommand{\any}{\mathsf{any}}
\newcommand{\any}{\top}
\newcommand{\dyn}{\top}
\newcommand{\dettypes}{{\sf dettypes}}
\newcommand{\Atom}{{\sf Atom}}
\newcommand{\vars}{\mathsf{vars}}
\newcommand{\Vars}{\mathsf{Vars}}
\newcommand{\range}{\mathsf{range}}
\newcommand{\varpos}{\mathsf{varpos}}
\newcommand{\varid}{\mathsf{varid}}
\newcommand{\argpos}{\mathsf{argpos}}
\newcommand{\elim}{\mathsf{elim}}
\newcommand{\pred}{\mathsf{pred}}
\newcommand{\predfuncs}{\mathsf{predfuncs}}
\newcommand{\project}{\mathsf{project}}
\newcommand{\reduce}{\mathsf{reduce}}
\newcommand{\positions}{\mathsf{positions}}
\newcommand{\contained}{\preceq}
\newcommand{\equivalent}{\cong}
\newcommand{\unify}{{\it unify}}
\newcommand{\Iff}{{\rm iff}}
%\newcommand{\And}{{\rm and}}
\newcommand{\Where}{{\rm where}}
%\newcommand{\State}{\mathsf{S}}
\newcommand{\qmap}{{\sf qmap}}
\newcommand{\fmap}{{\sf fmap}}
\newcommand{\ftable}{{\sf ftable}}
\newcommand{\Qmap}{{\sf Qmap}}
\newcommand{\states}{{\sf states}}
\newcommand{\head}{\tau}
\newcommand{\atomconstraints}{\mathsf{atomconstraints}}
\newcommand{\thresholds}{\mathsf{thresholds}}
\newcommand{\term}{\mathsf{Term}}
\newcommand{\trees}{\mathsf{trees}}
%\newcommand{\renames}{\mathsf{rens}}
%\newcommand{\renameps}{\mathsf{renps}}
\newcommand{\renames}{\rho_1}
\newcommand{\renameps}{\rho_2}
\newcommand{\predicates}{\mathsf{Predicates}}
\newcommand{\query}{\mathsf{q}}
\newcommand{\ans}{\mathsf{a}}
\newcommand{\trace}{\mathsf{tr}}
\newcommand{\constr}{\mathsf{constr}}
\newcommand{\Iproj}{\mathsf{proj}}
\newcommand{\SAT}{\mathsf{SAT}}
\newcommand{\interpolant}{\mathsf{interpolant}}
\newcommand{\unknown}{?}
\newcommand{\rhs}{{\sf rhs}}
\newcommand{\lhs}{{\sf lhs}}
\newcommand{\unfold}{{\sf unfold}}
\newcommand{\arity}{{\sf ar}}
\newcommand{\AND}{{\sf AND}}
\def\ll{[\![}
\def\rr{]\!]}
\newcommand{\todo}[1]{\textbf{**}\marginpar{\fbox{
\begin{minipage}{\oddsidemargin}
\textsf{{\small#1}}
\end{minipage}
}}}
\newcommand{\sset}[2]{\left\{~#1 \left|
\begin{array}{l}#2\end{array}
\right. \right\}}
\newcommand{\qin}{\hspace*{0.15in}}
\newenvironment{SProg}
{\begin{small}\begin{tt}\begin{tabular}[t]{l}}%
{\end{tabular}\end{tt}\end{small}}
\def\anno#1{{\ooalign{\hfil\raise.07ex\hbox{\small{\rm #1}}\hfil%
\crcr\mathhexbox20D}}}
\newtheorem{property}{Property}
\newtheorem{lemma}{Lemma}
\newtheorem{proof}{Proof}
\newtheorem{definition}{Definition}
\newtheorem{example}{Example}
\newtheorem{theorem}{Theorem}
\section{Introduction}
\label{ch7:intro}
In this paper we combine two existing techniques, namely abstract interpretation over the domain of convex polyhedra and interpolant tree automata in a new way for Horn clause verification. Abstract interpretation is a scalable program analysis technique which computes invariants allowing many program properties to be proven, but suffers from false alarms; safe but not provably safe programs may be indistinguishable from unsafe programs. Refinement is considered in this case. In previous work \cite{kafleG2015horn} we described an \emph{abstraction-refinement} scheme for Horn clause verification using abstract interpretation and refinement with finite tree automata. In that approach refinement eliminates a single spurious counterexample in each iteration of the abstraction-refinement loop, using a clause transformation based on a tree automata difference operation. In contrast to that work, we apply the method of Wang and Jiao
\cite{WangJ2015} for constructing an \emph{interpolant tree automaton} from an infeasible trace. This generalises the trace of a spurious counterexample, recognising a possibly infinite number of spurious counterexamples, which can then be eliminated in one iteration of the abstraction-refinement loop. We combine this construction in the framework of \cite{kafleG2015horn}. The experimental results on a set of Horn clause verification problems are reported, and compared with both \cite{kafleG2015horn} and the results of Wang and Jiao
\cite{WangJ2015} using trace abstraction and refinement.
%\begin{enumerate}
%%\item we show how to construct an interpolant tree automata from an infeasible Horn clause derivation (Section \ref{ch7:intautomata});
%
%\item we combine \emph{abstract interpretation} over the domain of convex polyhedra with \emph{interpolant tree automata} in an \emph{abstraction-refinement} scheme for Horn clause verification (Section \ref{ch7:application});
%
%
%\item we evaluate the effectiveness of this combination on a set of software verification benchmarks (Section \ref{ch7:experiments}).
%\end{enumerate}
In Section \ref{ch7:prelim} we introduce the key concepts of constrained Horn clauses and finite tree automata. Section \ref{ch7:intautomata} contains the definitions of interpolants and the construction of a tree interpolant automaton following the techniques of Wang and Jiao
\cite{WangJ2015}. In Section \ref{ch7:application} we describe our algorithm combining abstract interpretation with tree interpolant automata, including in Section \ref{ch7:experiments} an experimental evaluation and comparison with other approaches. Finally in Section \ref{ch7:rel} we discuss related work.
\section{Preliminaries}\label{ch7:prelim}
%Rather than eliminating a single spurious trace in each iteration of our abstraction-refinement procedure, one can generalise it to a larger set of traces which can be captured by an \emph{interpolant automata} which we define shortly.
A constrained Horn clause (CHC) is a first order predicate logic formula of the form
$\forall(\phi \wedge p_1(X_1) \wedge \ldots \wedge p_k(X_k) \rightarrow p(X))$ ($k \ge 0$), where $\phi$ is a first order logic formula (constraint) with respect to some background theory and $p_1,\ldots,p_k, p$ are predicate symbols. We assume (wlog) that $X_i, X$ are (possibly empty) tuples of distinct variables and $\phi$ is expressed in terms of $X_i, ~X$, which can be achieved by adding equalities to $\phi$. $p(X)$ is the head of the clause and $\phi \wedge p_1(X_1) \wedge \ldots \wedge p_k(X_k)$ is the body. There is a distinguished predicate symbol $\mathit{false}$ which is interpreted as $\false$. Clauses whose head is $\mathit{false}$ are called \emph{integrity constraints}. Following the notation used in constraint logic programming a clause is usually written as $H \leftarrow \phi, B_1, \ldots, B_k$ where $H, B_1,..., B_k$ stand for atomic formulas (atoms) $p(X), p_1(X_1), ..., p_k(X_k)$.
A set of CHCs is sometimes called a (constraint logic) program.
An interpretation of a set of CHCs is represented as a set of \emph{constrained facts} of the form $A \leftarrow \phi$ where $A$ is an atom and $ \phi$ is a formula with respect to some background theory. $A \leftarrow \phi$ represents a set of ground facts $A\theta$ such that $\phi \theta$ holds in the background theory ($\theta$ is called a grounding substitution). An interpretation that satisfies each clause in $P$ is called a model of $P$. In some works \cite{DBLP:conf/sas/BjornerMR13,McmillanR2013}, a \emph{model} is also called a \emph{solution} and we use them interchangeably in this paper.
\paragraph{Horn clause verification problem.}
Given a set of CHCs $P$, the CHC verification problem is to check whether there exists a model of $P$. It can easily be shown that $P$ has a model if and only if the fact $\mathit{false}$ is not a consequence of $P$.
\begin{figure}[t]
\centering
\begin{BVerbatim}
c1. fib(A, B):- A>=0, A=<1, B=1.
c2. fib(A, B) :- A>1, A2=A-2,
A1=A-1, B=B1+B2, fib(A1,B1), fib(A2,B2).
c3. false:- A>5, B<A, fib(A,B).
\end{BVerbatim}
\caption{Example CHCs (Fib) defining a Fibonacci function.}
\label{ch7:exprogram}
\end{figure}
%\todo{define horn clause derivations for say something informally}
An example set of CHCs, encoding the Fibonacci function is shown in Figure \ref{ch7:exprogram}. Since its derivations are trees, it serves as an interesting example from the point of view of \emph{interpolant tree automata}.
%Horn clause derivations can be captured using a formal representation known as finite tree automaton.
\begin{definition}[Finite tree automaton \cite{Comon}] An FTA $\A$ is a tuple $(Q, Q_f, \Sigma, \Delta)$, where
$Q$ is a finite set of states, $Q_f \subseteq Q$ is a set of final states, $\Sigma$ is a set of function symbols, and $\Delta$ is a set of transitions of the form $f(q_1, \ldots, q_n) \rightarrow q$ with $q, q_1, \ldots , q_n \in Q$ and $f \in \Sigma$.
We assume that $Q$ and $\Sigma$ are disjoint.
\end{definition}
%\todo{what was repeated here John}
We assume that each CHC in a program $P$ is associated with an identifier by a mapping $\id_P: P \rightarrow \Sigma$. An identifier (an element of $\Sigma$) is a function symbol whose arity is the same as the number of atoms in the clause body. For instance a clause $p(X) \leftarrow \phi, p_1(X_1), \ldots, p_k(X_k)$ is assigned a function symbol with arity $k$. As will be seen later, these identifiers are used to build trees that represent \emph{derivations} using the clauses. A set of derivation trees (traces) of a set of atoms of a program $P$ can be abstracted and represented by an FTA. We provide such a construction in Definition \ref{ch7:trace-fta}.
%Given a set of CHCs and a set $\Sigma$ of ranked function symbols, the function assigns identifiers to clauses in $P$.
%An identifier could be the name of a clause, but we want the name to be ranked so that we can get more information regarding the clause.
\begin{definition}[Trace FTA for a set of CHCs]
\label{ch7:trace-fta}
Let $P$ be a set of CHCs. Define the trace FTA for $P$ as $\A_P = (Q,Q_f,\Sigma,\Delta)$ where
\begin{itemize}
\item
$Q = \{ p \mid p ~ is ~a ~predicate ~symbol ~of ~P \} \cup \{\mathit{false} \} $;
\item
$Q_f = \{ \mathit{false} \}$;
\item
$\Sigma$ is a set of function symbols;
\item
$\Delta = \{c_j(p_1,\ldots,p_k) \rightarrow p \mid \mathrm{where~} c_j \in \Sigma, ~p(X) \leftarrow \phi, p_1(X_1), \ldots, p_k(X_k) \in P, ~c_j = \id_P(p(X) \leftarrow \phi, p_1(X_1), \ldots, p_k(X_k) )\}$.
\end{itemize}
\end{definition}
The elements of $\Lang(\A_P)$ are called trace-terms or trace-trees or simply traces of $P$ rooted at $\mathit{false}$.
\begin{example}
\label{ch7:exautP}
Let $Fib$ be the set of CHCs in Figure \ref{ch7:exprogram}. Let $\id_{Fib}$ map the clauses to identifiers $c_1,c_2,c_3$ respectively. Then $\A_{Fib} = (Q,Q_f,\Sigma,\Delta)$ where:
\[
\begin{array}{lll}
Q &=& \{\mathtt{fib}, \mathtt{false}\}\\
Q_{f} &=& \{ \mathtt{false}\}\\
\Sigma &=& \{ c_1, c_2, c_3\}\\
\Delta &=& \{ c_1 \rightarrow \mathtt{fib}, ~c_2(\mathtt{fib}, \mathtt{fib}) \rightarrow \mathtt{fib}, \\
&& c_3( \mathtt{fib}) \rightarrow \mathtt{false} \}
\end{array}
\]
\end{example}
%\begin{definition}[FTA for a trace-term]
\label{ch7:t-fta}
Similarly, we can also construct an FTA representing a single trace. It should be noted that the whole idea of representing program traces by FTAs is to use automata theoretic operations for dealing with program traces, for example, removal of an undesirable trace from a set of program traces.
Let $P$ be a set of CHCs and let $t \in \Lang(\A_P)$. There exists an FTA $\A_t$ such that $\Lang(\A_t) = \{t\}$. We illustrate the construction with an example.
%We assume that each node in the trace-tree is labelled by an identifier.
%\end{definition}
\begin{example}[Trace FTA]
Consider the FTA in Example \ref{ch7:exautP}. Let $t= c_{3}(c_{2}(c_{1}, c_1)) \in \Lang( \A_P)$. Then $\A_t = (Q,Q_f,\Sigma,\Delta)$ is defined as:
\[
\begin{array}{lll}
Q &=&\{ \mathtt{e_{1}, e_{2}, e_{3},e_{4}} \}\\
Q_{f} &=& \{ \mathtt{e_{1}}\} \\
\Sigma &=& \{ c_1, c_2, c_3, c_4\}\\
\Delta &=& \{ c_1 \rightarrow \mathtt{e_{3}}, ~c_1 \rightarrow \mathtt{e_{4}}, ~c_2(\mathtt{e_{3}, e_{4}}) \rightarrow \mathtt{e_2}, \\
&& ~c_3(\mathtt{e_2}) \rightarrow \mathtt{e_1} \} \\
%&& c_3( \mathtt{mc91}) \rightarrow \mathtt{false}, ~c_4( \mathtt{mc91}) \rightarrow \mathtt{false} \}
\end{array}
\]
\noindent
where $\Sigma$ is the same as in $\A_P$ and the states $\mathtt{e_i}$ $(i=1 \ldots 4)$ represent the nodes in the trace-tree, with root node $\mathtt{e_1}$ as the final state.
\end{example}
A trace-term is a representation of a \emph{derivation trees}, called an $\AND$-tree \cite{Stark89,Gallagher-Lafave-Dagstuhl} giving a proof of an atomic formula from a set of CHCs.
%An $\AND$-tree is unique up to variable renaming \cite{Stark89,Gallagher-Lafave-Dagstuhl}.
\begin{definition}[$\AND$-tree for a trace term $T(t)$ (adapted from \cite{kafleG2015horn})]
Let $P$ be a set of CHCs and let $t \in \Lang(\A_P)$.
An $\AND$-tree corresponding to $t$, denote by $T(t)$, is the following labelled tree, where each node of $T(t)$ is labelled by an atom, a clause identifier and a constraint.
\begin{enumerate}
\item
For each sub-term $c_j(t_1,\ldots,t_k)$ of $t$ there is a corresponding node in $T(t)$ labelled by an atom $p(X)$, an identifier $c_j$ such that $c_j = \id_P(p(X) \leftarrow \phi, p_1(X_1),\ldots,p_k(X_k))$, and a constraint $\phi$; the node's children (if $k>0$) are the nodes corresponding to $t_1,\ldots,t_k$ and are labelled by $p_1(X_1),\ldots,p_k(X_k)$.
\item
The variables in the labels are chosen such that if a node $n$ is labelled by a clause, the local variables in the clause body do not occur outside the subtree rooted at $n$.
\end{enumerate}
We assume that each node in $T(t)$ is uniquely identified by a natural number. We omit $t$ from $T(t)$ when it is clear from the context.
\end{definition}
\begin{figure}[h!]
\centering
\includegraphics[width=1.0 \textwidth, height=50mm]{images/traceTree.pdf}
\caption{A trace-term $c_3(c_2(c_1,c_1))$ of Fib (left) and its $\AND$-tree (right), where $\phi_1 \equiv \mathtt{A>5} \wedge \mathtt{B<A}; ~\phi_2 \equiv \mathtt{A>1} \wedge \mathtt{A2=A-2} \wedge \mathtt{A1=A-1} \wedge \mathtt{B=B1+B2}; ~\phi_3 \equiv \mathtt{A2\geq\ 0} \wedge
\mathtt{A2\leq\ 1} \wedge \mathtt{B2=1}; ~\phi_4 \equiv \mathtt{A1\geq\ 0} \wedge \mathtt{A1\leq\ 1} \wedge \mathtt{B1=1}$.}
\label{ch7:tracetree}
\end{figure}
The formula represented by an $\AND$-tree $T$, represented by $F(T)$ is
\begin{enumerate}
\item
$\phi$, if $T$ is a single leaf node labelled by a constraint $\phi$; or
\item
$\phi \wedge \bigwedge_{i=1..n}(F(T_i))$ if the root node of $T$ is labelled by the constraint $\phi$ and has subtrees
$T_1,\ldots,T_{n}$.
\end{enumerate}
The formula $F(T)$ where $T$ is the $\AND$-tree in Figure \ref{ch7:tracetree} is
\[
\begin{array}{l}
\mathtt{A>5} \wedge \mathtt{B<A} \wedge \mathtt{A>1} \wedge \mathtt{A2=A-2} \wedge \mathtt{A1= A-1} \wedge \mathtt{B=B1+B2}\\
\mathtt{A2\geq\ 0} \wedge \mathtt{A2\leq1} \wedge \mathtt{B2=1} \wedge \mathtt{A1\geq0} \wedge \mathtt{A1\leq1} \wedge \mathtt{B1=1}
\end{array}
\]
We say that an $\AND$-tree $T$ is satisfiable or feasible if $F(T)$ is satisfiable, otherwise unsatisfiable or infeasible. Similarly, we say a trace-term is satisfiable (unsatisfiable) iff its corresponding $\AND$-tree is satisfiable (unsatisfiable). The trace-term $c_3(c_2(c_1,c_1))$ in Figure \ref{ch7:tracetree} is unsatisfiable since $F(c_3(c_2(c_1,c_1))) $ is unsatisfiable.
%From this point on, a trace represents a trace of $\Lang( \A_P)$ and an $\AND$-tree (derivation tree) represents a tree corresponding to a trace of $\Lang( \A_P)$ unless otherwise stated.
%\todo{what about the following graph}
%
%\begin{definition}[ \emph{Tree-like} Horn clauses with \emph{integrity constraints}]
%\label{ch7:treelikeHC}
%A set of Horn clauses $P$ is \emph{tree-like} \cite{DBLP:conf/aplas/GuptaPR11,DBLP:conf/vstte/RummerHK13} if
%\begin{itemize}
%\item its predicate dependency graph is acyclic;
%\item for each predicate symbol $p$ there is at most one clause containing $p$ in its body ;
%\item for each predicate symbol $p$ there is at most one clause containing $p$ in its head ;
%\item every clause contains $p$ at most once.
%\item there is an integrity constraint.
% \end{itemize}
% \end{definition}
%
%Such \emph{tree-like} Horn clauses (Definition \ref{ch7:treelikeHC}) have a unique derivation tree rooted at any atom occurring in $P$, in particular $false$.
%
%To any derivation tree of Horn clauses $P$, we can construct a set of \emph{tree-like} Horn clauses by renaming the predicates appropriately. For the sake of space, we do not provide the details here but ask the readers to refer to \cite{DBLP:conf/aplas/GuptaPR11,McmillanR2013}.
%
%\begin{lemma}
%\label{ch7:solutionHCTree}
%Let $T$ be a derivation-tree of $P$ and $P_T$ be a set of \emph{tree-like} Horn clauses corresponding to $T$. $P_T$ has a solution iff $T$ is infeasible.
%\end{lemma}
\section{Interpolant tree automata}
\label{ch7:intautomata}
Refinement of trace abstraction is an approach to program verification \cite{DBLP:conf/sas/HeizmannHP09}. In this approach, if a property is not provable in an abstraction of program traces then an abstract trace showing the violation of the property is emitted. If such a trace is not feasible with respect to the original program, it is eliminated from the trace abstraction which is viewed as a refinement of the trace abstraction. The notion of interpolant automata \cite{DBLP:conf/sas/HeizmannHP09} allows one to generalise an infeasible trace to capture possibly infinitely many infeasible traces which can then be eliminated in one refinement step.
In this section, we revisit the construction of an \emph{interpolant tree automaton} \cite{WangJ2015} from an infeasible trace-tree. The automaton serves as a generalisation of the trace-tree; and we apply this construction in Horn clause verification.
\begin{definition}[(Craig) Interpolant \cite{DBLP:journals/jsyml/Craig57}]
\label{ch7:interpolant}
Given two formulas $\phi_1, \phi_2 $ such that $\phi_1 \wedge \phi_2 $ is unsatisfiable, a (Craig) interpolant is a formula $I$ with
(1) $\phi_1 \rightarrow I$; (2) $I \wedge \phi_2 \rightarrow \false$; and (3) vars($I$) $\subseteq$ vars($\phi_1$) $\cap$ vars($\phi_2$). An interpolant of $\phi_1$ and $\phi_2$ is represented by $I(\phi_1, \phi_2)$.
\end{definition}
The existence of an interpolant implies that $\phi_1 \wedge \phi_2$ is unsatisfiable \cite{DBLP:conf/cav/RummerHK13}. Similarly, if the background theory underlying the CHCs $P$ admits (Craig) interpolation \cite{DBLP:journals/jsyml/Craig57}, then every infeasible derivation using the clauses in $P$ has an interpolant \cite{McmillanR2013}.
\begin{example}[Interpolant example]
Let $\phi_1 \equiv \mathtt{A2 \leq 1} \wedge \mathtt{A > 1} \wedge \mathtt{A2 = A - 2} \wedge \mathtt{A1 = A - 1} \wedge \mathtt{B = B1 + B2}$ and $\phi_2 \equiv \mathtt{A>5} \wedge \mathtt{B<A}$ such that $\phi_1 \wedge \phi_2$ is unsatisfiable. Since the formula $I \equiv A \leq 3$ fulfills all the conditions of Definition \ref{ch7:interpolant}, it is an interpolant of $\phi_1$ and $\phi_2$.
\end{example}
%\begin{theorem}[\cite{McmillanR2013}]
%If the background theory underlying the CHCs $P$ admits (Craig) interpolation \cite{DBLP:journals/jsyml/Craig57}, then every infeasible derivation using the clauses in $P$ has an interpolant.
%\end{theorem}
Given a node $i$ in an $\AND$-tree $T$, we call $T_i$ the sub-tree rooted at $i$, $\phi_i$ the formula label of node $i$, $F(T_i)$ the formula of the sub-tree rooted at node $i$ and $G(T_i)$, the formula $F(T)$ except the formula $F(T_i)$, which is defined as follows:
\begin{enumerate}
\item
$\mathit{true}$, if $T$ is a single leaf node labelled by constraint $\phi$ and the node is $i$; or
\item
$\phi$, if $T$ is a single leaf node labelled by constraint $\phi$ and the node is different from $i$; or
\item
$\mathit{true}$, if the root node of $T$ is labelled by the
constraint $\phi$ and the node is $i$; or
\item
$\phi \wedge \bigwedge_{l=1..n}(G(T_l))$ if the root node of $T$ is labelled by the
constraint $\phi$, and the node is different from $i$ and has subtrees
$T_1,\ldots,T_{n}$.
\end{enumerate}
\begin{definition}[Tree Interpolant of an $\AND$-tree (\cite{WangJ2015})]
\label{ch7:treeInterpolant}
Let $T$ be an infeasible $\AND$-tree. A tree interpolant $TI(T)$ for $T$ is a tree constructed as follows:
\begin{enumerate}
\item
The root node $i$ of $TI(T)$ is labelled by $i$, the atom of the node $i$ of $T$ and the formula $\mathit{false}$;
\item
Each leaf node $i$ of $TI(T)$ is labelled by $i$, the atom of the node $i$ of $T$ and by $I(F(T_i), G(T_i))$;
\item
Let $i$ be any other node of $T$. We define $F_1$ as $(\phi_i \wedge \bigwedge_{k=1}^n I_k)$ where $\bigwedge_{k=1}^n I_k$ ($n\geq1$) is the conjunction of formulas representing the interpolants of the children of the node $i$ in $TI(T)$. Then
the node $i$ of $TI(T)$ is labelled by $i$, the atom of the node $i$ of $T$ and the formula $I(F_1 , G(T_i))$.
\end{enumerate}
\end{definition}
The \emph{tree interpolant} corresponding to \emph{AND tree} in Figure \ref{ch7:tracetree}(b) is shown in Figure \ref{ch7:interpolanttree}(b).
\begin{figure}[h!]
\centering
\includegraphics[width=1.0 \textwidth, height=50mm]{images/interpolantTree.pdf}
\caption{\emph{AND tree} of Figure \ref{ch7:tracetree} (left) and its \emph{tree interpolant} (right). Let $I_j$ represents an interpolant of the node $j$. Then $I_1 \equiv \mathit{false}$; $I_4 \equiv I(\phi_4, \phi_3 \wedge \phi_1 \wedge \phi_2$) ; $I_3 \equiv I(\phi_3, \phi_1 \wedge \phi_2 \wedge I_4)$; $I_2 \equiv I(I_3 \wedge I_4 \wedge \phi_2, \phi_1)$.}
\label{ch7:interpolanttree}
\end{figure}
Since there is a one-one correspondence between an $\AND$-tree and a trace-term, we can define a tree interpolant for a trace-term as follows:
\begin{definition}[Tree Interpolant of a trace-term $TI(t)$] Given an infeasible trace-term $t$, its tree interpolant, represented as $TI(t)$, is the tree interpolant of its corresponding $\AND$-tree.
\end{definition}
\begin{definition}[Interpolant mapping $\Pi_{TI}$]
\label{ch7:interpolantmapping}
Given a tree interpolant $TI$ for some tree, $\Pi_{TI}$ is a mapping from the atom labels and node numbers of each node in $TI$ to the formula label such that $\Pi_{TI}(A^j)=\psi$ where $A$ is the atom label and $\psi$ is the formula label at node $j$.
\end{definition}
%If $TI(t)$ be a tree interpolant for some infeasible trace $t \in \A_P$, then we say $\Pi_{TI(t)}$ is a solution (model) of $t$.
For our example program $\Pi_{TI}$ is the following:
$$\{ false^1 \mapsto \mathit{false}, fib^2(A,B) \mapsto A \le 3, fib^3(A2,B2) \mapsto A \le 1, fib^4(A1,B1) \mapsto \mathit{true} \}$$
\begin{property}[Tree interpolant property]
Let $TI(T)$ be a tree interpolant for some infeasible $\AND$-tree $T$. Then
\begin{enumerate}
\item $\Pi_{TI}(r^i)=\mathit{false}$ where $r$ is the atom label of the root of $TI(T)$;
\item for each node $j$ with children $j_1, ..., j_n$ ($n\geq 0$) the following property holds: \\
$(\bigwedge_{k=0}^n \Pi_{TI}(A^{j_k})) \wedge \phi_j \rightarrow \Pi_{TI}(A^{j})$ where $\phi_j$ is the formula label of the node $j$ of $T$;
%where $A_{j}$ is the atom label of the node $j$ in $\Pi(T)$.
\item for each node $j$ the following property holds: \\
$vars(\Pi_{TI}(A^j)) \subseteq (vars(F(T_j)) \cap vars(G(T_j)))$, where the formula $F(T_j)$ and $G(T_j)$ corresponds to $T$.
\end{enumerate}
\end{property}
%\begin{proof}
%(sketch)
%
%\begin{itemize}
%
%\item
%Point (1) follows from point (1) of Definition \ref{ch7:treeInterpolant}.
%
%\item
%Point (2): we reason by cases:
%
%
%\begin{itemize}
%
%\item Case 1 (node $j$ is a leaf node):
%
%so we need to prove $ \phi_j \rightarrow \Pi_{TI}(A^{j})$. This follows from the point (2) of Definition \ref{ch7:treeInterpolant} and from the point (1) of Definition \ref{ch7:interpolant}.
%
%
%
%\item Case 2 (node with children $\geq 1$):
%
% This follows from the point (3) of Definition \ref{ch7:treeInterpolant} and from the point (1) of Definition \ref{ch7:interpolant}.
%
%\end{itemize}
%
%\item
%
%Point (3): we reason by cases:
%
%
%\begin{itemize}
%
%\item Case 1 ( leaf node):
%
% This follows from the point (2) of Definition \ref{ch7:treeInterpolant} and from the point (3) of Definition \ref{ch7:interpolant}.
%
%
%
%\item Case 2 (node with children $\geq 1$):
%
% This follows from the point (3) of Definition \ref{ch7:treeInterpolant} and from the point (3) of Definition \ref{ch7:interpolant}.
%
%\end{itemize}
%
%
%
%\end{itemize}
%
%
%\end{proof}
%Now we define an injective mapping
%$\sigma: Atom \times J \rightarrow FTA ~ States$ where $\sigma$ maps an atom occurring in a set of CHCs and an index to a FTA state.
\begin{definition}[Interpolant tree automaton for Horn clauses $\A^I_t$=$(Q, Q_f, \Sigma, \Delta)$ \cite{WangJ2015}]
\label{ch7:interpolantautomata}
Let $P$ be a set of CHCs, $t \in \Lang(\A_P)$ be any infeasible trace-term and $TI(t)$ be a tree interpolant of $t$. Let $\sigma: As \times J \rightarrow Q$ where $\sigma$ maps an atom at node $i \in J$ of $TI(t)$ to an FTA state in $Q$. Define $\rho: Pred^J \rightarrow Pred$ which maps a predicate name with superscript to a predicate name of $P$. Then the interpolant automaton of $t$ is defined as an FTA $\A^I_t$ such that
\begin{itemize}
\item
$Q= \{ \sigma(A,i): A ~ is ~ the ~ atom ~ label ~ of ~the ~ node ~ i ~ of ~ TI(t) \}$;
\item
$F=\{ \sigma(A,i): A ~ is ~ the ~ atom ~ label ~of ~the ~root ~of ~ TI(t) \}$;
\item
$\Sigma$ is a set of function symbols of $P$;
\item
$\Delta = \{c(p_1^{j_1},\ldots, p_k^{j_k}) \rightarrow p^{j} \mid ~cl = p(X) \leftarrow \phi, p_1(X_1), \ldots, p_k(X_k) \in P, ~c = \id_P(cl), ~ \rho(p^i)=p,$ \\
$\rho(p_m^i)=p_m ~for ~m =1..k ~and ~ \Pi_{TI}(p^{j})(X) \leftarrow \phi,\Pi_{TI}(p_1^{j_1})(X_1), \ldots, \Pi_{TI}(p_k^{j_k})(X_k) \}$.
\end{itemize}
\end{definition}
\begin{example}[Interpolant automata for $c_3(c_2(c_1,c_1))$]
\[
\begin{array}{lll}
Q &=& \{\mathtt{fib^2}, \mathtt{fib^3},\mathtt{fib^4},\mathtt{error}\}\\
Q_{f} &=& \{ \mathtt{error}\}\\
\Sigma &=& \{ c_1, c_2, c_3\}\\
\Delta &=& \{ c_1 \rightarrow \mathtt{fib^2},
c_1 \rightarrow \mathtt{fib^3},
c_1 \rightarrow \mathtt{fib^4}, \\ &&
c_2(\mathtt{fib^2},\mathtt{fib^2}) \rightarrow \mathtt{fib^4},
c_2(\mathtt{fib^2},\mathtt{fib^3}) \rightarrow \mathtt{fib^2}, \\ &&
c_2(\mathtt{fib^2},\mathtt{fib^3}) \rightarrow \mathtt{fib^4},
c_2(\mathtt{fib^2},\mathtt{fib^4}) \rightarrow \mathtt{fib^4}, \\ &&
c_2(\mathtt{fib^3},\mathtt{fib^2}) \rightarrow \mathtt{fib^2},
c_2(\mathtt{fib^3},\mathtt{fib^2}) \rightarrow \mathtt{fib^4}, \\ &&
c_2(\mathtt{fib^3},\mathtt{fib^3}) \rightarrow \mathtt{fib^2},
c_2(\mathtt{fib^3},\mathtt{fib^3}) \rightarrow \mathtt{fib^4}, \\ &&
c_2(\mathtt{fib^3},\mathtt{fib^4}) \rightarrow \mathtt{fib^2},
c_2(\mathtt{fib^3},\mathtt{fib^4}) \rightarrow \mathtt{fib^4}, \\ &&
c_2(\mathtt{fib^4},\mathtt{fib^2}) \rightarrow \mathtt{fib^4},
c_2(\mathtt{fib^4},\mathtt{fib^3}) \rightarrow \mathtt{fib^2}, \\ &&
c_2(\mathtt{fib^4},\mathtt{fib^3}) \rightarrow \mathtt{fib^4},
c_2(\mathtt{fib^4},\mathtt{fib^4}) \rightarrow \mathtt{fib^4}, \\ &&
c_3(\mathtt{fib^2}) \rightarrow \mathtt{error},
c_3(\mathtt{fib^3}) \rightarrow \mathtt{error} \}
\end{array}
\]
\end{example}
The construction described in Definition \ref{ch7:interpolantautomata} recognizes only infeasible traces terms of $P$ as stated in Theorem \ref{ch7:soundness}.
\begin{theorem}[Soundness]
\label{ch7:soundness}
Let $P$ be a set of CHCs and $t \in \Lang(\A_P)$ be any infeasible trace-term. Then the interpolant automaton $\A^I_{t}$ recognises only infeasible trace-terms of $P$.
\end{theorem}
%\begin{proof}
%(sketch)
%%By induction on the height of the trace-tree.
%
%Let $t' \in \Lang(\A_P)$ be any trace-term different from $t$ recognized by $\A^I_{t}$.
%
%To prove: $t'$ is infeasible.
%
%\begin{itemize}
%
%\item
%There is a tree interpolant $TI$ according to which $\A^I_{t}$ is constructed and there is a mapping $\Pi_{TI}$ which maps each FTA states to a formula in $TI$ (Definition \ref{ch7:interpolantautomata});
%
%\item Whenever a symbol in $t'$ representing a clause of the form
%
%$p^{j}(X) \leftarrow \phi, p_1^{j_1}(X_1), \ldots, p_k^{j_k}(X_k)$ ($k \geq 0$) is accepted at some state in $\A^I_{t}$, then $\Pi_{TI}$ maps the state $p^{j}$ corresponding to the head of the clause to a formula in $TI$ and the head of the root clause accepted by $\A^I_{t}$, that is, $false$, is correctly mapped to its interpretation, $\false$.
%
%\item
%This means $t'$ is infeasible (Lemma \ref{ch7:solutionHCTree}).
%
%\end{itemize}
%
%\end{proof}
%Since the \emph{interpolant tree automata} of an infeasible trace can (possibly) recognise an infinite number of traces, it is useful to characterise the set of traces recognised by them. We do so in Lemma \ref{ch7:traceCharacterisation}.
%
%\begin{lemma}[Trace characterisation]
%\label{ch7:traceCharacterisation}
%Let $t \in \Lang(\A_P)$ be any infeasible trace and $\Pi_{TI(t)}$ be a solution of \emph{tree-like} Horn clauses corresponding to $t$. If $\Pi_{TI(t)}$ is a solution of any other
%\emph{tree-like} Horn clauses corresponding to $t' \in \Lang(\A_P)$ for $t' \neq t$ then $\A^I_t$ also recognise $t'$.
%\end{lemma}
%
%It is desirable that the \emph{interpolant tree automata} of a trace $t \in \Lang(\A_P)$ recognize as many traces as possible. In an ideal situation, all infeasible traces of $P$. We will state in Theorem \ref{ch7:completeness}, the condition on which this happens. Before doing so, we need the following definitions and a lemma.
\begin{definition}[Conjunctive interpolant mapping]
\label{ch7:conjunctiveInterpolantmapping}
Given an interpolant mapping $\Pi_{TI}$ of a tree interpolant $TI$, we define
a conjunctive interpolant mapping for an atom label $A$ of any node in $TI$, represented as $\Pi^c_{TI}(A)$, to be the following formula $ \Pi^c_{TI}(A)=\bigwedge_{j } \Pi_{TI}(A^j)$, where $j$ ranges over the nodes of $TI$. It is the conjunction of interpolants of all the nodes of $TI$ with atom label $A$. The conjunctive interpolant mapping of $TI$ is represented is $ \Pi^c_{TI} = \{ \Pi^c_{TI}(A) \mid ~A ~is ~the ~atom ~label ~of ~TI\}$.
\end{definition}
%
%\begin{theorem}[Conjunctive solution \cite{McmillanR2013}]
%\label{ch7:conjunctiveSolution}
%Let $t \in \Lang(\A_P)$ be any infeasible trace. Then $\Pi^c_{TI(t)}$ is a solution (model) of \emph{tree-like} Horn clauses corresponding to $t$.
%\end{theorem}
%
%An interpretation of a set of CHCs $P$ is represented as a set of \emph{facts} of the form $A \leftarrow \phi$ where $A$ is an atom occurring in $P$ and $ \phi$ is a formula with respect to some background theory underlying the clauses in $P$. An interpretation that makes each clause in $P$ $\true$ is called a model of $P$.
%
It is desirable that the \emph{interpolant tree automaton} of a trace $t \in \Lang(\A_P)$ recognizes as many infeasible traces as possible, in an ideal situation, all infeasible traces of $P$. This is possible under the condition described in Theorem \ref{ch7:completeness}.
\begin{theorem}[Model and Interpolant Automata ]
\label{ch7:completeness}
Let $t \in \Lang(\A_P)$ be any infeasible trace-term. If $\Pi^c_{TI(t)}$
is a model of $P$, then the interpolant automaton of $t$ recognises all infeasible trace-terms of $P$.
\end{theorem}
%
%\begin{proof}
%(sketch)
%\begin{itemize}
%\item
%
%$P ~has ~a ~model ~ \implies P \not \models false$;
%
%\item all derivation trees of $P$ with root $false$ are infeasible (correspondence between $\AND$-trees and derivations \cite{JaffarM94}). In other words, all trace-terms of $P$;
%
%\item $\Pi^c_{TI(t)}$ is a model of all \emph{tree-like} Horn clauses corresponding to $t \Lang_(A_P)$ (since $\Pi^c_{TI(t)}$ is a model of $P$);
%
%\item $\Pi^c_{TI(t)}$ is a model of \emph{tree-like} Horn clauses corresponding to $t$ (lemma \ref{ch7:conjunctiveSolution});
%
%\item $\A^I_t$ recognizes all infeasible trace terms of $P$ (using lemma \ref{ch7:traceCharacterisation} repeatedly for all trace-terms $t' \neq t$ of $P$).
%
%\end{itemize}
%
%\end{proof}
\section{Application to Horn clause verification}
\label{ch7:application}
An \emph{abstraction-refinement} scheme for Horn clause verification is described in \cite{kafleG2015horn} which is depicted in Figure \ref{ch7:fig:toolchain}. In this, a set of CHCs $P$ is analysed using the techniques of \emph{abstract interpretation} over the domain of convex polyhedra which produces an over-approximation $M$ of the minimal model of $P$. The set of traces used during the analysis can be captured by an FTA $\A_P^M$ (see Definition \ref{ch7:model-fta}). This automaton recognizes all trace-terms of $P$ except some infeasible ones. Some of the infeasible trace-terms are removed by the abstract interpretation. $P$ is solved or safe (that is, it has a model) if $\mathit{false} \not\in M$. If this is not the case, a trace-term $t \in \Lang(A_P^M)$ is selected and checked for feasibility. If the answer is positive, $P$ has no model, that is, $P$ is unsafe.
Otherwise $t$ is considered spurious and this drives the refinement process. The refinement in \cite{kafleG2015horn} consists of constructing an automaton $\A'_P$ which recognizes all traces in $\Lang(\A_P^M) \setminus \Lang(\A_t)$ and generating a refined set of clauses from $P$ and $\A'_P$. The automata difference construction refines a set of traces (abstraction), which induces refinement in the original program. The refined program is again fed to the abstract interpreter. This process continues until the problem is safe, unsafe or the resources are exhausted. We call this approach Refinement of Abstraction in Horn clauses using Finite Tree automata, $\rahft$ in short.
The approach just described lacks generalisation of spurious counterexamples during refinement. However, in our current approach, we generalise a spurious counterexample through the use of \emph{interpolant automata}. Section \ref{ch7:intautomata} describes how to compute an \emph{interpolant automaton} (taken from \cite{WangJ2015}) corresponding to an infeasible Horn clause derivation. We first construct an \emph{interpolant automaton} viz. $\A^I_t$ corresponding to $t$. In Figure \ref{ch7:fig:toolchain}, this is shown by a blue line (in the middle) connecting the Abstraction and Refinement boxes. The refinement proceeds as in $\rahft$ with the only difference that $\A'_P$ now recognizes all traces in $\Lang(\A_P^M) \setminus \Lang(\A^I_t)$. We call this approach Refinement of Abstraction in Horn clauses using Interpolant Tree automata, $\rahit$ in short.
\begin{figure}[h!]
\begin{center}
\adjustbox{max width=\linewidth}{
\begin{tikzpicture}
\draw[thick, color=blue] (0.5,0) rectangle (15,6);
\begin{scope}
\node at (6,5.1) {\it FTAM -- Finite tree automata manipulator};
\node at (4.5,5.6) {\it AI --Abstract interpretation};
%\node at (12.2,5.6) {\it PP -- Pre-processing};
\node at (12.2,5.1) {\it CG -- Clauses generator};
% \node at (1.7,3.8) {CHC $P$};
% \draw[thick][->] (1.5,3.6) -- (1.5,2.5);
\draw[thick,dashed,green] (.6,1.2) rectangle (7.5,4.5);
\node at (5.9,4.1) {\it Abstraction };
\draw[thick,dashed,red] (7.8,1.2) rectangle (14.7,4.5);
\node at (12.6,4.1) {\it Refinement};
%\draw[blue] (.8,1.5) rectangle (2.0,2.5);
%\node at (1.5,2) {PP};
\node at (2.4,3.5) {CHC $P$};
\draw[thick][->] (2.2,3.3) -- (2.2,2.5);
\draw[blue] (1.5,1.5) rectangle (2.7,2.5);
\node at (2.2,2) {AI };
% \node at (4.2,3.4) {\bf Approximation };
% \node at (9.1,2.8) {\bf no };
%\draw[thick][->] (4,2.5) -- (4,3.2);
\node at (3.9,2.4) { $\A_P^M$};
\draw[thick][->] (2.7,2.1) -- (4.5,2.1);
\node at (3.9,1.8) { $M$};
\draw[thick][->] (2.7,1.6) -- (4.5,1.6);
\node at (6.1,3.4) {\bf safe };
\node at (6.4,2.8) {\bf no };
\draw[thick][->] (6.1,2.5) -- (6.1,3.2);
\node at (6.1,0.3) {\bf unsafe };
\node at (6.1,1.1) {\bf yes and feasible };
\draw[thick][->] (6.1,1.5) -- (6.1,0.7);
%refiner
\node at (10.2,2.5) {$\A_P^M$};
\draw[thick][->] (7.2,2.3) -- (11.2,2.3);
\node at (10.2,1.9) { $\A^I_t$};
\draw[thick, blue][->] (7.2,2) -- (11.2,2);
\node at (10.2,1.4) { $\A_t$};
\draw[thick][->] (7.2,1.6) -- (11.2,1.6);
%\node at (12,2.3) {constrs};
% \draw[->] (10.2,2) -- (13,2);
\node at (10.5,0.8) {CHC $P_1$ };
\node at (3,0.8) { $P \leftarrow P_1$ };
\draw[thick][-] (13.9,1.5) -- (13.9,0.5);
\draw[thick][-] (13.9,0.5) -- (2,0.5);
\draw[thick][->] (2,0.5) -- (2,1.5);
\draw[thick][->] (13.9,3.2) -- (13.9,2.5);
\node at (14,3.4) {CHC $P$};
\draw[blue] (4.5,1.5) rectangle (7.2,2.5);
\node at (5.9,2.3) {$false \in$ M?};
\draw[-] (4.5,2) -- (7.2, 2);
\node at (6.0,1.8) {$t \in \Lang(\A_P^M)$ };
\draw[blue] (11.2,1.5) rectangle (12.4,2.5);
\node at (11.8,2) {FTAM};
\node at (12.9,2.4) {$\A'_P$};
\draw[thick][->] (12.4,2.1) -- (13.4,2.1);
\draw[blue] (13.4,1.5) rectangle (14.6,2.5);
\node at (14,2) {CG};
\end{scope}
\end{tikzpicture}
}
\end{center}
\caption{\it Abstraction-refinement scheme in Horn clause verification \cite{kafleG2015horn}. $M$ is an approximation produced as a result of abstract interpretation. $\A'_P$ recognizes all traces in $\Lang(\A_P^M) \setminus \Lang(\A_t)$. }
\label{ch7:fig:toolchain}
\end{figure}
Next we briefly describe how to generate an FTA, $\A_P^M$, corresponding to a set of clauses $P$ using the approximation produced by \emph{abstract interpretation}.
%This FTA captures all trace-terms of $P$ except some infeasible ones.
Finally we show some experimental results using our current approach on a set of Horn clause verification benchmarks.
%\subsection{Abstract FTA}
%\label{ch7:absAutomata}
%In Figure \ref{ch7:alg-naive} we present an algorithm, which constructs an FTA corresponding to $P$ from an approximation of the minimal model of $P$. Note that the FTA produced by the algorithm is same as $\A_P$ (Definition \ref{ch7:trace-fta}) except that transitions corresponding to clauses whose bodies are not satisfiable in the convex polyhedral approximation are omitted, since they cannot contribute to feasible derivations. We refer to \cite{HenriksenGB07} for details on how to construct an over-approximation of the minimal model of $P$ using \emph{abstract interpretation} over the domain of convex polyhedra. An over-approximation of a set of CHCs is represented as a set of \emph{constrained facts} of the form $A \leftarrow \phi$ (one for each $A$) where $A$ is an atomic formula $p(Z_1,\ldots,Z_n)$ where $Z_1,\ldots,Z_n$ are distinct variables and $\phi$ is a formula over $Z_1,\ldots,Z_n$ with respect to some background theory.
%
%Given an over-approximation $M$, the algorithm in Figure \ref{ch7:alg-naive} generates an abstract FTA for $P$. The idea is as follows: for each of the clause of the form $c: p(X) \leftarrow \phi, p_1(X_1) \ldots p_k(X_k) (k \geq 0) \in P$, if the conjunction of over-approximation of the body atoms $p_1(X_1) \ldots p_k(X_k)$ under $M$ is satisfiable (see \emph{if ... then condition} in Figure \ref{ch7:alg-naive}), then we add the corresponding transition $\{c(p_1,\ldots,p_k) \rightarrow p \}$ to the set of transitions, and the corresponding set of states $\{ p, p_1, \ldots p_k\}$ to the set of states. The alphabet $\Sigma$ is the set of clause identifiers of $P$ and the set of final states is the singleton set $\{ \mathit{false}\}$.
%% \gets \{ \id_P(cl): cl \in P \}$
%\begin{figure}
% \centering
% \fbox{
%\begin{minipage}{13 cm}
% \begin{algorithmic}
% \Procedure{FTA construction using Convex Polyhedral approximation for Horn clauses } {Input: CHCs $P$ and polyhedral approximation $M$, Output: $\A_P = (Q,Q_f ,\Sigma,\Delta)$}
%%\State $i \gets 0$
%%\State $Z_0 \gets \bot$
%%\State $New \gets \bot$
%\State $\Delta \gets \emptyset$;
%\State $Q \gets \emptyset$;
%\State $\Sigma \gets \{ \id_P(cl): cl \in P \}$
%\ \\
%%\State{\textbf{a. Convex Polyhedral approximation for Horn clauses}}
%%\ \\
%%\Repeat
%% \ForAll {$p(X) \leftarrow Body \in P$}
%% \State $New \gets New \sqcup \solve(p(X),Body,Z_i)$ \Comment{Upper bound}
%% \EndFor
%% \State $Z_{i+1} \gets Z_i \nabla (New \sqcup Z_i)$ \Comment{Upper bound and widen}
%% \State $i \gets i+1$
%%\Until{$Z_i \sqsubseteq Z_{i-1}$}
%%%\State \Return $Z_i$
%%\ \\
%
%
%\ForAll {$c: p(X) \leftarrow \phi, p_1(X_1) \ldots p_k(X_k) (k \geq 0) \in P$}
%
%\Comment{where $c = \id_P(p(X) \leftarrow \phi, p_1(X_1), \ldots, p_k(X_k)$ }
%
%\If {$\SAT(\phi \wedge \gamma(p_1(X_1), M) \wedge \ldots \wedge \gamma(p_1(X_1), M))$}
% \State $\Delta \gets \Delta \cup \{c(p_1,\ldots,p_k) \rightarrow p \}$
% \State $Q \gets Q \cup \{ p, p_1, \ldots p_k\}$
% %\State $\Sigma \gets \Sigma \cup \{ c\}$
%
%\EndIf
%
%
%\EndFor
%
%\State $Q \gets Q \cup \{\mathit{false}\}$
%\State $Q_f \gets \{ \mathit{false}\}$
%
%\State \Return $\A_P = (Q,Q_f ,\Sigma,\Delta)$
%\EndProcedure
%\end{algorithmic}
%\end{minipage}
%}
%
% \caption{Generation of FTA based on a Convex Polyhedral Analysis.
%% Given a clause $p(X) \leftarrow Body$, the function $\solve(p(X),Body,Z_i)$ returns a constrained fact $p(X) \leftarrow \phi$, where $\phi$ is the result of solving $Body$ in the current approximation $Z_i$.
% Let $\gamma: \mathcal{A} \times \mathcal{M} \rightarrow \mathcal{F}$ be an injective mapping.
%$\gamma(A,M)$ returns a formula $\phi \in \mathcal{F}$ corresponding to an atom $A \in \mathcal{A}$ in $M \in \mathcal{M}$.}
%
% \label{ch7:alg-naive}
%\end{figure}
%
%\begin{figure}
% \centering
% \fbox{
%\begin{minipage}{13 cm}
% \begin{algorithmic}
% \Procedure{Abstract automata construction using Convex Polyhedral approximation for Horn clauses} {Input: CHCs $P$, Output: $\A_P = (Q,Q_f ,\Sigma,\Delta)$}
%%\State $i \gets 0$
%%\State $Z_0 \gets \bot$
%%\State $New \gets \bot$
%\State $\Delta \gets \emptyset; Q \gets \emptyset; \Sigma \gets \{ \id_P(cl): cl \in P \}$
%\ \\
%%\State{\textbf{a. Convex Polyhedral approximation for Horn clauses}}
%%\ \\
%%\Repeat
%% \ForAll {$p(X) \leftarrow Body \in P$}
%% \State $New \gets New \sqcup \solve(p(X),Body,Z_i)$ \Comment{Upper bound}
%% \EndFor
%% \State $Z_{i+1} \gets Z_i \nabla (New \sqcup Z_i)$ \Comment{Upper bound and widen}
%% \State $i \gets i+1$
%%\Until{$Z_i \sqsubseteq Z_{i-1}$}
%%%\State \Return $Z_i$
%%\ \\
%\State{\textbf{ Constructing automata from the over-approximation $Z_i $}}
%\ \\
%
%\ForAll {$c: p(X) \leftarrow \phi, p_1(X_1) \ldots p_k(X_k) (k \geq 0) \in P$}
%
%\Comment{where $c = \id_P(p(X) \leftarrow \phi, p_1(X_1), \ldots, p_k(X_k)$ }
%
%\If {$\SAT(\phi \wedge \gamma(p_1(X_1), Z_i) \wedge \ldots \wedge \gamma(p_1(X_1), Z_i))$}
% \State $\Delta \gets \Delta \cup \{c(p_1,\ldots,p_k) \rightarrow p \}$
% \State $Q \gets Q \cup \{ p, p_1, \ldots p_k\}$
% %\State $\Sigma \gets \Sigma \cup \{ c\}$
%
%\EndIf
%
%
%\EndFor
%
%\State $Q \gets Q \cup \{\mathit{false}\}$
%\State $Q_f \gets \{ \mathit{false}\}$
%
%\State \Return $\A_P = (Q,Q_f ,\Sigma,\Delta)$
%\EndProcedure
%\end{algorithmic}
%\end{minipage}
%}
%
% \caption{Generation of abstract automata using Convex Polyhedral Analysis. Given a clause $p(X) \leftarrow Body$, the function $\solve(p(X),Body,Z_i)$ returns a constrained fact $p(X) \leftarrow \phi$, where $\phi$ is the result of solving $Body$ in the current approximation $Z_i$. Let $\gamma: \mathcal{A} \times \mathcal{M} \rightarrow \mathcal{F}$ be an injective mapping.
%$\gamma(A,M)$ returns a formula $\phi \in \mathcal{F}$ corresponding to an atom $A \in \mathcal{A}$ in $M \in \mathcal{M}$.}
%
% \label{ch7:alg-naive}
%\end{figure}
\paragraph{Obtaining an FTA from a program and a model.}
Let $M$ be a set of constrained atoms of the form $p(X) \leftarrow \phi$ where $p$ is a program predicate and $\phi$ is a constraint over $X$.
Given such an set $M$, define $\gamma_M$ to be the mapping from atoms to constraints such that $\gamma_M(p(X)) = \phi$ for each constrained fact $p(X) \leftarrow \phi$. $M$ is a model of $P$ (called a \emph{syntactic solution} in \cite{WangJ2015}) if for each clause $p(X) \leftarrow \phi,p_1(X_1), \ldots,p_n(X_n)$ in $P$, $\phi \wedge \bigwedge_{i=1}^n \gamma_M(p_i(X_i)) \rightarrow \gamma_M(p(X))$.
Given such an $M$, we construct an FTA corresponding to $P$, which is the same as $\A_P$ (Definition \ref{ch7:trace-fta}) except that transitions
corresponding to clauses whose bodies are not satisfiable in the model are omitted, since they cannot contribute to feasible derivations.
\begin{definition}[FTA defined by a model.]\label{ch7:model-fta}
Let $P$ be a set of CHCs and $M$ be a model defined by a set of constrained facts. Then the FTA $\A_P^M = (Q,Q_f,\Sigma,\Delta_M)$ where $Q,Q_f$ and $\Sigma$ are the same as for $\A_P$ (Definition \ref{ch7:trace-fta}) and $\Delta_M$ is the following set of transitions.
\[
\begin{array}{ll}
\Delta_M = \{c(p_1,\ldots,p_n) \rightarrow p \mid &id_P(c) = p(X) \leftarrow \phi,p_1(X_1), \ldots,p_n(X_n),\\
& \SAT(\phi \wedge \bigwedge_{i=1}^n \gamma_M(p_i(X_i)))
\end{array}
\]
\end{definition}
\begin{lemma}
Let $P$ be a set of clauses and $M$ be a model of $P$ then $\Lang(\A_P^M)$ includes all feasible trace-terms of $P$ rooted at $\mathit{false}$.
\end{lemma}
In our experiments, the abstract interpretation was over the domain of convex polyhedra, yielding a set of constrained facts where each constraints is a conjunction of linear equalities and inequalities representing a convex polyhedron.
\begin{example}[FTA produced as a result of \emph{abstract interpretation}]
For our example program in Figure \ref{ch7:exprogram}, the convex polyhedral abstraction produces an over-approximation $M$ which is represented as
\[
M = \{\mathit{fib(A,B)} \leftarrow \mathit{A>=0},\mathit{B>=1},\mathit{-A+B>=0}\}
\]
Since there is no constrained fact for $\mathit{false}$ in $M$, this is a model for the example program. Our abstraction-refinement approach terminates at this point. However for the purpose of example, we show the FTA constructed for the example program using $M$. Since the bodies of each clauses except the integrity constraint are satisfied under $M$, the FTA is same as the one depicted in Example \ref{ch7:exautP} except the transition $c_3( \mathtt{fib}) \rightarrow \mathtt{false}$, which is removed because of abstract interpretation.
\end{example}
\subsection{Experiments}
\label{ch7:experiments}
For our experiment, we have collected a set of 68 programs from different sources.
\begin{enumerate}
\item A set of 30 programs from SV-COMP'15 repository\footnote{http://sv-comp.sosy-lab.org/2015/benchmarks.php} \cite{DBLP:conf/tacas/000115} (recursive category) and translated them to Horn clauses using inter-procedural encoding of SeaHorn \cite{DBLP:conf/tacas/GurfinkelKN15,DBLP:conf/cav/GurfinkelKKN15} producing (mostly) non-linear Horn clauses.
\item A set of 38 problems taken from the source repository\footnote{https://github.com/sosy-lab/sv-benchmarks/tree/master/clauses/LIA/Eldarica}, compiled by the authors of the tool Eldarica \cite{DBLP:conf/fm/HojjatKGIKR12}. This set consists of problems, among others, from the NECLA static analysis suite, from the paper \cite{DBLP:conf/tacas/JhalaM06}. These tasks are also considered in \cite{WangJ2015} and are interpreted over \emph{integer linear arithmetic}.
\end{enumerate}
We made the following comparison between the tools.
\begin{enumerate}
\item We compare $\rahit$ with $\rahft$, which compares the effect of removing a set of traces rather than a single trace.
\item We compare $\rahit$ with the \emph{trace-abstraction} tool \cite{WangJ2015} (\emph{TAR} from now on). $\rahit$ uses polyhedral approximation combined with trace abstraction refinement whereas \emph{TAR} uses only trace abstraction refinement.
% and in explicitly removing the traces by program transformation.
\end{enumerate}
%(1) compare TI with the VMCAI approach, which compares the effect of removing a set of trees rather than one tree and (2) with the Weng approach which differs in using polyhedral approximation rather than property-based abstraction (which is also abstract interpretation by the way), and in explicitly removing the traces by program transformation. In (1), you would expect improvement in solving power, but not necessarily in time. In (2) the results could either better or worse, both in time and the number of solved problems.
The results are summarized in Table~\ref{ch7:tbl:experiments}.
\paragraph{Implementation:}
Most of the tools in our tool-chain depicted in Figure \ref{ch7:fig:toolchain} are implemented in Ciao Prolog \cite{DBLP:journals/tplp/HermenegildoBCLMMP12} except the one for determinisation of FTA, which is implemented in Java following the algorithm described in \cite{DBLP:journals/corr/GallagherAK15}. Our tool-chain obtained by combining various tools using a \emph{shell script} serves as a proof of concept which is not optimised at all. For handling constraints, we use the Parma polyhedra library \cite{DBLP:journals/scp/BagnaraHZ08} and the Yices SMT solver \cite{Dutertre:cav2014} over \emph{linear real arithmetic}. The construction of tree interpolation uses constrained based algorithm presented in \cite{DBLP:journals/jsc/RybalchenkoS10} for computing interpolant of two formulas.
\paragraph{Description:} In Table~\ref{ch7:tbl:experiments}, {\it Program} represents a verification task, {\it Time (secs) RAHFT} and {\it Time (secs) RAHIT} - respectively represent the time in seconds taken by the the tool $\rahft$ and $\rahit$ respectively for solving a given task. Similarly, the number of \emph{abstraction-refinement} iteration needed in these cases to solve a task are represented by {\it \#Itr. RAHFT} and {\it \#Itr. RAHIT}. Similarly, {\it Time (secs) TAR} and {\it \#Itr. TAR} represent the time taken and the number of iterations needed by the tool \emph{TAR}. The experiments were run on a MAC computer running OS X on 2.3 GHz Intel core i7 processor and 8 GB memory.
\paragraph{Discussion:}
The comparison between $\rahft$ and $\rahit$ would reflect purely the role of \emph{interpolant tree automata} in Horn clause verification (Table~\ref{ch7:tbl:experiments}) since the only difference between them is the refinement part using \emph{(interpolant) tree automata}.
The results show that $\rahit$ is more effective in practice than its counterpart $\rahft$. This is justified by the number of tasks 61/68 solved by $\rahit$ using fewer iterations compared to $\rahft$, which only solves 56/68 tasks. This is due to the generalisation of a spurious counterexample during refinement, which also captures other infeasible traces. Since these traces can be removed in the same iteration, it (possibly) reduces the number of refinements, however the solving time goes up because of the cost of computing an interpolant automaton. It is not always the case that $\rahit$ takes less iterations for a task (for example \emph{Addition03 false-unreach}) than $\rahft$. This is because the restructuring of the program obtained as a result of removing a set of traces may or may not favour polyhedral approximation. It is still not clear to us how to produce a right restructuring which favours polyhedral approximation. $\rahit$ times out on \texttt{cggmp2005\_true-unreach} whereas $\rahft$ solves it in 5 iterations. We suspect that this is due to the cost of generating interpolant automata. We are not sure about the complexity of interpolant generation algorithm we used (the size of the formula generated was quite large with respect to the original program, magnitude not known) and there are several calls to the theorem prover to label each tree node with interpolants. So the bigger is the trace-tree, the longer it takes to compute the interpolant tree. In average, $\rahit$ needs 2.08 iterations and 11.40 seconds time to solve a task whereas $\rahft$ needs 2.32 iterations and 10.55 seconds.
%On the other hand, $\rahit$ or $\rahft$ is not directly comparable to \emph{TAR} since they differ in the techniques used, for example, $\rahit$ and $\rahft$ use \emph{abstract interpretation} but \emph{TAR} does not.
The use of \emph{interpolant tree automata} for trace generalisation and the tree automata based operations for trace-refinement are same in both $\rahit$ and \emph{TAR}. Since \emph{TAR} is not publicly available, we chose the same set of benchmarks used by \emph{TAR} for the purpose of comparison and presented the results (the results corresponding to \emph{TAR} are taken from \cite{WangJ2015}). The computer used in our experiments and in \emph{TAR} \cite{WangJ2015} have similar characteristics. $\rahit$ solves more than half of the problems only with \emph{abstract interpretation} over the domain of convex polyhedra without needing any refinement, which indicates its power. $\rahit$ solves 33/38 problems where as \emph{TAR} solves 28/38 problems. In average, $\rahit$ takes less time than \emph{TAR}. In many cases \emph{TAR} solves a task faster than $\rahit$, however it spends much longer time in some tasks.
%In average, $\rahit$ needs less than one iteration and 8.78 seconds to solve a task whereas \emph{TAR} needs almost 38 iterations and 9.52 seconds.
Our current constraint solver is over \emph{linear real arithmetic}. If we use it over \emph{linear integer arithmetic} then the results may differ.
We made some observation with the problems \emph{boustrophedon.c}, \emph{boustrophedon\_expansed.c} and \emph{cousot.correct} (which are supposed to be interpreted over integers). In them, if we replace strict inequalities ($>, <$) with non-strict inequalities ($\geq,\leq$) over integers (for example replace $X>Y$ with $X \geq Y+1$), then we can solve them only with \emph{abstract interpretation} without refinement which were not solved before the transformation using our solver. On the other hand, $\rahit$ times out for \emph{ mergesort.error } whereas \emph{TAR} solves it in a single iteration. This indicates that the choice of a spurious counterexample and the quality of interpolant generated from it for generalisation have some effects on verification.
\begin{table}
\resizebox{1.0\textwidth}{106mm}{
\begin{tabular}{|l|l|l|l|l|l|l|}
\hline
\textbf{Program} & \textbf{Time (secs) RAHFT} & \textbf{\#Itr. RAHFT} & \textbf{Time (secs) RAHIT} & \textbf{\#Itr. RAHIT} & \textbf{Time (secs) TAR \cite{WangJ2015}} & \textbf{\#Itr. TAR} \\ \hline
addition & 1 & 0 & 1 & 0 & 0.26 & 3 \\ \hline
anubhav.correct & 2 & 0 & 2 & 0 & 1.72 & 9 \\ \hline
bfprt & 1 & 0 & 1 & 0 & 0.43 & 6 \\ \hline
binarysearch & 2 & 0 & 2 & 0 & 0.36 & 5 \\ \hline
blast.correct & 5 & 1 & 11 & 1 & 8.93 & 65 \\ \hline
boustrophedon.c & TO & - & TO & - & 53.65 & 193 \\ \hline
boustrophedon\_expansed.c & TO & - & TO & - & 69.06 & 340 \\ \hline
buildheap & 44 & 9 & 44 & 9 & TO & - \\ \hline
copy1.error & 11 & 0 & 11 & 0 & 12.79 & 19 \\ \hline
countZero & 1 & 0 & 1 & 0 & TO & - \\ \hline
cousot.correct & TO & - & TO & - & TO & - \\ \hline
gopan.c & 3 & 0 & 3 & 0 & TO & - \\ \hline
halbwachs.c & TO & - & TO & - & TO & - \\ \hline
identity & 1 & 0 & 1 & 0 & 7.67 & 34 \\ \hline
inf1.error & 4 & 1 & 9 & 1 & 0.51 & 6 \\ \hline
inf6.correct & 5 & 1 & 5 & 1 & 1.96 & 33 \\ \hline
insdel.error & 2 & 0 & 2 & 0 & 0.17 & 1 \\ \hline
listcounter.correct & 1 & 0 & 1 & 0 & TO & ~ \\ \hline
listcounter.error & 9 & 1 & 9 & 1 & 0.21 & 1 \\ \hline
listreversal.correct & 4 & 0 & 4 & 0 & 35.79 & 149 \\ \hline
listreversal.error & 9 & 0 & 9 & 0 & 0.3 & 1 \\ \hline
loop.error & 3 & 0 & 3 & 0 & 3 & 3 \\ \hline
loop1.error & 8 & 0 & 8 & 0 & 10.87 & 19 \\ \hline
mc91.pl & 139 & 24 & 7 & 3 & 0.57 & 7 \\ \hline
merge & 2 & 0 & 2 & 0 & 0.86 & 10 \\ \hline
mergesort.error & TO & - & TO & - & 0.32 & 1 \\ \hline
palindrome & 2 & 0 & 2 & 0 & 0.61 & 6 \\ \hline
parity & 3 & 1 & 4 & 1 & 0.62 & 7 \\ \hline
rate\_limiter.c & 3 & 0 & 3 & 0 & 49.96 & 130 \\ \hline
remainder & 1 & 0 & 1 & 0 & 1.5 & 17 \\ \hline
running & 3 & 1 & 8 & 2 & 0.4 & 5 \\ \hline
scan.error & 3 & 0 & 3 & 0 & TO & - \\ \hline
string\_concat.error & 6 & 0 & 6 & 0 & TO & - \\ \hline
string\_concat1.error & TO & - & TO & - & TO & - \\ \hline
string\_copy.error & 3 & 0 & 3 & 0 & TO & - \\ \hline
substring.error & 5 & 0 & 5 & 0 & 0.55 & 1 \\ \hline
substring1.error & 15 & 0 & 15 & 0 & 2.84 & 5 \\ \hline
triple & 27 & 10 & 13 & 1 & 0.86 & 6 \\ \hline
\hline \textbf{average (over 38)} & ~ & ~ & \textbf{8.78} & \textbf{0.93} & \textbf{9.52} & \textbf{38.64} \\ \hline
\textbf{solved/total} & ~ & ~ & \textbf{33/38} & - & \textbf{28/38} & ~ \\ \hline
\hline Primes\_true-unreach & 16 & 4 & 4 & 1 & ~ & ~ \\ \hline
sum\_10x0\_false-unreach & 5 & 2 & 12 & 2 & ~ & ~ \\ \hline
afterrec\_false-unreach & 2 & 1 & 3 & 1 & ~ & ~ \\ \hline
id\_o3\_false-unreach & 6 & 3 & 7 & 3 & ~ & ~ \\ \hline
cggmp2005\_variant\_true-unreach & 2 & 1 & 3 & 1 & ~ & ~ \\ \hline
recHanoi01\_true-unreach & 8 & 3 & 10 & 3 & ~ & ~ \\ \hline
cggmp2005b\_true-unreach & 3 & 1 & 3 & 1 & ~ & ~ \\ \hline
gcd02\_true-unreach & 11 & 4 & 11 & 4 & ~ & ~ \\ \hline
diamond\_false-unreach & 3 & 1 & 3 & 1 & ~ & ~ \\ \hline
Addition03\_false-unreach & 6 & 2 & 13 & 5 & ~ & ~ \\ \hline
diamond\_true-unreach-call1 & 2 & 1 & 3 & 1 & ~ & ~ \\ \hline
id\_i5\_o5\_false-unreach & 19 & 8 & 12 & 5 & ~ & ~ \\ \hline
diamond\_true-unreach-call2 & 6 & 1 & 5 & 1 & ~ & ~ \\ \hline
cggmp2005\_true-unreach & 10 & 5 & TO & - & ~ & ~ \\ \hline
gsv2008\_true-unreach & 3 & 1 & 3 & 1 & ~ & ~ \\ \hline
Fibocci01\_true-unreach & 52 & 10 & 29 & 6 & ~ & ~ \\ \hline
id\_b3\_o2\_false-unreach & 5 & 2 & 3 & 1 & ~ & ~ \\ \hline
Ackermann02\_false-unreach & 68 & 17 & 25 & 7 & ~ & ~ \\ \hline
mcmillan2006\_true-unreach & 2 & 1 & 3 & 1 & ~ & ~ \\ \hline
ddlm2013\_true-unreach & TO & - & 17 & 7 & ~ & ~ \\ \hline
sum\_2x3\_false-unreach & 2 & 1 & 3 & 1 & ~ & ~ \\ \hline
fibo\_5\_true-unreach & TO & - & 77 & 7 & ~ & ~ \\ \hline
Addition01\_true-unreach & 6 & 2 & 5 & 2 & ~ & ~ \\ \hline
Ackermann04\_true-unreach & TO & - & 59 & 8 & ~ & ~ \\ \hline
Addition02\_false-unreach & 4 & 2 & 5 & 2 & ~ & ~ \\ \hline
id\_i10\_o10\_false-unreach & TO & - & 39 & 10 & ~ & ~ \\ \hline
gcd01\_true-unreach & 9 & 4 & 5 & 2 & ~ & ~ \\ \hline
id\_o10\_false-unreach & TO & - & 38 & 10 & ~ & ~ \\ \hline
gcnr2008\_false-unreach & 13 & 4 & 6 & 2 & ~ & ~ \\ \hline
Fibocci04\_false-unreach & TO & - & 91 & 11 & ~ & ~ \\ \hline
\hline \textbf{average (over 68)} & \textbf{10.55} & \textbf{2.32} & \textbf{11.40} & \textbf{2.08} & ~ & ~ \\ \hline
\textbf{solved/total} & \textbf{56/68} & ~ & \textbf{61/68} & ~ & ~ & ~ \\ \hline
\end{tabular}
}
\caption{Experiments on software verification problems. In the table ``TO'' means time out which is set for 300 seconds, ``-'' indicates the insignificance of the result.}
\label{ch7:tbl:experiments}
\end{table}
\section{Related work}
\label{ch7:rel}
Horn Clauses, as an intermediate language, have become a popular formalism for verification \cite{DBLP:conf/birthday/BjornerGMR15,DBLP:journals/corr/GallagherK14}, attracting both the logic programming and software verification communities \cite{DBLP:journals/corr/BjornerFRS14}. As a result of these, several verification techniques and tools have been developed for CHCs, among others, \cite{DBLP:conf/cav/GurfinkelKKN15,DBLP:conf/pldi/GrebenshchikovLPR12,DBLP:conf/pepm/KafleG15,DBLP:conf/tacas/AngelisFPP14,kafleG2015horn,DBLP:conf/cav/JaffarMNS12,DBLP:conf/fm/HojjatKGIKR12}. To the best of our knowledge, the use of automata based approach for \emph{abstraction-refinement} of Horn clauses is relatively new \cite{kafleG2015horn,WangJ2015}, though the original framework proposed for imperative programs goes back to \cite{DBLP:conf/sas/HeizmannHP09,DBLP:conf/popl/HeizmannHP10}.
The work described in \cite{kafleG2015horn} uses FTA based approach for refining \emph{abstract interpretation} over the domain of convex polyhedra \cite{Cousot-Halbwachs-78}, which is similar to \emph{trace abstraction} \cite{DBLP:conf/sas/HeizmannHP09,DBLP:conf/cav/HeizmannHP13, WangJ2015} with the following differences. In \cite{kafleG2015horn}, there is an interaction between state abstraction by \emph{abstract interpretation} \cite{DBLP:conf/popl/CousotC77} and trace abstraction by FTA but there is no generalisation of spurious counterexamples. On one hand, \cite{DBLP:conf/sas/HeizmannHP09,DBLP:conf/cav/HeizmannHP13, WangJ2015} use \emph{trace-abstraction} with the generalisation of spurious counterexamples using \emph{interpolant automata} and may diverge from the solution due to the lack of right generalisation. On the other hand, \emph{abstract interpretation} \cite{DBLP:conf/popl/CousotC77} is one of the most promising techniques for verification which is scalable but suffers from \emph{false alarms}. When combined with refinement \emph{false alarms} can be minimized. Our current work takes the best of both of these approaches.
% Our approach does not need nested string automaton \cite{DBLP:conf/sas/HeizmannHP09,DBLP:conf/popl/HeizmannHP10} construction for representing program with recursive procedures which give rise to non-linear Horn clauses; but captures them using FTA. In the same direction, Cassez et al. \cite{DBLP:conf/fsttcs/CassezMB14} used summary-based modular trace abstraction method for verifying programs with procedures.
%Horn Clauses offer several features that make them convenient for verification \cite{DBLP:conf/birthday/BjornerGMR15}. Recently there is a growing interest in CHC verification from both the logic programming and software verification communities, and several verification techniques and tools have been developed for CHC \cite{DBLP:conf/cav/GurfinkelKKN15,DBLP:conf/pldi/GrebenshchikovLPR12,DBLP:conf/pepm/KafleG15,DBLP:conf/vmcai/KafleG15,DBLP:conf/cav/JaffarMNS12,DBLP:conf/fm/HojjatKGIKR12}. Roughly speaking, techniques for solving a set of CHCs involve in generalising an under-approximation (bounded model checking \cite{DBLP:journals/ac/BiereCCSZ03}, property-directed reachability \cite{DBLP:conf/fmcad/BradleyM07}, counterexample guided abstraction refinement \cite{DBLP:conf/cav/ClarkeGJLV00}) or over-approximation (abstract interpretation\cite{DBLP:conf/popl/CousotC77}, program specialisation \cite{Leuschel-Massart-LOPSTR99,Peralta-Gallagher-Saglam-SAS98,DBLP:journals/scp/AngelisFPP14}) or the combination of both. Techniques of over-approximation suffers from \emph{false alarms} where as techniques based on under-approximation may not \emph{converge}. We ask readers to refer to \cite{DBLP:conf/birthday/BjornerGMR15} for more details.
%one of the promising techniques for Horn clause verification is by AI, which is scalable but suffers from \emph{false alarms}. There are some works on refining AI with progress guarantee, for example, \cite{DBLP:journals/ipl/GulavaniCNR10,kafleG2015horn}.
%Since any derivations of Horn clauses can be captured by an finite tree automata (FTA), there is no need of nested string automaton \cite{DBLP:conf/sas/HeizmannHP09,DBLP:conf/popl/HeizmannHP10} for representing program with recursive procedures which give rise to non-linear Horn clauses.
\section{Conclusion}
This paper brings together \emph{abstract interpretation} over the domain of convex polyhedra and \emph{interpolant tree automata} in an \emph{abstraction-refinement} scheme for Horn clause verification and combines them in a new way. Experimental results on a set of software verification benchmarks using this scheme demonstrated their usefulness in practice; showing some slight improvements over the previous approaches. In the future, we plan to evaluate its effectiveness in a larger set of benchmarks, compare our approach with other similar approaches and improve the implementation aspects of our tool. Further study is needed to find a suitable combination of abstract interpretation and interpolation based techniques, based on a deeper understanding of the interaction among interpolation, trace elimination and abstract interpretation.
% Further study is needed to find a suitable combination between trace abstraction by abstract interpretation and trace generalisation using interpolant automaton.
\begin{thebibliography}{10}
\providecommand{\bibitemdeclare}[2]{}
\providecommand{\surnamestart}{}
\providecommand{\surnameend}{}
\providecommand{\urlprefix}{Available at }
\providecommand{\url}[1]{\texttt{#1}}
\providecommand{\href}[2]{\texttt{#2}}
\providecommand{\urlalt}[2]{\href{#1}{#2}}
\providecommand{\doi}[1]{doi:\urlalt{http://dx.doi.org/#1}{#1}}
\providecommand{\bibinfo}[2]{#2}
\bibitemdeclare{article}{DBLP:journals/scp/BagnaraHZ08}
\bibitem{DBLP:journals/scp/BagnaraHZ08}
\bibinfo{author}{Roberto \surnamestart Bagnara\surnameend},
\bibinfo{author}{Patricia~M. \surnamestart Hill\surnameend} \&
\bibinfo{author}{Enea \surnamestart Zaffanella\surnameend}
(\bibinfo{year}{2008}): \emph{\bibinfo{title}{The Parma Polyhedra Library:
Toward a complete set of numerical abstractions for the analysis and
verification of hardware and software systems}}.
\newblock {\sl \bibinfo{journal}{Sci. Comput. Program.}}
\bibinfo{volume}{72}(\bibinfo{number}{1-2}), pp. \bibinfo{pages}{3--21},
\doi{10.1016/j.scico.2007.08.001}.
\bibitemdeclare{proceedings}{DBLP:conf/tacas/2015}
\bibitem{DBLP:conf/tacas/2015}
\bibinfo{editor}{Christel \surnamestart Baier\surnameend} \&
\bibinfo{editor}{Cesare \surnamestart Tinelli\surnameend}, editors
(\bibinfo{year}{2015}): \emph{\bibinfo{title}{{TACAS} . Proceedings}}. {\sl
\bibinfo{series}{LNCS}} \bibinfo{volume}{9035},
\bibinfo{publisher}{Springer}, \doi{10.1007/978-3-662-46681-0}.
\bibitemdeclare{inproceedings}{DBLP:conf/tacas/000115}
\bibitem{DBLP:conf/tacas/000115}
\bibinfo{author}{Dirk \surnamestart Beyer\surnameend} (\bibinfo{year}{2015}):
\emph{\bibinfo{title}{Software Verification and Verifiable Witnesses -
(Report on {SV-COMP} 2015)}}.
\newblock In \bibinfo{editor}{Baier} \& \bibinfo{editor}{Tinelli}
\cite{DBLP:conf/tacas/2015}, pp. \bibinfo{pages}{401--416},
\doi{10.1007/978-3-662-46681-0\_31}.
\bibitemdeclare{proceedings}{DBLP:journals/corr/BjornerFRS14}
\bibitem{DBLP:journals/corr/BjornerFRS14}
\bibinfo{editor}{Nikolaj \surnamestart Bj{\o}rner\surnameend},
\bibinfo{editor}{Fabio \surnamestart Fioravanti\surnameend},
\bibinfo{editor}{Andrey \surnamestart Rybalchenko\surnameend} \&
\bibinfo{editor}{Valerio \surnamestart Senni\surnameend}, editors
(\bibinfo{year}{2014}): \emph{\bibinfo{title}{Proceedings First Workshop on
{H}orn Clauses for Verification and Synthesis, {HCVS} 2014, Vienna, Austria,
17 July 2014}}. {\sl \bibinfo{series}{{EPTCS}}} \bibinfo{volume}{169},
\doi{10.4204/EPTCS.169}.
\bibitemdeclare{inproceedings}{DBLP:conf/birthday/BjornerGMR15}
\bibitem{DBLP:conf/birthday/BjornerGMR15}
\bibinfo{author}{Nikolaj \surnamestart Bj{\o}rner\surnameend},
\bibinfo{author}{Arie \surnamestart Gurfinkel\surnameend},
\bibinfo{author}{Kenneth~L. \surnamestart McMillan\surnameend} \&
\bibinfo{author}{Andrey \surnamestart Rybalchenko\surnameend}
(\bibinfo{year}{2015}): \emph{\bibinfo{title}{{H}orn Clause Solvers for
Program Verification}}.
\newblock In \bibinfo{editor}{Lev~D. \surnamestart Beklemishev\surnameend},
\bibinfo{editor}{Andreas \surnamestart Blass\surnameend},
\bibinfo{editor}{Nachum \surnamestart Dershowitz\surnameend},
\bibinfo{editor}{Bernd \surnamestart Finkbeiner\surnameend} \&
\bibinfo{editor}{Wolfram \surnamestart Schulte\surnameend}, editors: {\sl
\bibinfo{booktitle}{Fields of Logic and Computation {II} - Essays Dedicated
to Yuri Gurevich on the Occasion of His 75th Birthday}}, {\sl
\bibinfo{series}{{LNCS}}} \bibinfo{volume}{9300},
\bibinfo{publisher}{Springer}, pp. \bibinfo{pages}{24--51},
\doi{10.1007/978-3-319-23534-9\_2}.
\bibitemdeclare{inproceedings}{DBLP:conf/sas/BjornerMR13}
\bibitem{DBLP:conf/sas/BjornerMR13}
\bibinfo{author}{Nikolaj \surnamestart Bj{\o}rner\surnameend},
\bibinfo{author}{Kenneth~L. \surnamestart McMillan\surnameend} \&
\bibinfo{author}{Andrey \surnamestart Rybalchenko\surnameend}
(\bibinfo{year}{2013}): \emph{\bibinfo{title}{On Solving Universally
Quantified {H}orn Clauses}}.
\newblock In \bibinfo{editor}{Francesco \surnamestart Logozzo\surnameend} \&
\bibinfo{editor}{Manuel \surnamestart F{\"a}hndrich\surnameend}, editors:
{\sl \bibinfo{booktitle}{SAS}}, {\sl \bibinfo{series}{LNCS}}
\bibinfo{volume}{7935}, \bibinfo{publisher}{Springer}, pp.
\bibinfo{pages}{105--125}.
\newblock \urlprefix\url{http://dx.doi.org/10.1007/978-3-642-38856-9_8}.
\bibitemdeclare{misc}{Comon}
\bibitem{Comon}
\bibinfo{author}{H.~\surnamestart Comon\surnameend},
\bibinfo{author}{M.~\surnamestart Dauchet\surnameend},
\bibinfo{author}{R.~\surnamestart Gilleron\surnameend},
\bibinfo{author}{C.~\surnamestart L\"oding\surnameend},
\bibinfo{author}{F.~\surnamestart Jacquemard\surnameend},
\bibinfo{author}{D.~\surnamestart Lugiez\surnameend},
\bibinfo{author}{S.~\surnamestart Tison\surnameend} \&
\bibinfo{author}{M.~\surnamestart Tommasi\surnameend} (\bibinfo{year}{2007}):
\emph{\bibinfo{title}{Tree Automata Techniques and Applications}}.
\newblock \bibinfo{howpublished}{Available on:
\url{http://www.grappa.univ-lille3.fr/tata}}.
\newblock \bibinfo{note}{Release October, 12th 2007}.
\bibitemdeclare{inproceedings}{Cousot-Halbwachs-78}
\bibitem{Cousot-Halbwachs-78}
\bibinfo{author}{P.~\surnamestart Cousot\surnameend} \&
\bibinfo{author}{N.~\surnamestart Halbwachs\surnameend}
(\bibinfo{year}{{1978}}): \emph{\bibinfo{title}{Automatic Discovery of Linear
Restraints Among Variables of a Program}}.
\newblock In: {\sl \bibinfo{booktitle}{Proceedings of the 5th Annual ACM
Symposium on Principles of Programming Languages}}, pp.
\bibinfo{pages}{84--96}, \doi{10.1145/512760.512770}.
\bibitemdeclare{inproceedings}{DBLP:conf/popl/CousotC77}
\bibitem{DBLP:conf/popl/CousotC77}
\bibinfo{author}{Patrick \surnamestart Cousot\surnameend} \&
\bibinfo{author}{Radhia \surnamestart Cousot\surnameend}
(\bibinfo{year}{1977}): \emph{\bibinfo{title}{Abstract Interpretation: A
Unified Lattice Model for Static Analysis of Programs by Construction or
Approximation of Fixpoints}}.
\newblock In \bibinfo{editor}{Robert~M. \surnamestart Graham\surnameend},
\bibinfo{editor}{Michael~A. \surnamestart Harrison\surnameend} \&
\bibinfo{editor}{Ravi \surnamestart Sethi\surnameend}, editors: {\sl
\bibinfo{booktitle}{POPL}}, \bibinfo{publisher}{ACM}, pp.
\bibinfo{pages}{238--252}.
\newblock \urlprefix\url{http://doi.acm.org/10.1145/512950.512973}.
\bibitemdeclare{article}{DBLP:journals/jsyml/Craig57}
\bibitem{DBLP:journals/jsyml/Craig57}
\bibinfo{author}{William \surnamestart Craig\surnameend}
(\bibinfo{year}{1957}): \emph{\bibinfo{title}{Linear Reasoning. {A} New Form
of the Herbrand-Gentzen Theorem}}.
\newblock {\sl \bibinfo{journal}{J. Symb. Log.}}
\bibinfo{volume}{22}(\bibinfo{number}{3}), pp. \bibinfo{pages}{250--268},
\doi{10.2307/2963593}.
\bibitemdeclare{inproceedings}{DBLP:conf/tacas/AngelisFPP14}
\bibitem{DBLP:conf/tacas/AngelisFPP14}
\bibinfo{author}{Emanuele \surnamestart De~Angelis\surnameend},
\bibinfo{author}{Fabio \surnamestart Fioravanti\surnameend},
\bibinfo{author}{Alberto \surnamestart Pettorossi\surnameend} \&
\bibinfo{author}{Maurizio \surnamestart Proietti\surnameend}
(\bibinfo{year}{2014}): \emph{\bibinfo{title}{VeriMAP: A Tool for Verifying
Programs through Transformations}}.
\newblock In \bibinfo{editor}{Erika \surnamestart {\'A}brah{\'a}m\surnameend}
\& \bibinfo{editor}{Klaus \surnamestart Havelund\surnameend}, editors: {\sl
\bibinfo{booktitle}{TACAS}}, {\sl \bibinfo{series}{LNCS}}
\bibinfo{volume}{8413}, \bibinfo{publisher}{Springer}, pp.
\bibinfo{pages}{568--574}.
\newblock \urlprefix\url{http://dx.doi.org/10.1007/978-3-642-54862-8_47}.
\bibitemdeclare{inproceedings}{Dutertre:cav2014}
\bibitem{Dutertre:cav2014}
\bibinfo{author}{Bruno \surnamestart Dutertre\surnameend}
(\bibinfo{year}{2014}): \emph{\bibinfo{title}{Yices 2.2}}.
\newblock In \bibinfo{editor}{Armin \surnamestart Biere\surnameend} \&
\bibinfo{editor}{Roderick \surnamestart Bloem\surnameend}, editors: {\sl
\bibinfo{booktitle}{Computer-Aided Verification (CAV'2014)}}, {\sl
\bibinfo{series}{Lecture Notes in Computer Science}} \bibinfo{volume}{8559},
\bibinfo{publisher}{Springer}, pp. \bibinfo{pages}{737--744},
\doi{10.1007/978-3-319-08867-9\_49}.
\bibitemdeclare{inproceedings}{Gallagher-Lafave-Dagstuhl}
\bibitem{Gallagher-Lafave-Dagstuhl}
\bibinfo{author}{J.~P. \surnamestart Gallagher\surnameend} \&
\bibinfo{author}{L.~\surnamestart Lafave\surnameend} (\bibinfo{year}{1996}):
\emph{\bibinfo{title}{Regular Approximation of Computation Paths in Logic and
Functional Languages}}.
\newblock In \bibinfo{editor}{O.~\surnamestart Danvy\surnameend},
\bibinfo{editor}{R.~\surnamestart Gl{\"u}ck\surnameend} \&
\bibinfo{editor}{P.~\surnamestart Thiemann\surnameend}, editors: {\sl
\bibinfo{booktitle}{Partial Evaluation}}, {\sl
\bibinfo{series}{Springer-Verlag {LNCS}}} \bibinfo{volume}{1110}, pp.
\bibinfo{pages}{115--136}.
\newblock \urlprefix\url{http://dx.doi.org/10.1007/3-540-61580-6\_7}.
\bibitemdeclare{article}{DBLP:journals/corr/GallagherAK15}
\bibitem{DBLP:journals/corr/GallagherAK15}
\bibinfo{author}{John~P. \surnamestart Gallagher\surnameend},
\bibinfo{author}{Mai \surnamestart Ajspur\surnameend} \&
\bibinfo{author}{Bishoksan \surnamestart Kafle\surnameend}
(\bibinfo{year}{2015}): \emph{\bibinfo{title}{An Optimised Algorithm for
Determinisation and Completion of Finite Tree Automata}}.
\newblock {\sl \bibinfo{journal}{CoRR}} \bibinfo{volume}{abs/1511.03595}.
\newblock \urlprefix\url{http://arxiv.org/abs/1511.03595}.
\bibitemdeclare{article}{DBLP:journals/corr/GallagherK14}
\bibitem{DBLP:journals/corr/GallagherK14}
\bibinfo{author}{John~P. \surnamestart Gallagher\surnameend} \&
\bibinfo{author}{Bishoksan \surnamestart Kafle\surnameend}
(\bibinfo{year}{2014}): \emph{\bibinfo{title}{Analysis and Transformation
Tools for Constrained {H}orn Clause Verification}}.
\newblock {\sl \bibinfo{journal}{{TPLP}}}
\bibinfo{volume}{14}(\bibinfo{number}{4-5 (additional materials in online
edition)}), pp. \bibinfo{pages}{90--101}.
\newblock
\urlprefix\url{http://journals.cambridge.org/action/displaySuppMaterial?cupCode=1&type=4&jid=TLP&volumeId=14&issueId=4-5&aid=9303163}.
\bibitemdeclare{inproceedings}{DBLP:conf/pldi/GrebenshchikovLPR12}
\bibitem{DBLP:conf/pldi/GrebenshchikovLPR12}
\bibinfo{author}{Sergey \surnamestart Grebenshchikov\surnameend},
\bibinfo{author}{Nuno~P. \surnamestart Lopes\surnameend},
\bibinfo{author}{Corneliu \surnamestart Popeea\surnameend} \&
\bibinfo{author}{Andrey \surnamestart Rybalchenko\surnameend}
(\bibinfo{year}{2012}): \emph{\bibinfo{title}{Synthesizing software verifiers
from proof rules}}.
\newblock In \bibinfo{editor}{Jan \surnamestart Vitek\surnameend},
\bibinfo{editor}{Haibo \surnamestart Lin\surnameend} \&
\bibinfo{editor}{Frank \surnamestart Tip\surnameend}, editors: {\sl
\bibinfo{booktitle}{{ACM} {SIGPLAN} Conference on Programming Language Design
and Implementation, {PLDI} '12, Beijing, China - June 11 - 16, 2012}},
\bibinfo{publisher}{{ACM}}, pp. \bibinfo{pages}{405--416},
\doi{10.1145/2254064.2254112}.
\newblock \urlprefix\url{http://dl.acm.org/citation.cfm?id=2254064}.
\bibitemdeclare{inproceedings}{DBLP:conf/cav/GurfinkelKKN15}
\bibitem{DBLP:conf/cav/GurfinkelKKN15}
\bibinfo{author}{Arie \surnamestart Gurfinkel\surnameend},
\bibinfo{author}{Temesghen \surnamestart Kahsai\surnameend},
\bibinfo{author}{Anvesh \surnamestart Komuravelli\surnameend} \&
\bibinfo{author}{Jorge~A. \surnamestart Navas\surnameend}
(\bibinfo{year}{2015}): \emph{\bibinfo{title}{The Sea{H}orn Verification
Framework}}.
\newblock In \bibinfo{editor}{Daniel \surnamestart Kroening\surnameend} \&
\bibinfo{editor}{Corina~S. \surnamestart Pasareanu\surnameend}, editors: {\sl
\bibinfo{booktitle}{{CAV} , Proceedings, Part {I}}}, {\sl
\bibinfo{series}{{LNCS}}} \bibinfo{volume}{9206},
\bibinfo{publisher}{Springer}, pp. \bibinfo{pages}{343--361},
\doi{10.1007/978-3-319-21690-4\_20}.
\bibitemdeclare{inproceedings}{DBLP:conf/tacas/GurfinkelKN15}
\bibitem{DBLP:conf/tacas/GurfinkelKN15}
\bibinfo{author}{Arie \surnamestart Gurfinkel\surnameend},
\bibinfo{author}{Temesghen \surnamestart Kahsai\surnameend} \&
\bibinfo{author}{Jorge~A. \surnamestart Navas\surnameend}
(\bibinfo{year}{2015}): \emph{\bibinfo{title}{Sea{H}orn: {A} Framework for
Verifying {C} Programs (Competition Contribution)}}.
\newblock In \bibinfo{editor}{Baier} \& \bibinfo{editor}{Tinelli}
\cite{DBLP:conf/tacas/2015}, pp. \bibinfo{pages}{447--450},
\doi{10.1007/978-3-662-46681-0\_41}.
\bibitemdeclare{inproceedings}{DBLP:conf/sas/HeizmannHP09}
\bibitem{DBLP:conf/sas/HeizmannHP09}
\bibinfo{author}{Matthias \surnamestart Heizmann\surnameend},
\bibinfo{author}{Jochen \surnamestart Hoenicke\surnameend} \&
\bibinfo{author}{Andreas \surnamestart Podelski\surnameend}
(\bibinfo{year}{2009}): \emph{\bibinfo{title}{Refinement of Trace
Abstraction.}}
\newblock In \bibinfo{editor}{Jens \surnamestart Palsberg\surnameend} \&
\bibinfo{editor}{Zhendong \surnamestart Su\surnameend}, editors: {\sl
\bibinfo{booktitle}{Static Analysis, 16th International Symposium, {SAS}
2009}}, {\sl \bibinfo{series}{LNCS}} \bibinfo{volume}{5673},
\bibinfo{publisher}{Springer}, pp. \bibinfo{pages}{69--85},
\doi{10.1007/978-3-642-03237-0\_7}.
\bibitemdeclare{inproceedings}{DBLP:conf/popl/HeizmannHP10}
\bibitem{DBLP:conf/popl/HeizmannHP10}
\bibinfo{author}{Matthias \surnamestart Heizmann\surnameend},
\bibinfo{author}{Jochen \surnamestart Hoenicke\surnameend} \&
\bibinfo{author}{Andreas \surnamestart Podelski\surnameend}
(\bibinfo{year}{2010}): \emph{\bibinfo{title}{Nested interpolants}}.
\newblock In \bibinfo{editor}{Manuel~V. \surnamestart Hermenegildo\surnameend}
\& \bibinfo{editor}{Jens \surnamestart Palsberg\surnameend}, editors: {\sl
\bibinfo{booktitle}{Proceedings of the 37th {ACM} {SIGPLAN-SIGACT} Symposium
on Principles of Programming Languages, {POPL} 2010, Madrid, Spain, January
17-23, 2010}}, \bibinfo{publisher}{{ACM}}, pp. \bibinfo{pages}{471--482},
\doi{10.1145/1706299.1706353}.
\newblock \urlprefix\url{http://dl.acm.org/citation.cfm?id=1706299}.
\bibitemdeclare{inproceedings}{DBLP:conf/cav/HeizmannHP13}
\bibitem{DBLP:conf/cav/HeizmannHP13}
\bibinfo{author}{Matthias \surnamestart Heizmann\surnameend},
\bibinfo{author}{Jochen \surnamestart Hoenicke\surnameend} \&
\bibinfo{author}{Andreas \surnamestart Podelski\surnameend}
(\bibinfo{year}{2013}): \emph{\bibinfo{title}{Software Model Checking for
People Who Love Automata}}.
\newblock In \bibinfo{editor}{Sharygina} \& \bibinfo{editor}{Veith}
\cite{DBLP:conf/cav/2013}, pp. \bibinfo{pages}{36--52},
\doi{10.1007/978-3-642-39799-8\_2}.
\bibitemdeclare{article}{DBLP:journals/tplp/HermenegildoBCLMMP12}
\bibitem{DBLP:journals/tplp/HermenegildoBCLMMP12}
\bibinfo{author}{Manuel~V. \surnamestart Hermenegildo\surnameend},
\bibinfo{author}{Francisco \surnamestart Bueno\surnameend},
\bibinfo{author}{Manuel \surnamestart Carro\surnameend},
\bibinfo{author}{Pedro \surnamestart L{\'{o}}pez{-}Garc{\'{\i}}a\surnameend},
\bibinfo{author}{Edison \surnamestart Mera\surnameend},
\bibinfo{author}{Jos{\'{e}}~F. \surnamestart Morales\surnameend} \&
\bibinfo{author}{Germ{\'{a}}n \surnamestart Puebla\surnameend}
(\bibinfo{year}{2012}): \emph{\bibinfo{title}{An overview of Ciao and its
design philosophy}}.
\newblock {\sl \bibinfo{journal}{{TPLP}}}
\bibinfo{volume}{12}(\bibinfo{number}{1-2}), pp. \bibinfo{pages}{219--252},
\doi{10.1017/S1471068411000457}.
\bibitemdeclare{inproceedings}{DBLP:conf/fm/HojjatKGIKR12}
\bibitem{DBLP:conf/fm/HojjatKGIKR12}
\bibinfo{author}{Hossein \surnamestart Hojjat\surnameend},
\bibinfo{author}{Filip \surnamestart Konecn{\'{y}}\surnameend},
\bibinfo{author}{Florent \surnamestart Garnier\surnameend},
\bibinfo{author}{Radu \surnamestart Iosif\surnameend},
\bibinfo{author}{Viktor \surnamestart Kuncak\surnameend} \&
\bibinfo{author}{Philipp \surnamestart R{\"{u}}mmer\surnameend}
(\bibinfo{year}{2012}): \emph{\bibinfo{title}{A Verification Toolkit for
Numerical Transition Systems - Tool Paper}}.
\newblock In \bibinfo{editor}{Dimitra \surnamestart Giannakopoulou\surnameend}
\& \bibinfo{editor}{Dominique \surnamestart M{\'{e}}ry\surnameend}, editors:
{\sl \bibinfo{booktitle}{{FM} 2012: Formal Methods - 18th International
Symposium, Paris, France, August 27-31, 2012. Proceedings}}, {\sl
\bibinfo{series}{{LNCS}}} \bibinfo{volume}{7436},
\bibinfo{publisher}{Springer}, pp. \bibinfo{pages}{247--251},
\doi{10.1007/978-3-642-32759-9\_21}.
\bibitemdeclare{inproceedings}{DBLP:conf/cav/JaffarMNS12}
\bibitem{DBLP:conf/cav/JaffarMNS12}
\bibinfo{author}{Joxan \surnamestart Jaffar\surnameend},
\bibinfo{author}{Vijayaraghavan \surnamestart Murali\surnameend},
\bibinfo{author}{Jorge~A. \surnamestart Navas\surnameend} \&
\bibinfo{author}{Andrew~E. \surnamestart Santosa\surnameend}
(\bibinfo{year}{2012}): \emph{\bibinfo{title}{TRACER: A Symbolic Execution
Tool for Verification}}.
\newblock In \bibinfo{editor}{P.~\surnamestart Madhusudan\surnameend} \&
\bibinfo{editor}{Sanjit~A. \surnamestart Seshia\surnameend}, editors: {\sl
\bibinfo{booktitle}{CAV}}, {\sl \bibinfo{series}{LNCS}}
\bibinfo{volume}{7358}, \bibinfo{publisher}{Springer}, pp.
\bibinfo{pages}{758--766}.
\newblock \urlprefix\url{http://dx.doi.org/10.1007/978-3-642-31424-7_61}.
\bibitemdeclare{inproceedings}{DBLP:conf/tacas/JhalaM06}
\bibitem{DBLP:conf/tacas/JhalaM06}
\bibinfo{author}{Ranjit \surnamestart Jhala\surnameend} \&
\bibinfo{author}{Kenneth~L. \surnamestart McMillan\surnameend}
(\bibinfo{year}{2006}): \emph{\bibinfo{title}{A Practical and Complete
Approach to Predicate Refinement}}.
\newblock In \bibinfo{editor}{Holger \surnamestart Hermanns\surnameend} \&
\bibinfo{editor}{Jens \surnamestart Palsberg\surnameend}, editors: {\sl
\bibinfo{booktitle}{TACAS}}, {\sl \bibinfo{series}{LNCS}}
\bibinfo{volume}{3920}, \bibinfo{publisher}{Springer}, pp.
\bibinfo{pages}{459--473}.
\newblock \urlprefix\url{http://dx.doi.org/10.1007/11691372_33}.
\bibitemdeclare{inproceedings}{DBLP:conf/pepm/KafleG15}
\bibitem{DBLP:conf/pepm/KafleG15}
\bibinfo{author}{Bishoksan \surnamestart Kafle\surnameend} \&
\bibinfo{author}{John~P. \surnamestart Gallagher\surnameend}
(\bibinfo{year}{2015}): \emph{\bibinfo{title}{Constraint Specialisation in
{H}orn Clause Verification}}.
\newblock In \bibinfo{editor}{Kenichi \surnamestart Asai\surnameend} \&
\bibinfo{editor}{Kostis \surnamestart Sagonas\surnameend}, editors: {\sl
\bibinfo{booktitle}{Proceedings of the 2015 Workshop on Partial Evaluation
and Program Manipulation, PEPM, Mumbai, India, January 15-17, 2015}},
\bibinfo{publisher}{{ACM}}, pp. \bibinfo{pages}{85--90},
\doi{10.1145/2678015.2682544}.
\newblock \urlprefix\url{http://dl.acm.org/citation.cfm?id=2678015}.
\bibitemdeclare{article}{kafleG2015horn}
\bibitem{kafleG2015horn}
\bibinfo{author}{Bishoksan \surnamestart Kafle\surnameend} \&
\bibinfo{author}{John~P. \surnamestart Gallagher\surnameend}
(\bibinfo{year}{2015}): \emph{\bibinfo{title}{{H}orn clause verification with
convex polyhedral abstraction and tree automata-based refinement}}.
\newblock {\sl \bibinfo{journal}{Computer Languages, Systems \& Structures}},
\doi{10.1016/j.cl.2015.11.001}.
\bibitemdeclare{techreport}{McmillanR2013}
\bibitem{McmillanR2013}
\bibinfo{author}{Kenneth~L. \surnamestart McMillan\surnameend} \&
\bibinfo{author}{Andrey \surnamestart Rybalchenko\surnameend}
(\bibinfo{year}{2013}): \emph{\bibinfo{title}{Solving Constrained {H}orn
Clauses using Interpolation}}.
\newblock \bibinfo{type}{Technical Report}, \bibinfo{institution}{Microsoft
Research}.
\bibitemdeclare{inproceedings}{DBLP:conf/cav/RummerHK13}
\bibitem{DBLP:conf/cav/RummerHK13}
\bibinfo{author}{Philipp \surnamestart R{\"u}mmer\surnameend},
\bibinfo{author}{Hossein \surnamestart Hojjat\surnameend} \&
\bibinfo{author}{Viktor \surnamestart Kuncak\surnameend}
(\bibinfo{year}{2013}): \emph{\bibinfo{title}{Disjunctive Interpolants for
{H}orn-Clause Verification}}.
\newblock In \bibinfo{editor}{Sharygina} \& \bibinfo{editor}{Veith}
\cite{DBLP:conf/cav/2013}, pp. \bibinfo{pages}{347--363},
\doi{10.1007/978-3-642-39799-8\_24}.
\bibitemdeclare{article}{DBLP:journals/jsc/RybalchenkoS10}
\bibitem{DBLP:journals/jsc/RybalchenkoS10}
\bibinfo{author}{Andrey \surnamestart Rybalchenko\surnameend} \&
\bibinfo{author}{Viorica \surnamestart Sofronie-Stokkermans\surnameend}
(\bibinfo{year}{2010}): \emph{\bibinfo{title}{Constraint solving for
interpolation}}.
\newblock {\sl \bibinfo{journal}{J. Symb. Comput.}}
\bibinfo{volume}{45}(\bibinfo{number}{11}), pp. \bibinfo{pages}{1212--1233}.
\newblock \urlprefix\url{http://dx.doi.org/10.1016/j.jsc.2010.06.005}.
\bibitemdeclare{proceedings}{DBLP:conf/cav/2013}
\bibitem{DBLP:conf/cav/2013}
\bibinfo{editor}{Natasha \surnamestart Sharygina\surnameend} \&
\bibinfo{editor}{Helmut \surnamestart Veith\surnameend}, editors
(\bibinfo{year}{2013}): \emph{\bibinfo{title}{Computer Aided Verification -
25th International Conference, {CAV} 2013, Saint Petersburg, Russia, July
13-19, 2013. Proceedings}}. {\sl \bibinfo{series}{{LNCS}}}
\bibinfo{volume}{8044}, \bibinfo{publisher}{Springer},
\doi{10.1007/978-3-642-39799-8}.
\bibitemdeclare{inproceedings}{Stark89}
\bibitem{Stark89}
\bibinfo{author}{Robert~F. \surnamestart St{\"a}rk\surnameend}
(\bibinfo{year}{1989}): \emph{\bibinfo{title}{A Direct Proof for the
Completeness of {SLD}-Resolution}}.
\newblock In \bibinfo{editor}{Egon \surnamestart B{\"o}rger\surnameend},
\bibinfo{editor}{Hans~Kleine \surnamestart B{\"u}ning\surnameend} \&
\bibinfo{editor}{Michael~M. \surnamestart Richter\surnameend}, editors: {\sl
\bibinfo{booktitle}{CSL '89, 3rd Workshop on Computer Science Logic,
Kaiserslautern, Germany, October 2-6, 1989, Proceedings}}, {\sl
\bibinfo{series}{LNCS}} \bibinfo{volume}{440}, \bibinfo{publisher}{Springer},
pp. \bibinfo{pages}{382--383}.
\bibitemdeclare{techreport}{WangJ2015}
\bibitem{WangJ2015}
\bibinfo{author}{Weifeng \surnamestart Wang\surnameend} \&
\bibinfo{author}{Li~\surnamestart Jiao\surnameend} (\bibinfo{year}{2015}):
\emph{\bibinfo{title}{Trace abstraction refinement for solving {H}orn
clauses}}.
\newblock \bibinfo{type}{Technical Report} \bibinfo{number}{ISCAS-SKLCS-15-19},
\bibinfo{institution}{State Key Laboratory of Computer Science, Institute of
Software, Chinese Academy of Sciences}.
\newblock \bibinfo{note}{Available on:
\url{http://lcs.ios.ac.cn/~wangwf/TechReportISCAS-SKLCS-15-19.pdf}}.
\end{thebibliography}