FTP 2007 - Program with abstracts

Many problems in computer science can be reduced to proving the satisfiability of conjunctions of literals w.r.t. a background theory. This theory can be a concrete theory (e.g. the theory of real or rational numbers), the extension of a theory with additional functions (free, monotone, or recursively defined) or a combination of theories. It is therefore very important to have efficient procedures for checking the satisfiability of conjunctions of ground literals in such theories.

We here give an overview of results on hierarchical and modular reasoning in complex theories. We show that for a special type of extensions of a base theory, which we call local, hierarchic reasoning is possible (i.e. proof tasks in the extension can be hierarchically reduced to proof tasks w.r.t. the base theory). Many theories important for computer science or mathematics fall into this class (typical examples are theories of data structures, theories of free or monotone functions, but also functions occurring in mathematical analysis).

In fact, it is often necessary to consider complex extensions, in which various types of functions or data structures need to be taken into account at the same time. We show how such local theory extensions can be identified and under which conditions locality is preserved when combining theories, and we investigate possibilities of efficient modular reasoning in such theory combinations.

We present several examples of application domains where such theories occur in a natural way. We show, in particular, that various phenomena analyzed in the verification literature can be explained in a unified way using the notion of locality.

10:30 - 11:00

Coffee Break

Session 2 (Joint session with FroCoS'07)

11:00 - 11:35

Combining Proof-Producing Decision Procedures
Silvio Ranise, Christophe Ringeissen, and Duk Khanh Tran
Constraint solvers are key modules in many systems with reasoning capabilities (e.g., automated theorem provers). To incorporate constraint solvers in such systems, the capability of producing conflict sets or explanations of their results is crucial. For expressiveness, constraints are usually built out in unions of theories and constraint solvers in such unions are obtained by modularly combining solvers for the component theories. In this paper, we consider the problem of modularly constructing conflict sets for a combined theory by re-using available proof-producing procedures for the component theories. The key idea of our solution to this problem is the concept of explanation graph, which is a labelled, acyclic and undirected graph capable of recording the entailment of some equalities. Explanation graphs allow us to record explanations computed by a proof-producing procedure and to refine the Nelson-Oppen combination method to modularly build conflict sets for disjoint unions of theories. We also study how the computed conflict sets relate to an appropriate notion of minimality.

11:35 - 12:10

Towards an Automatic Analysis of Web Service Security
Yannick Chevalier, Denis Lugiez, and Michael Rusinowitch
Web services send and receive messages in XML syntax with some parts hashed, encrypted or signed, according to the WS-Security standard.

In this paper we introduce a model to formally describe the protocols that underly these services, their security properties and the rewriting attacks they might be subject to. Unlike other protocol models (in symbolic analysis) ours can handle non-deterministic receive/send actions and unordered sequence of XML nodes.

Then to detect the attacks we have to consider the services as combining multiset operators and cryptographic ones and we have to solve specific satisfiability problems in the combined theory. By non-trivial extension of the combination techniques of [CR05] we obtain a decision procedure for insecurity of Web services with messages built using encryption, signature, and other cryptographic primitives. This combination technique allows one to decide insecurity in a modular way by reducing the associated constraint solving problems to problems in simpler theories.

12:10 - 12:45

Certification of Automated Termination Proofs
Evelyne Contejan, Piere Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain
Nowadays, formal methods rely on tools of different kinds: proof assistants with which the user interacts to discover a proof step by step; and fully automated tools which make use of (intricate) decision procedures. But while some proof assistants can check the soundness of a proof, they lack automation. Regarding automated tools, one still has to be satisfied with their answers Yes/No/Do not know, the validity of which can be subject to question, in particular because of the increasing size and complexity of these tools.

In the context of rewriting techniques, we aim at bridging the gap between proof assistants that yield formal guarantees of reliability and highly automated tools one has to trust. We present an approach making use of both shallow and deep embeddings. We illustrate this approach with a prototype based on the CiME rewriting toolbox, which can discover involved termination proofs that can be certified by the coq proof assistant, using the Coccinelle library for rewriting.

12:45 - 14:05

Lunch

14:05 - 14:15

Further Details for FTP 2007 Participant

Session 3

Chair: Christophe Ringeissen

14:15 - 14:50

Inductive Proof Search Modulo
Fabrice Nahon, Claude Kirchner and Helene Kirchner

We present an original narrowing-based proof search method for inductive theorems in equational rewrite theories given by a rewrite system R and a set E of equalities. It has the specificity to be grounded on deduction modulo and to rely on narrowing to provide both induction variables and instantiation schemas. Whenever the equational rewrite system (R,E) has good properties of termination, sufficient completeness, and when E is constructor and variable preserving, narrowing at defined-innermost positions leads to consider only unifiers which are constructor substitutions. This is especially interesting for associative and associative-commutative theories for which the general proof search system is refined. The method is shown to be sound and refutationaly complete.

14:50 - 15:25

Extending Poitín to Handle Explicit Quantification
Humayun Kabir and Geoff Hamilton

We have previously shown how the distillation program transformation algorithm can be used to prove inductive theorems in which there is no explicit quantification, and all variables are assumed to be implicitly universally quantified. These techniques were implemented in the theorem prover Poitín. In this paper, we show how Poitín can be extended to prove inductive theorems which contain explicit universal and existential quantifiers. This extension has also been implemented and added to Poitín; we give the results of applying the resulting theorem prover to a number of example conjectures.

15:25 - 15:55

Coffee Break

Session 4

Chair: Michael Rusinovitch

15:55 - 16:30

Developing Modal Tableaux and Resolution Methods via First-Order Resolution
Renate Schmidt

This paper explores the use of resolution as a meta-framework for developing different deduction calculi for modal dynamic logics. Dynamic modal logics are PDL-like extended modal logics which are closely related to description logics. We show how tableau systems, modal resolution systems and Rasiowa Sikorski systems, which are dual tableau systems, can be developed and studied by using standard principles and methods of first-order theorem proving. The approach is based on the translation of modal logic reasoning problems to first-order clausal form and using a suitable refinement of resolution to construct and mimic deriviations of the desired proof method. The inference rules of the calculus can then be read off from the clausal form used. We show how this approach can be used to generate new proof calculi for logics that have been considered in the literature before and prove soundness, completeness and decidability results. This slightly unusual approach allows us to gain new insight and results for familiar and less familiar logics and difference proof methods, and compare them in a common framework.

16:30 - 17:05

Reasoning Automatically about Termination and Refinement
Georg Struth

We present very short automated proofs of Bachmair and Dershowitz’s termination theorem in different variants of Kleene alge- bras. Through our experiments we also discover three novel refinement laws for nested infinite loops. Finally, we introduce novel divergence mod- ules in which the automation is particularly satisfactory. These structures seem very promising for automated reasoning about infinite behaviours in programs and discrete dynamical systems.

17:05 - 17:35

Business Meeting

19:00

Conference Dinner
Racquet Club (Hargreaves Buildings, 5 Chapel Street, Liverpool L3 9AG)

Thursday, 13 September 2007

Session 5

Chair: Hans de Nivelle

9:00 - 10:00

Invited Talk
Aspects of First-order Reasoning in the KeY system
Martin Giese

The deductive program verification system developed as part of the KeY project is based on a sequent calculus for a certain dynamic logic, which is specially tailored to the verification of Java-Card programs. The sequent calculus symbolically executes programs, until proof obligations in first-order logic are obtained. To simplify reasoning about Objects of a Java program, the first-order logic of KeY has strongly typed terms and subtyping. In the context of program verification, it is desirable to be able to have an integrated interactive and automated theorem prover, and moreover, an automated proof procedure without backtracking is desirable. Theory specific reasoning in KeY is done by enhancing the prover with theory specific rules, known as taclets, which can easily be formulated in a special rule language.

10:00 - 10:30

ProofBuilder: An Interactive Prover for Students, with Extensive Capabilities
Hugh McGuire

This paper will present an interactive first-order theorem-proving system named ProofBuilder, which is pedagogically oriented. As with other systems, ProofBuilder covers a wide range of formal reasoning, from propositional simplification to strong induction; but what distinguishes ProofBuilder is that it is designed to enable users to prove theorems as much as possible like the way they do manually. Such aspects of the design include a framework that clarifies which formulas in a proof are premises that are hypothesized to be true, and which are goal formulas that need to be proven; and mechanisms to apply a variety of proof methods and strategies such as forward and backward reasoning, proving by contradiction, and proving by cases.

10:30 - 11:00

Coffee Break

Session 6

Chair: Georg Struth

11:00 - 11:35

Labeled tableaux for distributed temporal logic
David Basin, Carlos Caleiro, Jaime Ramos and Luca Viganó

The distributed temporal logic DTL is a logic for reasoning about temporal properties of distributed systems from the local point of view of the system agents, which are assumed to execute sequentially and to interact by means of synchronous event sharing. Distribution is implicit, making it easier to state the properties of an entire system through the local properties of its agents and their interaction. The interpretation structures of DTL are suitably labeled distributed life-cycles, built upon a form of Winskel's event structures. In this paper, we present a sound and complete labeled tableaux system for DTL, which we formalize by first introducing a labeled tableaux system for linear temporal logic (LTL), where the reasoning is local, and then combining LTL systems local for each agent with rules that capture the distributed nature of DTL, where one can further express global properties via communication.

11:35 - 12:10

What First Order Theorem Provers Do For Monodic Temporal Reasoning
Ullrich Hustadt

Monodic temporal logic is the most general fragment of first-order temporal logic for which sound and complete calculi have been developed so far, including resolution calculi. In this paper we present one such calculus, the ordered fine-grained resolution calculus, discuss the role that first-order resolution can play in the implementation of that calculus, consider some of the problems involved with the realisation of fair derivations in such an implementation, and present a solution to these problems.

12:10 - 13:45

Lunch

Session 7

Chair: Silvio Ranise

13:45 - 14:45

Invited Talk
Applying FTPs in Formal Software Safety Certification
Bernd Fischer

Formal software safety certification approaches like proof-carrying code use Hoare-techniques to prove that programs satisfy a range of given safety properties. Since these properties are simpler than full functional correctness, the emerging proof obligations are simpler as well, and come within reach of the capabilities of current fully automated first-order theorem provers.

In this talk, I will describe our approach to safety certification of automatically generated code. I will focus on our experience in integrating first-order theorem provers as "off-the-shelf" components into such a system, and on the results we achieved with different provers.

(Joint work with Ewen Denney and Johann Schumann, RIACS/NASA Ames Research Center.)

14:45 - 15:15

Coffee Break

Session 8

Chair: Renate Schmidt

15:15 - 15:50

A Graph-based Strategy for the Selection of Hypotheses
Jean-Francois Couchot and Thierry Hubert

In previous works on verifying C programs by deductive approaches based on SMT provers, we proposed the heuristic of separation analysis to handle more difficult problems. Nevertheless, this approach suffers from yielding too large Verification Conditions (VCs) when applied on industrial C programs. This work presents a strategy to select relevant hypotheses in each VC. The relevance of an hypothesis is the combination of two separated dependency analyzes formalized by some graph traversals. The approach is applied on a benchmark issued from an industrial program verification.

15:50 - 16:25

Redundancy in the Geometric Resolution Calculus
Hans de Nivelle

We study redundancy for the geometric resolution calculus used by Geo. We show that geometric resolution allows elimination of redundant formulas, similar to superposition. In order to prove completeness and to study the effect of the elimination of redundandant formulas on proof length, we introduce a new calculus for proving redundancy. It turns out that the calculus which was originally used in Geo, can be replaced by this new calculus without changing the structure of the proof search process. The new calculus is simpler than the old calculus, and it sometimes derives stronger results from the same set of premisses as the old calculus. We prove completeness of elimination of redundant clauses, using proof permutations in the new calculus.

16:25 - 17:00

Edit and Verify
Radu Grigore and Michal Moskal

Automated theorem provers are used in extended static checking, where they are the performance bottleneck. Extended static checkers are run typically after incremental changes to the code. We propose to exploit this usage pattern to improve performance. We present two approaches of how to do so and a full solution.