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.