This workshop is part of QSL. Past workshops: Nov 2004, Jun 2004.
Register to the Nancy-Saarbrücken mailing list to be informed about what is happening in both sites !
Register to the workshop before October 6 by sending a mail to Chantal Llorens (firstname.lastname@example.org), if you want us to reserve lunches for you. The registration is free and includes the two lunches and the diner on Thursday evening. Please, indicate in your mail:
For your accomodation, you can find a hotel by contacting Nancy's tourism office. Here is another list. See for instance Akena Hotel.
Château Saint Fiacre, 210 rue de la grange aux moines, Villers-lès-Nancy
Tel: 03 83 58 17 02
List of participants
Organizer: Frédéric Blanqui
10:30 Session 1
10:30 Local reasoning for Termination, Ina Schaefer (MPI), joint work with Andreas Podelski (MPI) [pdf]
Separation logic is only able to express assertions over one program state of a heap-manipulating program whereas in the context of transition invariants it has been found that expressing relations of program states enables new possibilities for proving safety as well as liveness properties of programs. In this work, we bridge the gap between separation logic and transition invariants in order to obtain a uniform framework for proving total correctness of pointer programs. We introduce the concept of separated transition constraints which desribe the local effect of pointer programs by relations over program states. Separated transition constraints constitute the basis for separated transition logic which enables local reasoning about relations. We put the framework of transition invariants to work with separated transition logic as a consequence obtain a conservative extension of separation logic that is able to prove termination.
11:10 Characterizing provability in BI's pointer logic, Daniel Méry (UHP), joint work with Didier Galmiche (UHP) [pdf]
We propose a characterization of provability in BI's Pointer Logic (PL) that is based on semantic structures called resource graphs. This logic has been defined for reasoning about mutable data structures and some results about models and verification have been already provided. Here, we define resource graphs that capture PL models by considering heaps as resources and by using a labelling process. Then, we study provability in PL from a new calculus that builds such graphs from which proofs or countermodels can be generated.
11:50 Semantic Construction in Hybrid Intensional Logic, Patrick Blackburn (LORIA) joint work with Carlos Areces (LORIA) [pdf]
In the early 1970s Richard Montague developed IL (Intensional Logic) and in his classic paper "The Proper Treatment of Quantification in Ordinary English" laid the foundations of modern natural language semantics. In this talk (which is based on joint work with Carlos Areces) I will explore the consequences of replacing Montague's IL with HIL (Hybrid Intensional Logic).
13:40 Session 2
13:40 Terms and proof nets considered as sets-with-structure, François Lamarche (INRIA)
I want to make an important point, which I know by experience not to be well understood by many people who deal with representations of formal proofs. Things like proof terms, proof nets, or just plain terms (modulo some equational theory) can have non-trivial structure-preserving permutations (automorphisms). But it does not mean that, for example, there is a unique proof of A * A |- A * A, i.e. that the identity proof and the "twist" proof should be identitified. A simple and elegant language to express these phenonmena was developed by André Joyal 20 years ago.
14:20 On the Dynamic Increase of Multiplicities in Matrix Proof Methods for Classical Higher-Order Logic, Serge Autexier (DFKI) [pdf]
A major source of the undecidability of a logic is the number of instances --- the so-called multiplicities --- of existentially quantified formulas that are required in a proof. We consider the problem in the context of matrix proof methods for classical higher-order logic and present a technique which improves the standard practice of iterative deepening over the multiplicities. We present a mechanism that allows to adjust multiplicities on demand during matrix-based proof search and not only preserves existing substitutions and connections, but additionally adapts them to the parts that result from the increase of the multiplicities.
15:00 Resource tree models and semi structured data, Nicolas Biri (UHP), joint work with Didier Galmiche (UHP) [pdf]
We present a new tree structure, called resource tree, that represents complex information, through resources inside nodes, and also distinguishes the structure and the information it contains. Moreover, we define a separation and spatial logic with a modality for locations (BI-Loc). Our model is enriched with a general command language for manipulating resource trees and also with a Hoare's triple semantics. This language allows basic manipulations of trees and we study particular instantiations of our resource tree model, namely one that allows to represent the pointer and permission models and another one that allows to represent XML data and their transformations.
16:00 Session 3
16:00 On the Role of Medial in a Boolean Category, Lutz Strassburger (Saarland University)
In its most general meaning, a Boolean category is to categories what a Boolean algebra is to posets. In a more specific meaning a Boolean category should provide the abstract algebraic structure underlying the proofs in Boolean Logic, in the same sense as a Cartesian closed category captures the proofs in intuitionistic logic and a *-autonomous category captures the proofs in linear logic. However, recent work has shown that there is no canonical axiomatisation of a Boolean category. In this work, we will see a series (with increasing strength) of possible such axiomatisations, all based on the notion of *-autonomous category. We will particularly focus on the medial map, which has its origin in an inference rule in KS, a cut-free deductive system for Boolean logic in the calculus of structures.
16:40 A Structured Set of Higher-Order Problems, Christoph Benzmueller (Saarland University), joint work with Chad Brown (Saarland University) [pdf]
We present a set of problems that may support the development of calculi and theorem provers for classical higher-order logic. We propose to employ these test problems as quick and easy criteria preceding the formal soundness and completeness analysis of proof systems under development. Our set of problems is structured according to different technical issues and along different notions of semantics (including Henkin semantics) for higher-order logic. Many examples are either theorems or non-theorems depending on the choice of semantics. The examples can thus indicate the deductive strength of a proof system.
17:20 Challenges for Church's Type Theory, Chad Brown (Saarland University) [pdf]
Church's type theory is sometimes suggested as a potential foundation for mathematics. We examine some challenging issues related to representation and automation using Church's type theory and its variants. We consider how sets and partial functions are encoded in Church's type theory and how such encodings relate to mathematical practice. We also consider how the need for automation suggests both the inclusion and exclusion of type variables.
50 rue Henri Poincaré, Nancy [map]
Tel: 03 83 35 24 57
09:00 Session 4
09:00 Resolution-based verification of cryptographic protocols and blind signatures, Eugen Zalinescu (LORIA) [pdf]
We present a decidability result for verifying secrecy for a class of protocols with an unbounded number of sessions, when the intruder power is extended to take into account CBC encryption and blind signatures. This is achived using Horn clauses and ordered resolution strategies. We apply this result to fix the Needham-Schroeder symmetric key authentication protocol, which is known to be flawed when CBC mode is used.
09:40 Relations between abstract and probalistic models of cryptographic protocols, Véronique Cortier (CNRS) [pdf]
Since the 1980s, two approaches have been developed for analyzing security protocols. One of the approaches relies on a computational model that considers issues of complexity and probability. This approach captures a strong notion of security, guaranteed against all probabilistic polynomial-time attacks. The other approach relies on a symbolic model of protocol executions in which cryptographic primitives are treated as black boxes. Since the seminal work of Dolev and Yao, it has been realized that this latter approach enables significantly simpler and often automated proofs. However, the guarantees that it offers have been quite unclear. In this talk, we will present results relating them to each other, that is, connecting the formal model with computational notions of security.
10:40 Session 5
10:40 Security in Multi-Agents Systems, Dieter Hutter (DFKI) [pdf]
This talk uses a comparison-shopping scenario to introduce a general methodology for formally verifying the security of multi-agent systems. Following the approach of possibilistic information flow security, the flow of information between and within agents is restricted in order to ensure that secrets will not be disclosed to unauthorized meddlers. The security requirements for the overall system are then decomposed into requirements for the individual agents that can be verified independently from each other. Exploiting the modular structure of a multi-agent system considerably reduces the complexity of the overall security analysis. The techniques for decomposing security requirements, for verifying individual agents, and for deriving global security guarantees for the entire system from locally verified properties are all generic in the sense that they apply also to many other systems and security requirements than the ones that appear in the example scenario.
11:50 Resources, process calculi and Gödel logic, Dominique Larchey-Wendling (CNRS) [pdf]
Gödel-Dummett logic LC and its finite approximations LCn are the intermediate logics complete w.r.t. linearly ordered Kripke models. In this paper, we use LCn logics as a tool to bound resource consumption in some process calculi. We introduce a non-deterministic process calculus where the consumption of a particular resource denoted o is explicit and provide an operational semantics which measures the consumption of this resource. We present a linear transformation of a process P into a formula f of LC. We show that the consumption of the resource by P can be bounded by the positive integer n if and only if the formula f admits a counter-model in LCn. Combining this result with our previous results on proof and counter-model construction for LCn, we conclude that bounding resource consumption is (linearly) equivalent to searching counter-models in LCn.
13:40 Session 6
13:40 Dependability evaluation of real-time applications distributed on TDMA-based networks, Françoise Simonot-Lion (LORIA) [ppt]
TDMA is largely adopted by many networks for providing to real-time applications with determinism. However, this determinism could be jeopardized under the transient environmental perturbations, causing application failures. In this paper, we investigate the impact of the transient perturbations (especially due to Electromagnetic Interferences) on the application dependability. We give a contribution on the method for evaluating the application failure probability in function of the TDMA cycle error probability within an EMI zone. This method extends the existing one on the "consecutive-k-out-of-n:F" systems to including variable probability. Numerical applications have shown its efficiency for computing the application failure probability within a given EMI area.
14:20 Combining Sequential and Concurrent Verification - The SMTP Case Study, Werner Stephan (DFKI) and Bruno Langenstein (DFKI) [pdf]
Verification of real world applications typically has to address both, the verification of sequential program fragments and properties of the asynchronous communication between concurrent threads or processes. While sequential verification is concerned with the manipulation of complex data structures and/or elaborate algorithms communication issues include the integrity of data exchanged between components and liveness properties. Using the SMTP implementation the talk describes how techniques for the formal development of sequential code fragments can be combined with temporal reasoning about communication in an abstract interface model. It includes a discussion of the integration of that model into the overall development of a verified system in the VERISOFT project.
15:20 Session 7
15:20 Towards a Combination of Heterogenous Deductive Tools for System Verification, Alwen Tiu (LORIA) joint work with Pascal Fontaine (LORIA), Kamal Gupta, Jean-Yves Marion (INPL), Stephan Merz (INRIA) and Leonor Prensa Nieto (INPL) [pdf]
We present an ongoing work at LORIA on combining Isabelle/HOL with different automatic deductive tools for system verification. The main case study is the verification of distributed algorithms, in particular the fault-tolerant clock synchronization algorithms. We will talk about our current implementation of interfaces between Isabelle, using the oracle facility, with the automatic tools ICS, CVC-Lite and harVey, and the interface with SAT solvers. For the latter part, we show how to reconstruct the proof of unsatisfiability from the SAT solver. This is done by first transforming the formula to be proved into CNF (while generating proofs at the same time), which is then given to the SAT solver. The transformation is done within Isabelle, where, given a formula phi, one gets the theorem phi = phi', where phi' is the CNF formula. With the help of the proof trace produced by the SAT solver, an Isabelle proof of the original formula is then reconstructed based on simple resolution steps. We will also discuss several experiments on CNF transformation and proof reconstruction to improve efficiency.
16:00 haRVey : from congruence closure to a decision procedure for sets and much more, Pascal Fontaine (LORIA) [pdf]
The fragment of quantifier-free first-order formulas containing only equalities, and uninterpreted predicates and functions is decidable. Congruence closure is the key element for an efficient decision procedure : it adds to the power of SAT solvers the expressive power of this quantifier-free fragment. We present a method for further extending the expressive power of tools built on sat solvers and congruence closure. It allows, for instance, to use in a natural way some set-related operators, in addition to uninterpreted symbols. [web]