Nancy's GECCOO Report
B2-3 Discharging Proof Obligations

Silvio Ranise and Calogero G. Zarba

1  The Problem

The main goal of this subtask is to design and implement decision procedures which help to automatically discharge a large part of the proof obligations generated by the verification of various properties of programs. We consider a wide range of properties going from safety (such as the absence of null-pointer dereferences) to full correctness (such as a program implementing quick-sort returns a vector of integers ordered in ascending or descending order).

We want to identify theories which allow us to adequately express the properties of interest. While for certain properties (e.g. all expressions denoting an index of an array are in its bounds), the related theories are well-known (the quantifier-free fragment of Presburger arithmetic), for others (e.g. expressing that a set of memory locations reachable before a certain manipulation is still reachable afterwards) this is not clear and constitutes an interesting research problem. The situation is furtherly complicated by the fact that certain properties can only be expressed by combining several theories. This gives rise to the need of designing methods to combine the decision procedures for the various theories into one reasoning specialist for the union of the constituent theories.

An orthogonal problem is to handle the control-flow of the program which can be so large to generate proof obligations with a complex propositional structure which the automatic tool is required to exploit in order to scale up to real programs. Given the success of propositional solvers (such as BDD and SAT), it is common to use them to handle the Boolean structure of the proof obligations. An efficient integration between Boolean solvers and decision procedures is crucial to build reasoning tools for the verification of programs which scale up significantly.

2  Our Approach

Our approach consists of conducting both experimental and theoretical investigations, each influencing the other.

2.1  Experimental work

In collaboration with David Déharbe (DIMAp/UFRN, Natal, Brazil), we are developing a system called haRVey [DR03]. The system takes as input a theory T and several formulae f1, ..., fn and returns whether T entails fi for i=1,...,n. The key features of the system are the integration between Boolean solving, superposition theorem proving, and linear arithmetic reasoning, as we all as a pre-processing phase to handle quantifiers and the theory T.

2.1.1  Integrating Linear Arithmetic [IDR04]

Proof obligations frequently contain quantifiers. Classic combination methods, such the Nelson-Oppen [NO79], allows to handle only quantifier-free formulae. We have generalized the Nelson-Oppen method to combine superposition theorem proving (which handles quantified formulae) and linear arithmetic reasoning (which only handles quantifier-free formulae). The resulting procedure is sound but not complete and it gives good results in practice. Our benchmarks range from proof obligations obtained from the verification of the correctness of some sorting algorithms [FM99] to checking safety properties such as the the absence of ``array-out-of-bounds'' [DFS04].

2.1.2  Handling the Background Theory

The theory of a group of proof obligations is usually quite large since it specifies a lot of details such as the memory model of the programming language in which programs are written, its type system, etc. Indeed, each proof obligation only requires a tiny portion of such a big theory. We have adapted and implemented in haRVey existing methods [RS97] to identify a subset of the theory which is sufficient to prove a certain proof obligation. We have also adapted some techniques to expand definitions [NW01] in order to ease the task of the superposition prover. Preliminary experimental results on benchmarks coming from the verification of safety properties [DFS04], the retrieval of software components [Fis01], and proof obligations generated from Krakatoa are quite encouraging.

2.1.3  Automatic Verification of Pointer Programs [MR04]

In collaboration with F. Mehta (Technical University of Munich, Germany), we have investigated the use of haRVey to automatically discharge some of the sub-goals obtained while proving the correctness of an algorithm for garbage collection. The all verification effort [MN03] has been carried out in Isabelle, some of the sub-goals derived from a key lemma have been translated from Isabelle's higher-order syntax to haRVey's first-order syntax by hand, and then the latter has been invoked. The experience was positive since haRVey was capable to automatically handle all the translated sub-goals. Furthermore, after gaining some experience with the theory necessary to state the key lemma, we have been able to identify a (decidable) theory capable of expressing interesting properties about the reachability of certain memory locations following chains of pointers (see Section 2.2.4 below).

2.2  Theoretical work

In the context of Calogero Zarba's Post-Doc position attached to GECCOO, we are currently investigating how to decide and combine together theories that allow us to express interesting properties of programs. In particular, classic methods [NO79] for combination require that the component theories to satisfy certain conditions such as signature disjointness or stable infiniteness. The methods that we are developing attempt to relax these restrictions.

2.2.1  Lists [FRZ05]

We devised a decision procedures for the quantifier-free theory of lists with length constraints. The decision procedure can be combined with any other decision procedure for the theory of the elements, regardless of whether or not the theory of the elements is stably infinite or not.

2.2.2  Container Data structures [RRZ05]

We are devising a new general method for combining a general theory of container data structures (such as lists, arrays, sets, and multisets), with a theory of the elements (such as integers, reals, or booleans). The main contribution of our method is that it works for any general theory of the elements, even if the theory of the elements is not stable infinite.

2.2.3  Sets [CGRZ05]

Sets are ubiquitous in automated reasoning and program verification. For instance, set theory forms the central kernel of the high-level programming language SETL [SDDS86], as well as of the specification languages Z [Spi88] and B [Abr96]. Even for programming and specification languages that are not entirely based on set theory, sets still play a crucial role because they can be used either at the meta-level or as a data structure.

We are exploring different ways of deciding fragments of set theory efficiently (this study was started in [CDD+04, CDGR03]). These methods involve the reduction of a certain fragment of set theory to other simpler theories for which the research community has already developed efficient decision methods. Some of the simpler theories include: a core theory of insertion and membership, decidable by superposition [ARR03]; the theory of arithmetic (cf. [HLL03]); and the theory of equality with uninterpreted functions, decidable with combinations of SAT solving and decision procedures for equality (see e.g. [GHN+04]).

2.2.4  Pointers [RZ05]

When verifying programs manipulating pointers, one has often to reason about the set of memory cells that are reachable from an initial memory cell. To mechanize this kind of reasoning, we have defined a basic fragment of set theory, extended with a reachability operator. We are currently devising a decision procedure based on superposition that can decide this theory.

References

[Abr96]
Jean-Raymond Abrial. The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996.

[ARR03]
Alessandro Armando, Silvio Ranise, and Michaël Rusinowitch. A rewriting approach to satisfiability procedures. Information and Computation, 183(2):140--164, 2003.

[CDD+04]
J.-F. Couchot, F. Dadeau, D. Déharbe, A. Giorgetti, and S. Ranise. Proving and debugging set-based specifications. In A. Cavalcanti and P. Machado, editors, Electronic Notes in Theoretical Computer Science, proceedings of the Sixth Brazilian Workshop on Formal Methods (WMF'03), volume 95, pages 189--208, Campina Grande, Brazil, May 2004.

[CDGR03]
J.-F. Couchot, D. Déharbe, A. Giorgetti, and S. Ranise. Scalable automated proving and debugging of set-based specifications. Journal of the Brazilian Computer Society, 9(2):17--36, November 2003. ISSN 0104-6500.

[CGRZ05]
Jean-François Couchot, Alain Giorgetti, Silvio Ranise, and Calogero G. Zarba. Verification of set-based specifications. Draft, 2005.

[DFS04]
Ewen Denney, Bernd Fischer, and Johann Schumann. Using automated theorem provers to certify auto-generated aerospace software. In Proc. of the 2nd Int. Joint Conf. on Automated Reasoning, LNCS. Springer, 2004.

[DR03]
D. Déharbe and S. Ranise. Light-Weight Theorem Proving for Debugging and Verifying Units of Code. In Proc. of the International Conference on Software Engineering and Formal Methods (SEFM03), Brisbane, Australia, September 2003. IEEE Computer Society Press.

[Fis01]
B. Fischer. Deduction-Based Software Component Retrieval. PhD thesis, Universität Passau, 2001.

[FM99]
J.-C. Filliâtre and N. Magaud. Certification of sorting algorithms in the system Coq. In Theorem Proving in Higher Order Logics: Emerging Trends, 1999.

[FRZ05]
Pascal Fontaine, Silvio Ranise, and Calogero G. Zarba. Combining lists with non-stably infinite theories. In Franz Baader and Andrei Voronkov, editors, Logic Programming and Automated Reasoning. Springer, 2005. To appear.

[GHN+04]
Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. DPLL(T): Fast decision procedures. In R. Alur and D. Peled, editors, Proceedings of the 16th International Conference on Computer Aided Verification, CAV'04 (Boston, Massachusetts), volume 3114 of Lecture Notes in Computer Science, pages 175--188. Springer, 2004.

[HLL03]
Mohamed Hibti, Henri Lombardi, and Bruno Legeard. Deciding in HFS-theory via linear integer programming. In Andrei Voronkov, editor, Logic Programming and Automated Reasoning, volume 698 of Lecture Notes in Computer Science, pages 170--181. Springer, 2003.

[IDR04]
A. Imine, D. Déharbe, and S. Ranise. Abstraction-Driven Verification of Array Programs. In Proceedings of the 7th International Conference on Artificial Intelligence and Symbolic Computation (AISC'04), number 3249 in LNCS, pages 271--275, Linz, Austria, September 2004. Springer.

[MN03]
Farhad Mehta and Tobias Nipkow. Proving pointer programs in higher-order logic. In F. Baader, editor, Automated Deduction --- CADE-19, volume 2741 of Lecture Notes in Computer Science, pages 121--135, 2003.

[MR04]
F. Mehta and S. Ranise. Automated provers doing (higher-order) proof search: A case study in the verification of pointer programs. In Proc. of the 2nd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR'04), 2004.

[NO79]
Greg Nelson and Derek C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245--257, 1979.

[NW01]
Andreas Nonnengart and Christoph Weidenbach. Computing small clause normal forms. In Handbook of Automated Reasoning, pages 335--367. 2001.

[RRZ05]
Silvio Ranise, Christophe Ringeissen, and Calogero G. Zarba. Combining data structures with non-stably infinite theories. Draft, 2005.

[RS97]
Wolfgang Reif and Gerhard Schellhorn. Theorem proving in large theories. In Maria Paola Bonacina and Ulrich Furbach, editors, Int. Workshop on First-Order Theorem Proving, FTP'97, pages 119--124. Johannes Kepler Universität, Linz (Austria), 1997.

[RZ05]
Silvio Ranise and Calogero G. Zarba. Superposition-based of pointer programs. Draft, 2005.

[SDDS86]
Jacob T. Schwartz, Robert B. K. Dewar, Ed Dubinsky, and Edmond Schonberg. Programming with Sets: An Introduction to SETL. Springer, 1986.

[Spi88]
J. Michael Spivey. Understanding Z: A Specification Language and its Formal Semantics, volume 3 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1988.
This document was translated from LATEX by HEVEA.