

CAV 2006


english only


Currently, we model bounded asynchrony with an explicit scheduler that tells processes when they can move. However, the communications between processes is very limited. We would like to exploit this fact in order to reduce the number of possible interactions that have to be considered.
This project starts from the theory of bounded asynchrony, analysis and suggestion of reductions, and finally implementaion of enumerative and symbolic model checking algorithms.
Supervisor: Nir
We first observe that the subset of STL for which this can be accomplished is universal STL (that is, we may use only universal path quantifiers). Given a formula, we use its dual (an existential STL formula) to guide the construction of the monitor.
Supervisor: Marc
In this project, we would like to combine CEGAR into Mocha model checking.
Supervisor: Nir
We would like to compare our improved construction with the original construction. Both constructions were implemented in the same framework and are availablle for us. In order to compare these two implementations we have to separate them and modify them slightly. Then try the two different implementations on several examples.
We could then try to run them on randomly generated automata (either directly or generated from random LTL).
Supervisor: Nir
One of the greatest advantages of Scala is (from our point of view) that it is developped in the lamp group in EPFL. This means that we can have full access to the compiler sources and internal data structures (and people to talk with about them.
We have an initial implementation that takes a basic subset of the scala languages and interfaces with a software model checker called ARMC. This project will aim to extend the set of features of scala that are supported by the model checker.
Supervisor: Andrey
The aim of this project would be to explore the capabilities of CUTE and to suggest ways to integrate this technology into software model checkers.
Supervisor: Dirk
The model checkers may include:
Supervisor: Dirk
As mentioned we build models that mimic aspects of biological behavior. We then use model checking to make sure that these models reproduce experimental observations. Currently we are using BDDs and enumerative model checking. The kind of models that we build do not have long executions and it seems that the SAT approach would work well in practice.
The goal of this project is to check whether this is indeed the case. We take an existing model that is written in reactive modules and translate it to a nuSMV model (a formalism that resembles the examples that we saw with TLV). The tool nuSMV then enables us to use SAT solvers for model checking.
Supervisor: Jasmin
Shape analysis aims at abstractly representing dynamic data structures stored on the heap (like lists, trees, etc.) in a compact way. Different representations exist for those shapes. We are in particular interested in two implementations: TVLA and Hob.
In the current implementation, we are using TVLA. The goal of the miniproject is to find out how Hob can be used in Blast instead of TVLA, by comparing the two tools on examples from programs checked by Blast.
Supervisor: Gregory