The workshop takes place in the First Floor Lecture Theatre of
the Ashton Building. See
facilities for additional information.
|Wednesday, 12 September 2007
||Introduction to FTP 2007
|Session 1 (Joint session with FroCoS'07)
||Chair: Ullrich Hustadt
|9:30 - 10:30
Hierarchical and Modular Reasoning in Complex Theories: The Case of Local Theory Extension
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
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
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
|11:00 - 11:35
||Combining Proof-Producing Decision Procedures
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
|11:35 - 12:10
|| Towards an Automatic Analysis of Web Service Security
Denis Lugiez, and
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
Olivier Pons, and
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
|14:05 - 14:15
||Further Details for FTP 2007 Participant
||Chair: Christophe Ringeissen
|14:15 - 14:50
Inductive Proof Search Modulo
Claude Kirchner and
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
|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
||Chair: Michael Rusinovitch
|15:55 - 16:30
||Developing Modal Tableaux and Resolution Methods via First-Order Resolution
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
|16:30 - 17:05
||Reasoning Automatically about Termination and Refinement
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
Racquet Club (Hargreaves Buildings,
5 Chapel Street, Liverpool L3 9AG)
|Thursday, 13 September 2007
||Chair: Hans de Nivelle
|9:00 - 10:00
Aspects of First-order Reasoning in the KeY system
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
|10:00 - 10:30
||ProofBuilder: An Interactive Prover for Students, with Extensive Capabilities
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
||Chair: Georg Struth
|11:00 - 11:35
||Labeled tableaux for distributed temporal logic
Jaime Ramos and
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
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
|12:10 - 13:45
||Chair: Silvio Ranise
|13:45 - 14:45
Applying FTPs in Formal Software Safety Certification
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
(Joint work with Ewen Denney and Johann Schumann, RIACS/NASA Ames
|14:45 - 15:15
||Chair: Renate Schmidt
|15:15 - 15:50
||A Graph-based Strategy for the Selection of Hypotheses |
Jean-Francois Couchot and
In previous works on verifying C programs by deductive approaches based on
SMT provers, we proposed the heuristic of separation analysis to handle more
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
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.