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.
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.
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]).
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.