Centre Fédéré en Vérification

Message sequence charts are a popular visual notation for describing communication protocols in form of scenarios. They are a standard of the ITU and part of UML.

This talk gives a survey of recent results on two main verification problems concerning MSC specifications: model-checking (regular/cooperative HMSCs) and the realization of HMSC specifications by communicating finite-state machines.

Pushdown processes are pushdown automata seen under a different light: we are not interested in the languages they recognise, but in the transitions systems they generate. These are infinite transition systems with pairs of the form (control state, stack content) as states.

We started to work on the analysis of pushdown processes in 1997. At that time our motivation was purely theoretical. Six years later, our work (and what we have drawn from the work of others) has produced the Moped tool, a model-checker for pushdown systems able to find bugs in Windows XP drivers with 27000 lines of code.

In this talk I'll sketch the (rather long) way from the theory to the realisation. I will spend some time explaining the basic ideas, and then present some experimental results. I'll then sketch some other applications.

This is joint work with Stefan Schwoon

We present ProB, an animation and model checking tool for the B method. ProB's animation facilities allow users to gain confidence in their specifications, and unlike the animator provided by the B-Toolkit, the user does not have to guess the right values for the operation arguments or choice variables. ProB contains a model checker and a constraint-based checker, both of which can be used to detect various errors in B specifications. We present our first experiences in using ProB on several case studies, highlighting that ProB enables users to uncover errors that are not easily discovered by existing tools.

We show applications and limitations of the theory of well quasi-ordered programs, by analyzing different classes of parameterized timed systems.

We consider verification of safety properties for timed networks: systems consisting of an arbitrary set of identical timed processes. First, we show that checking safety properties is decidable in the case where each timed process is equipped with a single real-valued clock. Then, we consider multi-clock timed networks. We prove that the problem becomes undecidable when each process has two clocks. On the other hand, we show that the problem is decidable when clocks range over a discrete time domain. This decidability result holds when processes have any finite number of clocks.

Pnueli and Rosner showed that deciding two-player games over finite graphs with winning conditions specified as an LTL formula is 2EXPTIME-complete. Recent papers have shown the complexity bounds for this decision problem in various fragments of LTL. In this talk, we will survey on these results.

A surprising result is that disallowing next and until, and retaining only the always and eventually operators in the specifications, deciding LTL games is still 2EXPTIME-hard. This clearly contrasts with the complexity bounds of model checking that is NP-complete for this fragment while is PSPACE-complete in the general case. To achieve this result new techniques for encoding Turing machine computations using games are introduced.

The complexity can be reduced to EXPSPACE-complete, disallowing in this fragment the always in the scope of the eventually operator and vice-versa. Note that the complexity stays unchanged if the next operator is added. Also, it is interesting that if the only temporal operator is either the always or the eventually operator, and Boolean negation is allowed only at the level of the atomic propositions, deciding games becomes PSPACE-complete. Thus the Boolean closure of such specifications causes the complexity to raise from PSPACE-complete to EXPSPACE-complete.

Finally, if the winning condition is a Boolean combination of formulas of the form ``eventually p'' and ``infinitely often p'', for a state-formula p, then the game can be decided still in PSPACE, and also a matching lower bound is established. Such conditions include safety and reachability specifications on game graphs augmented with fairness conditions for the two players.

• Speaker: Markus Müller-Olm Lehrgebiet Praktische Informatik V, FernUniversität in Hagen, Germany
• Date: April, 23th, 2004
• Time: 11AM
• Location: Louvain-la-Neuve University (UCL) classroom BARB91
• Abstract:

  Automatic program analyses that determine run-time properties of programs are needed in optimizing compilers and for validation of programs. Due to fundamental recursion-theoretic reasons, however, all non-trivial semantic properties are undecidable in programs of a computationally-universal programming language. One way out is to work with approximate analyses. Such analyses determine certain but not necessarily all valid properties of a given type; they are correct but in general incomplete ("approximate").

  This leads to the question how to assess the precision of an approximate analysis. One way to do so is to define an abstraction of programs and to show that the approximate analysis solves the abstracted problem thus obtained exactly. Abstraction also allows us to study abstracted analyses problems as such. In order to do so we fix a (hopefully natural) abstraction, establish (un-)decidability and complexity results for the abstracted problem, and construct algorithms that solve the abstracted problem completely and as efficient as possible. The talk reports on some results of this kind obtained in recent years in various classes of programs. The goal of such studies is to get a better understanding of the trade-off between efficiency and precision in the construction of approximate analysis algorithms and to uncover potential for construction of better analysis algorithms.

• Speaker: Pascal Van Hentenryck, Brown university
• Date: April, 23th, 2004
• Time: 2PM
• Location: Louvain-la-Neuve University (UCL) classroom BARB92
• Abstract:

  We present an overview of Comet, an object-oriented language specifically designed to simplify the implementation of local search algorithms in combinatorial optimization. The main novelty in Comet is its constraint-based architecture organized around two main components: a declarative component which models the application in terms of differentiable objects such as constraints, and a search component which describes the heuristic and meta-heuristic in terms of high-level control abstractions such as events. The architecture enables local search algorithms to be extremely high-level, compositional, and modular, often decreasing development time by orders of magnitude. We report experimental results on a variety of applications in scheduling and logistics, where Comet was instrumental in closing open problems and discovering novel, more effective, algorithms. (Joint work with Laurent Michel)

• Speaker: Isabelle Pollet, Université Catholique de Louvain
• Date: April, 23th, 2004
• Time: 3:45PM
• Location: Louvain-la-Neuve University (UCL) classroom BARB92
• Abstract:

  The application field for static analysis of Java programs is getting broader, ranging from compiler optimizations (like dynamic dispatch elimination) to security issues. Many of those analyses include type analyses. We propose a `generic' framework, which improves on previous types analyses by introducing structural information. Moreover, structural information allows us to easily extend the framework to perform many different kinds of analyses. The framework is based on the abstract interpretation methodology. It is composed of a standard semantics, a family of abstract domains, an abstract semantics based on these domains and a post-fixpoint algorithm to compute this semantics. The analysis is limited to a representative subset of Java, without concurrency. A complete prototype of the framework allows us to illustrate the accuracy and the efficiency of the approach (for moderately sized programs).

• Speaker: Franck Cassez, CNRS, Nantes
• Time: 11AM
• Download Franck Cassez' slides
• Abstract:

  Priced timed (game) automata extend timed (game) automata with costs on both locations and transitions. In this paper we focus on reachability games for priced timed game automata and prove that the optimal cost for winning such a game is computable under conditions concerning the non-zenoness of cost. Under stronger conditions (strictness of constraints) we prove that it is decidable whether there is an optimal strategy in which case an optimal strategy can be computed. Our results extend previous decidability result which require the underlying game automata to be acyclic. Finally, our results are encoded in a first prototype in HyTech which is applied on a small case-study.

• Speaker: Thomas Henzinger, University of California, Berkeley, Ecole Polytechnique Fédérale de Lausanne
• Time: 2PM
• Abstract:

  While model checking has entered industrial practice in hardware verification for some time now, the original goal of model checking ---namely, software verification--- has proved elusive until recently. One of the main reasons is that boolean finite-state abstractions are readily available for circuits, but not for programs. A central problem in software verification is to find an abstraction of the input program which is sufficiently fine to prove or disprove the desired property, and yet sufficiently coarse not to overwhelm the exhaustive exploration of the state space performed by a model checker. It is often useful to abstract the values of program variables by recording, instead, at each program location the truth of critical predicates. The critical predicates can be found automatically using counterexample-guided abstraction refinement, which starts with a coarse abstraction of the program and iteratively refines the abstraction until either an error trace is found or the property is proved.

  The BLAST project has improved this approach in three significant ways. First, the program abstraction is constructed lazily, which means that a critical predicate is evaluated only at those program locations where its value is relevant. While for a large piece of software, hundreds of predicates may be critical, at any given location typically less than 10 of these predicates are relevant. Second, BLAST finds critical predicates by Craig interpolation, which means that each predicate is an assertion about the current values of program variables at a location. Computed in this way, predicates do not encode the history of a program trace but rather capture exactly the relevant current state information at each program location. Third, in order to handle multi-threaded programs, BLAST deals with one thread at a time and automatically infers a context assumption for each thread, which summarizes the interference caused by the other threads. The context assumptions, in turn, are automatically discharged by assume-guarantee reasoning.

  Given a C program and a temporal safety property, BLAST provides either a test vector that exhibits a violation of the property, or a succinct proof certificate in the form of an abstract reachability tree, which can be reused incrementally for checking updated versions of the program. The tool has been applied successfully to Linux and Windows device drivers and NesC protocols with tens of thousands of lines of C code.

  The BLAST project is the work of Ranjit Jhala, Rupak Majumdar, Dirk Beyer, Shaz Qadeer, Marco Sanvido, and Gregoire Sutre.

• Speaker: Laurent Van Begin, Université Libre de Bruxelles
• Time: 4PM
• Abstract:

  In this talk, we will present a general schema called "Expand-Enlarge and Check" from which new efficient algorithms for the coverability problem of WSTS can be constructed. Well-structured transition systems (WSTS for short) are a general class of infinite state systems for which decidability results rely on the existence of a well-quasi-ordering between states that is compatible with the transitions. In particular, the coverabiliy problem (reachability of an upward-closed set of states, relative to the wqo), is decidable for that class of systems. Popular examples of WSTS are Petri nets, monotonic extensions of Petri nets, and lossy fifo systems. For all those systems, the coverability problem can be answered by a simple backward algorithm. Unfortunately, this general backward algorithm may be highly inefficient because it often has to manipulate sets of states that are unreachable and difficult to represent compactly. In the late 60s, Karp and Miller have defined a procedure that uses forward reachability and acceleration to decide the coverability problem of Petri nets. The advantage of the forward approach is that it has to manipulate sets of reachable states that are usually easier to represent compactly. Several attempts to generalize this approach to other classes of WSTS have failled. We show here that our schema allows us to define forward algorithms that decide coverability for classes of systems for which the Karp and Miller procedure can not be generalized. In particular, we present a direct application of our schema to monotonic extensions of Petri nets. Our result has important applications in parametric verification and allows us to prove a completness result for a recent algorithm proposed by Henzinger et al for the analysis of multi-threaded programs.

  This is a joint work with Gilles Geeraerts and J-F Raskin.

Parameterized complexity is a theoretical framework developed by Downey and Fellows for studying problems where complexity depends differently on the size n of the input and on some other parameter k that varies less in some sense. An introduction of this framework is the first part of the talk.

Then, a wide variety of model checking problems for non-flat systems under the light of parameterized complexity, taking the number of synchronized components as a parameter, is presented. In model checking, the state explosion problem occurs when one checks a non-flat system, i.e. a system implicitly described as a synchronized product of elementary subsystems.

Precise complexity measures (in the parameterized sense) for most of such parameterised model-checking problems, and evidence that the results are robust are given along the talk.