Rapport Avancement Final
Projet CASSIS LORIA INRIA Lorraine
Novembre 2006
Composition de l'équipe
Silvio Ranise, CR INRIA
Christophe Ringeissen, CR INRIA
Below, I give a summary of the research performed within GECCOO and
use the section numbering of the previous report (mis-parcour). The
bibliographic citations I use below refer to the one in the web page
containing the publications (publis-geccoo.html).
Section 2.1.2
--------------
haRVey has been designed as the reasoning component of verification
tools requiring to discharge proof obligations such as verification
condition generator for program verification (e.g., Jack and Krakatoa)
or software model checkers (SLAM, Blast, etc).
The system has two incarnations: haRVey-FOL and haRVey-SAT. The
former integrates Boolean solvers with an equational theorem prover
and a decision procedure for Linear Arithmetic along the lines of
[34]. The latter integrates a SAT solver with a combination (a la
Nelson-Oppen) of decision procedures for the theory of uninterpreted
function symbols and Linear Arithmetics with techniques to instantiate
quantifiers and lambda-expressions. Furthermore, haRVey-SAT can
produce proofs which can independently checked by the proof assistant
Isabelle.
While haRVey-FOL offers a high-degree of automation for a variety of
theories, haRVey-SAT is usually faster on problems with simple
background theories and ensures a high-degree of certification by its
proof-checking capability. Along the lines of [34], our current work
aims at merging the two incarnations to build a system retaining the
flexibility and automatic reasoning support for expressive theories of
haRVey-FOL while providing better performances with simple theories as
haRVey-SAT.
Section 2.4
------------
Reasoning about container data structures
----------------------------------------------------------------
Recent work has put forward the use of a theory of sets with
cardinality (SC) for the static analysis of consistency properties of
data structures. A decision procedure for SC theory has been proposed
to support program analysis. Sometimes, abstracting data structures
to sets is too imprecise for certain kind of analysis and more
accurate theories must be used; for example, when the order in which
the elements are stored matters.
We have investigated the decidability of the theory of arrays
augmented with integer variables (counting the number of elements
stored). We have considered the theory of arrays (Tarr) as the theory
modeling the container data structure because such a theory has played
a very important role in Computer Science since its introduction by
McCarthy in 1968. In fact, many papers have been devoted to its study
in the context of verification and many reasoning techniques, both
automatic and manual, have been developed to reason in such a theory.
Unfortunately, as already observed, Tarr alone or even extended with
extensional equality between arrays is not sufficient for many
applications of verification. For example, some works tried to extend
the theory to reason about sorted arrays while, more recently, Bradley
et al have shown the decidability of a restricted class of first-order
(possibly quantified) formulae whose satisfiability is decidable and
allows one to express many important properties about arrays.
In~\cite{ranise-jelia06}, we have considered the theory of arrays with
extensionality whose indexes have the algebraic structure of
Presburger Arithmetic (Tpr) and extended it with additional (function
or predicate) symbols expressing important features of arrays (e.g.,
the dimension of an array or an array being sorted). The main
contribution of the work is a method to integrate two decision
procedures, one for Tarr and one for Tpr, with instantiation
strategies that allow us to reduce the satisfiability problem of the
extension of Tarr union Tpr to the satisfiability problems decided by
the two available procedures.
Our approach to integrating decision procedures and instantiation
strategies is inspired by model-theoretic considerations and by the
rewriting-approach to build satisfiability procedures. For the
rewriting-based method, we followed the lines of [34], where it is
suggested that the (ground) formulae derived by the superposition
calculus between the axioms of a theory T, extending the theory of
equality Eq, and some ground literals while attempting to solve the
satisfiability problem of T can be passed to a decision procedure for
Eq. In~\cite{ranise-jelia06}, we used superposition to generate enough (ground)
instances of an extension of Tarr so to enable the decision procedures
for Tpr and Tarr to decide its satisfiability problem. An immediate
by-product of the approach is the fact that the various extensions of
Tarr can be combined together to decide the satisfiability of the
union of the various extensions.
Related work. The work most closely related to ours is that by Bradey
et al. The main difference is that we have a semantic approach to
extending Tarr since we consider only the satisfiability of ground
formulae and we introduce additional functions and predicates while in
Bradley et al, a syntactic characterization of a class of full
first-order formulae is considered which turns out to express many
properties of interest of arrays. Our approach allows us to get a
more refined characterization of some properties of arrays, yielding
the decidability of the extension of Tarr with injective arrays, which
is left open in Bradley et al.
Our instantiation strategy based on superposition has a similar spirit
of the work in Korovin and Ganzinger, where equational reasoning is
integrated in instantiation-based theorem proving. The main
difference with the work by Korovin and Ganzinger is that we solve the
state-explosion problem, due to the recombination of formulae caused
by the use of standard superposition rules, by deriving a new
termination result for an extension of Tarr as recommended by the
rewriting approach to satisfiability procedures. This allows us to
re-use efficient state-of-the-art theorem provers without the need to
implement a new inference system as required by Korvin and Ganzinger.
The instantiation strategies described in~\cite{ranise-jelia06} can
also be seen as an instance of instantiation-based methods that allow
one to employ decision procedures for first-order fragments more
complex than propositional logic as proposed by Korovin and Ganzinger.
The main difference between our work and that by Ganzinger and Korovin
is that our instantiation strategy is precise since it generates a
ground formula which is equisatisfiable to the original one, thereby
enabling the available decision procedures to conclude about the
satisfiability of the original formula without the need of further
instantiations (as required by Korvin and Ganzinger).
Discharging proof obligations in combinations of theories containing
enumerated data types
----------------------------------------------------------------------------------------------------
Finite sorts occur frequently and naturally as part of many program
verification problems; for example, in the presence of enumerated data
types. Indeed, theories formalizing finite sorts only admits finite
models and are problematic when combined with other theories (as it is
the case in many verification problems) since they do not satisfy the
stably-infinite hypothesis of the well-known combination method
proposed by Nelson and Oppen.
In~\cite{ranise-ijcar06}, we have investigated the requirement of
being stably-infinite for a (decidable) theory to be combined with
others by using the Nelson-Oppen combination schema. In particular,
we have considered combinations of theories whose signatures are
disjoint and classify the component theories according to the
decidability of their satisfiability problems in finite and infinite
models, respectively (notice that such problems coincide for
stably-infinite theories). Assume that the satisfiability problem in a
theory T1 is decidable in arbitrary models but not in infinite models.
Then, any combination of T1 with a theory T2 that does not have finite
models yields an undecidable satisfiability problem. This holds even
if T1 and T2 have disjoint signatures and even if satisfiability in T2
is decidable in arbitrary models. As a consequence of this
observation, we obtain the first (undecidability) result of the paper,
by exhibiting a theory whose satisfiability problem is decidable but
whose satisfiability problem in infinite models is undecidable.
The second result of~\cite{ranise-ijcar06} is related to decision
procedures based on rewriting. Armando \emph{et al} [2] showed how to
use a rewrite-based inference system to obtain decision procedures for
(disjoint) unions of variable-inactive theories, when there exist
rewrite-based decision procedures for the component theories. Here,
we explain the relationship between variable-inactivity and
stable-infiniteness. We show that if a theory is not stably infinite,
then the inference system is guaranteed to generate clauses that
constrain the cardinality of its models, so that the theory is not
variable-inactive. This result has two applications: first, it
generalizes the combination schema of [2] for (disjoint) unions of
theories that have rewrite-based satisfiability procedures. Second, it
suggests a simple way to combine the rewrite-based approach with
constraint-solving techniques that check satisfiability in finite
models.
Related Work. Recently, relaxing the stably-infinite requirement of
Nelson-Oppen combination schema has received a lot of attention in
order to design combination schemas handling theories that are not
stably-infinite. For instance, Tinelli and Zarba have recently shown
how to combine an arbitrary theory with one satisfying requirements
which are stronger than stable-infiniteness. Thus, contrary to the
combination schema by Nelson-Oppen, such a schema is asymmetric in the
sense that the requirements on the component theories are not the
same. Our combination schema, while going beyond Nelson-Oppen schema,
is symmetric and it allows us to precisely state the limitations of
the Nelson-Oppen combination schema.
Discharging proof obligations in pointer-based data structures
-----------------------------------------------------------------
The use of pointer-based data structures, i.e. of structures where an
updatable field can be referenced from more than one point, is
widespread in programming as well as in other areas of computer
science. Many approaches to reason about this technique have been
studied since the pioneering work of Burstall in 1972, but the result
has been methods that suffer from extreme complexity and serious
difficulties to incorporate reasoning in a wealth of decidable
theories over data and pointer values, such as integers.
The key to many of these approaches is the availability of a decision
procedure to automatically discharge proof obligations in a theory
encompassing cells, memories, and a reachability relation induced by
following pointers. Since reachability is not a first-order concept,
some higher-order feature must be included to precisely cope with it.
So, while there exist precise and automatic techniques to reason about
pointer reachability (see, e.g., the PALE tool), little has been done
to combine such techniques with available decision procedures for
theories over data and pointers. As a consequence, approximate
solutions have been proposed. Either the structure over data and
pointers have been abstracted away so that tools to reason about
reachability can be used, or a first-order approximation of
reachability has been found so that available decision procedures for
the theories of pointers and data can be used. Indeed, this
compromise causes a lack of precision in the verification techniques
where such reasoning procedures are used. It would be very desirable
to build a decision procedure capable of precisely reason about
reachability while being extensible with available decision procedures
for fragments of first-order logic.
In~\cite{ranise-sefm06}, we have considered the pointer-based data
structure of singly-linked lists and we have defined a Theory of
Linked Lists (TLL) as a class of structures of many-sorted first-order
logic. The theory is quite expressive: we can reason about cells
(which are pairs of data and pointers), indexed collections of cells
(i.e. memory configurations or heaps), and the reachability of a
certain cell from another.
We have shown the decidability of TLL by proving a small model
property. We have also proved that the decision problem of TLL is
\NP-complete. Then, we have shown that TLL satisfies the hypothesis
of a recent combination schema~\cite{frocos05b} that allows us to
incorporate arbitrary (decidable) theories over the elements or the
pointers. Given a decision procedure for TLL, we are capable of
combining it with a wide range of available decision procedures for
various decidable theories in first-order logic. We are left with the
problem of building a decision procedure for TLL. In fact, the
decision procedure suggested by a naive exploitation of the small
model property is not practical. We view TLL as an extension of a
core theory TBase by constructs for reachability. In this way, we
devise a reduction of the decision problem for TLL to that of TBase
and then we regard this theory as a combination of theories for which
available decision procedures exist.
Related Work. The theory TLL is similar to that used by Mehta and
Nipkow (which is a refinement of that of Bornat). The decidability of
TLL should explain why Isabelle is so successful in automatically
discharging most proof obligations about programs manipulating linked
lists considered by Mehta and Nipkow. The use of decidable fragments
of higher-order logic to reason about pointer-based data structures
have received a lot of attention and provides a high degree of
expressiveness for reachability. However, little is known about the
combination of such logics with decidable first-order theories to
reason about data and pointer values. In the context of Separation
Logic, a decision procedure for singly linked lists based on a
small-model theorem has been designed. The main difference with our
work is that that work abstracts away the theories over data and
pointers. In combination with predicate abstractions, some decision
procedures have been described by Balaban et al and Bingham et al for
logics which are similar to TLL. The main difference is in
expressiveness: both works abstract away theories over data and they
seem more restrictive than ours (for example, they cannot express
disjointness of lists). The works by Nelson, McPeak and Necula, and
Qaader and Lahiri are the most closely related to ours since they all
try to combine reachability reasoning with available procedures for
decidable fragments of first-order logic. The main difference is in
the treatment of reachability as they only provide first-order
approximations which are easy to combine with decision procedures but
provide limited precision. In contrast, we develop a (full) decision
procedure for TLL.
Publications (format Bibtex),
Here follows the list of the new publications:
@ARTICLE{RaniseT-IS06,
AUTHOR = {Ranise, S. and Tinelli, C.},
TITLE = {{Satisfiability Modulo Theories}},
JOURNAL = {IEEE Magazine on Intelligent Systems},
MONTH = {November},
YEAR = {2006},
NOTE = {To appear}
}
@INPROCEEDINGS{ranise-ijcar06,
AUTHOR = {Bonacina, M. P. and Ghilardi, S. and Nicolini, E. and Ranise, S. and
Zucchelli, D.},
TITLE = {{Decidability and Undecidability Results for Nelson-Oppen and
Rewrite-Based Decision Procedures}},
BOOKTITLE = {Proc. of the 3rd Int. Conference on Automated Reasoning (IJCAR)},
ADDRESS = {Seattle, WA, USA},
MONTH = {August},
NUMBER = {4130},
PAGES = {513--527},
SERIES = {LNAI},
YEAR = {2006}
}
@INPROCEEDINGS{ranise-disproving06,
AUTHOR = {Ranise, S.},
TITLE = {{Satisfiability Solving for Program Verification: towards the
efficient Combination of Automated Theorem Provers and Satisfiability Modulo
Theory Tools}},
BOOKTITLE = {Proc. of the IJCAR'06 Ws. DISPROVING: Non-Theorems, Non-Validity,
Non-Provability},
EDITOR = {Ahrendt, W. and Baumgartner, P. and de Nivelle, H.},
ADDRESS = {Seattle, WA, USA},
MONTH = {August},
PAGES = {49--58},
YEAR = {2006},
NOTE = {Invited paper}
}
@INPROCEEDINGS{ranise-pdpar06-a,
AUTHOR = {Ghilardi, S. and Nicolini, E. and Ranise, S. and Zucchelli, D.},
TITLE = {{Deciding Extensions of the Theory of Arrays by Integrating Decision
Procedures and Instantiation Strategies}},
BOOKTITLE = {Proc. of the IJCAR'06 Ws. PDPAR: Pragmatical Aspects of Decision
Procedures in Automated Reasoning},
EDITOR = {Cook, B. and Sebastiani, R.},
ADDRESS = {Seattle, WA, USA},
MONTH = {August},
YEAR = {2006}
}
@INPROCEEDINGS{ranise-sefm06,
AUTHOR = {Ranise, S. and Zarba, C.},
TITLE = {{A Theory of Singly-Linked Lists and its Extensible Decision
Procedure}},
BOOKTITLE = {Proc. of the 4th IEEE International Conference on Software
Engineering and Formal Methods (SEFM)},
ADDRESS = {Pune, India},
MONTH = {September},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {2006},
NOTE = {Extended version with full proofs, motivations, and examples in a
technical report available at
\texttt{\url{http://www.loria.fr/~ranise/pubs}}.}
}
@INPROCEEDINGS{ranise-jelia06,
AUTHOR = {Ghilardi, S. and Nicolini, E. and Ranise, S. and Zucchelli, D.},
TITLE = {{Deciding Extensions of the Theory of Arrays by Integrating Decision
Procedures and Instantiation Strategies}},
BOOKTITLE = {Proc. of the 10th European Conference on Logics in Artificial
Intelligence (Jelia)},
MONTH = {September},
NUMBER = {4160},
SERIES = {Lecture Notes in Computer Science},
YEAR = {2006},
NOTE = {Extended version with full proofs, motivations, and examples in a
technical report available at \url{http://www.loria.fr/~ranise/pubs}.}
}
@ARTICLE{ranise-ic06,
AUTHOR = {Bozzano, M. and Bruttomesso, R. and Cimatti, A. and Junttila, T. and
van Rossum, P. and Ranise, S. and Sebastiani, R.},
TITLE = {{Efficient Theory Combination via Boolean Search}},
JOURNAL = {Journal of Information and Computation},
NUMBER = {204},
PAGES = {1411-1596},
VOLUME = {10},
YEAR = {2006},
NOTE = {Special Issue on Combining Logical Systems}
}
@INPROCEEDINGS{DucLPAR06,
AUTHOR = {Kirchner, H\'el\`ene and Ranise, Silvio and Ringeissen, Christophe
and Tran, Duc-Khanh},
TITLE = {{Automatic Combinability of Rewriting-Based Satisfiability
Procedures}},
BOOKTITLE = {Proc. of the 13th Int. Conference on Logic for Programming,
Artificial Intelligence, and Reasoning (LPAR)},
ADDRESS = {Phnom Penh, Cambodia},
MONTH = {November},
PUBLISHER = {Springer},
SERIES = {To appear in Lecture Notes in Artificial Intelligence},
YEAR = {2006}
}
@INPROCEEDINGS{KirchnerRRT-TFIT06,
AUTHOR = {Kirchner, H\'el\`ene and Ranise, Silvio and Ringeissen, Christophe
and Tran, Duc-Khanh},
TITLE = {{Building and Combining Satisfiability Procedures for Software
Verification}},
BOOKTITLE = {Proceedings of 3rd Taiwanese-French Conference on Information
Technology (TFIT)},
ADDRESS = {Nancy, France},
MONTH = {March},
PAGES = {125-139},
YEAR = {2006}
}
@INPROCEEDINGS{RaniseRT-PDPAR06,
AUTHOR = {Ranise, Silvio and Ringeissen, Christophe and Tran, Duc-Khanh},
TITLE = {{Producing Conflict Sets for Combination of Theories}},
BOOKTITLE = {Pragmatics of Decision Procedures in Automated Reasoning
(PDPAR)},
EDITOR = {Cook, B. and Sebastiani, R.},
ADDRESS = {Seattle (WA)},
MONTH = {August},
YEAR = {2006},
NOTE = {Workshop affiliated to the 3rd International Joint Conference on
Automated Reasoning, IJCAR}
}
@INPROCEEDINGS{DeharbeFRR-ICTAC06,
AUTHOR = {D\'eharbe, David and Fontaine, Pascal and Ranise, Silvio and
Ringeissen, Christophe},
TITLE = {{Decision Procedures for the Formal Analysis of Software}},
BOOKTITLE = {3rd International Colloquium on Theoretical Aspects of Computing,
ICTAC},
ADDRESS = {Tunis, Tunisia},
MONTH = {November},
PUBLISHER = {Springer},
VOLUME = {4281},
SERIES = {Lecture Notes in Computer Science},
YEAR = {2006},
NOTE = {Tutorial}
}
@INPROCEEDINGS{ftp05,
AUTHOR = {Boughanmi, N. and Ranise, S. and Ringeissen, C.},
TITLE = {{On Structural Information and the Experimental Evaluation of SMT
Tools}},
BOOKTITLE = {Proc. of the International Workshop on First-Order Theorem
Proving (FTP'05)},
ADDRESS = {Koblenz, Germany},
YEAR = {2005}
}
@INPROCEEDINGS{pdpar05,
AUTHOR = {Armando, A. and Bonacina, M. P. and Ranise, S. and Schulz, S.},
TITLE = {Big proof engines as little proof engines: new results on
rewrite-based satisfiability procedures (Extended abstract)},
BOOKTITLE = {Notes of the Third Workshop on Pragmatics of Decision Procedures
in Automated Reasoning (PDPAR), co-located with the Seventeenth International
Conference on Computer Aided Verification (CAV'05)},
ADDRESS = {Edinburgh, Scotland (UK)},
YEAR = {2005}
}
@INPROCEEDINGS{frocos05b,
AUTHOR = {Ranise, S. and Ringeissen, C. and Zarba, C. G.},
TITLE = {{Combining data structures with nonstably infinite theories using
many-sorted logic}},
BOOKTITLE = {Proc. of the 5th Int. Workshop on Frontiers of Combining Systems
(FroCoS'2005)},
EDITOR = {Gramlich, B.},
ADDRESS = {Vienna, Austria},
MONTH = {September},
PAGES = {48--64},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {3717},
YEAR = {2005}
}
@INPROCEEDINGS{cav05,
AUTHOR = {Bozzano, M. and Bruttomesso, R. and Cimatti, A. and Junttila, T. and
van Rossum, P. and Ranise, S. and Sebastiani, R.},
TITLE = {{Efficient Satisfiability Modulo Theories via Delayed Theory
Combination}},
BOOKTITLE = {Proc. of the Int. Conf. on Computer-Aided Verification (CAV
2005)},
EDITOR = {Springer},
ADDRESS = {Edinburg, Scotland (UK)},
NUMBER = {3576},
SERIES = {Lecture Notes in Computer Science},
YEAR = {2005}
}
> statut des logiciels.
haRVey is distributed under LGPL and it has a new home page at
http://harvey.loria.fr .
Ciao,
Silvio.