9:30-10:00 Emmanuel Filiot (ULB). Towards Efficient Synthesis of LTL Specifications.

10:00-10:30 Laurent Doyen (LSV, CNRS, ENS Cachan), Raffaella Gentilini (ULB, University of Perugia), Jean-François Raskin (ULB). Faster Pseudo-Polynomial Algorithms for Mean-Payoff Games.

10:30-11:00

11:00-11:30 Theofrastos Mantadelis (KUL), Gerda Janssens (KUL). Compressing Boolean Formulas.

11:30-12:00 Bernard Boigelot (ULg), Jean-François Degbomont (ULg), Julien Brusten (ULg). Implicit Real Vector Automata.

12:00-12:30 José Vander Meulen (UCL), Charles Pecheur (UCL). Combining Partial Order Reduction with Symbolic Model Checking.

12:30-14:00

14:00-15:00 Hubert Garavel (INRIA-LIG/VASY). An Overview of CADP 2009.

15:00-15:30

15:30-16:00 Andreas Classen (FUNDP), Patrick Heymans (FUNDP), Pierre-Yves Schobbens (FUNDP), Axel Legay (IRISA/INRIA Rennes), Jean-François Raskin (ULB). Model Checking Lots of Systems: Efficient Verification of Temporal Properties in Software Product Lines.

16:00-16:30 Bart Jacobs (KUL), Jan Smans (KUL), Frank Piessens (KUL). VeriFast: a Simple, Sound Verifier for Rich Separation Logic Contracts.

16:30-17:00 Pierre-Yves Schobbens (FUNDP), Hubert Toussaint (FUNDP). Formalization and Verification of Access Control Policies.

In this talk, we present the LTL synthesis problem. We show how to reduce it to computing winning strategies in a safety game. The safety game is played on an arena which has a nice structure and which can be exploited by an incremental algorithm that manipulates antichains of game positions. Antichains offer a compact representation of sets of game positions. Although LTL synthesis is 2-exptime-complete, this symbolic representation made an implementation possible, whose preliminary results are very encouraging.

We consider two-player games played on a weighted graph with mean-payoff objectives. We present a new pseudo-polynomial algorithm for solving such games, improving the best known worst-case complexity for pseudo-polynomial mean-payoff algorithms. Our solution relies on a simple fixpoint iteration to solve the log-space equivalent problem of deciding the winner of energy games.

Reduced Ordered Binary Decision Diagrams (ROBDDs), are vastly used in formal verification, and circuit synthesize. A less known application of ROBDDs is their usage for calculating the probability of a sum of products in a DNF formula. In this work we present how to identify local structures that appear in ROBDDs that can be compressed leading to faster generation and smaller ROBDDs.

We also present an algorithm that detects prior to the ROBDD generation these localities in DNF formulas. Finally we present our promising results of its application calculating the probability of a sum of products.

This work addresses the efficient handling of non-convex real polyhedra, i.e., sets of real vectors satisfying arbitrary Boolean combinations of linear constraints. We develop a symbolic data structure for representing such sets, based on an implicit and concise encoding of a known structure, the Real Vector Automaton. The resulting formalism provides a canonical representation of non-convex polyhedra, is closed under Boolean operators, and admits an efficient decision procedure for testing the membership of a vector.

Model checking is an efficient technique for verifying properties on reactive systems. Partial-order reduction (POR) and symbolic model checking are two common approaches to deal with the state space explosion problem in model checking. Traditionally, symbolic model checking uses BDDs which can suffer from space blow-up. More recently bounded model checking (BMC) using SAT-based procedures has been used as a very successful alternative to BDDs. However, these approaches give poor results when it is applied to models with a lot of asynchronism. This talk presents two algorithms which combine partial order reduction methods and symbolic model checking techniques that allow efficient verification of temporal logic properties (LTLX) on models featuring asynchronous processes. The starting-point of our work is the two-phase algorithm (Namalesu and Gopalakrishnan) which performs partial-order reduction on process-based models.

This lecture will present the latest release of CADP (Construction and Analysis of Distributed Processes), a toolbox for formal specification, verification and performance evaluation of concurrent systems. A new version of CADP will be released soon, which delivers many enhancements added between 2006 and 2009. The major features of CADP will be presented, with a special focus on the new features in CADP 2009.

Hubert Garavel heads the VASY research group at INRIA. His main research interest is about the application of formal methods to the development of complex systems. He is mostly interested in formal methods at work. CADP is his main piece of software.

In product line engineering, systems are developed in families and differences between family members are expressed in terms of features. Formal modelling and verification is an important issue in this context as more and more critical systems are developed this way. Since the number of systems in a family can be exponential in the number of features, two major challenges are the scaleable modelling and the efficient verification of system behaviour. Currently, the few attempts to address them fail to recognise the importance of features as a unit of difference, or do not offer means for automated verification.

In this paper, we tackle those challenges at a fundamental level. We first extend transition systems with features in order to describe the combined behaviour of an entire system family. We then define and implement a model checking technique that allows to verify such transition systems against temporal properties. An empirical evaluation shows substantial gains over classical approaches.

VeriFast is a program verification tool for single-threaded and multi-threaded C and Java programs that we are developing. Successful verification guarantees absence of hard to catch programming errors such as data races and memory leaks, as well as compliance with rich preconditions and postconditions specified by the programmer in source code annotations in a form of separation logic. The tool takes an annotated program as input and reports success or failure without further interaction. Verification time is predictable and low. We have verified various challenging programs, including a multiple-compare-and-swap implementation, a lock-coupling set, and a program that dynamically loads and unloads C modules, mimicking how the Linux kernel loads and unloads device drivers. We have developed an IDE that allows the user to step through a failed symbolic execution path, inspecting the symbolic values of locals and the symbolic heap at each point.

Secure software development is an increasingly complex task. It requires proper modeling of the desired security properties and their correct implementation in the code. It is very important to be able to guarantee that the properties specified during the requirements phase are respected in the final product and in each of its evolutions. Software is not a frozen concept, it evolves with every new customer requirement and bugfix.

As software evolves, so should the security model. But constraints, for instance client-imposed delivery time constraints (like “we require this functionnality for yesterday”), render such co-evolution of the security model and the code impossible to manage with reasonable cost. Thus changes are applied directly into code and delivered to the client without proper testing or verification. This may lead to unwanted behaviours and/or security breaches.

We propose a tool-supported methodology to help the developper to figure out what are exactly the implications of an apparent minor modification to code. We focus on access-control sections of the source code and take advantage of existing coding conventions. By extraction and formal modeling of access control-related fragment of the code, we show the developper the real security implications of the source code modification made and propose alternatives and/or corrections to make sure produced code still satisfy the security model. The tool can also be used the other way round : by extracting the security model from code and confronting it to desired properties, it can help to find the origins of existing security breaches.