Mini Projects

Model checking bounded asynchrony

In order to build models that mimic aspects of biological behavior we have developed a notion of concurrency called bounded asynchrony. As its name suggests, bounded asynchrony allows processes to move asynchronously however keeps the distance between them bounded so that the processes do not drift apart and make more or less the same number of moves.

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

Translate USTL to monitors

We have learned that Safe Temporal Logic corresponds to repeated reachability. In addition, we know that monitors are used to transform general safety requirements to invariants. In this project we combine these two. Our aim is to write a translator that receives a universal STL formula as input and produces a reactive module monitor as output.

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

Predicate Abstraction for Safety in Mocha

Counter example guided abstraction refinement (CEGAR) is one of the most prominent approaches in model checking. The idea is to start model checking from a very abstract model that includes almost no details. The abstract model is a safe approximation of the concrete model, namely, if the abstract model is safe then so is the concrete model. Now, if the abstract model is unsafe, model checking produces a counter example. This counter example may either be a real counter example that is then reported to the user or a spurious counter example. In the case of a spurious counter example, we try to use the counter example in order to refine the model. We add information that would prevent the model checker from rediscovering the same counter example again.

In this project, we would like to combine CEGAR into Mocha model checking.

Supervisor: Nir

Comparing Deterministic Automata

Recently we have proposed an improved algorithm for determinization of automata on infinite words. This construction is important for several decision procedures of logics such as mu-calculus, CTL^*, solution of games, and reasoning about tree automata.

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

Verifying Compiler for Scala

Scala is a modern multi-paradigm programming language designed to express common programming patterns in a concise, elegant, and type-safe way. It smoothly integrates features of object-oriented and functional languages.

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

Working out CUTE

CUTE is an automatic testing tool. It analyzes the structure of a program in order to produce tests that explore all execution paths of the program. It can be used to explore all execution paths of the program much like a model checker.

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

Software Model Checking

In this project we would evaluate and compare several software model checkers to prove safety properties of programs.

The model checkers may include:

CMBC
BOGOR
JPF(see also here)

Supervisor: Dirk

Going SAT with biological modeling

An approach that seems to be very successful in model checking in recent years is to reduce the question of reachability to bounded reachability. Instead of checking whether an error is reachable we check whether it is reachable in some number of steps. This reduction enables to replace BDDs by satisfiability solvers (SAT solvers or SAT).

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 nu-SMV model (a formalism that resembles the examples that we saw with TLV). The tool nu-SMV then enables us to use SAT solvers for model checking.

Supervisor: Jasmin

Compare HOB and TVLA on examples produced by Blast

Blast is a software model checker developped in our group. Traditionally, model checkers are very good at handling control intensive programs but not so good when it comes to handle data. In order to tackle this problem, we have extended the Blast with shape analysis in order to have a more precise abstraction of the heap (i.e., the data structures used by the program).

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 mini-project 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