Le séminaire du LSV

Le séminaire du LSV a lieu le mardi à 11h00. Le lieu habituel est la salle de conférences au Pavillon des Jardins (plan d'accès). Pour être informé par email des prochains séminaires, contacter Stéphane Le Roux and Matthias Fuegger.

Le séminaire du LSV est public et ne nécessite aucune inscription préalable.

Séminaires passés

Regular Model Checking using nondeterministic tree automata

Visiter le site web pour cet événement | Exporter cet événement au format iCalendar

Date
Le mardi 08 juillet 2008 à 11:00
Lieu
Salle de Conférence (Pavillon des Jardins)
Orateur
Tomas Vojnar (FIT Technical University Brno)

Abstract regular tree model checking (ARTMC) is a generic technique for automated formal verification of various kinds of infinite-state and parameterised systems, including, e.g., parameterised protocols or programs manipulating dynamic, pointer-linked data structures. ARTMC is based on representing infinite sets of configurations of the examined systems by finite tree automata whose efficient manipulation is thus crucial for an overall efficiency of ARTMC. It turns out that a significant bottleneck in dealing with finite tree automata is the need to determinise them when checking inclusion or within the classical automata minimisation procedure. In the talk, we will present several recent works whose aim is to eliminate the need to determinise the automata being handled in ARTMC. In particular, we will present methods for an antichain-based inclusion checking on nondeterministic tree automata and efficient methods for reducing the size of such automata based on various types of upward, downward, and composed (bi)simulations. According to our experimental results, these techniques really very significantly improve the performance of ARTMC.

The talk is based on joint work with Ahmed Bouajjani and Tayssir Touili from LIAFA, Peter Habermehl from LSV, Parosh Aziz Abdulla and Lisa Kaati from Uppsala, and Lukas Holik from FIT BUT.


À propos du LSV

Agenda des séminaires

Exporter l'agenda au format iCalendar | Les séminaires précédents

No entries.

Les séminaires précédents