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

A formalization of bisimulation-up-to techniques and their meta-theory

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

 Matteo Cimini
Date
Le mardi 21 janvier 2014 à 11:00
Lieu
Salle de Conférence (Pavillon des Jardins)
Orateur
Matteo Cimini (LIX, Ecole Polytechnique)

Bisimilarity of two processes is formally established by producing a bisimulation relation, i.e. a set of pairs of process expressions that contains those two processes and obeys certain closure properties. In many situations, particularly when the underlying labeled transition system is unbounded, these bisimulation relations can be large and even infinite.

The bisimulation-up-to technique has been developed to reduce the size of the relations to exhibit while retaining soundness, that is, the guarantee of the existence of a bisimulation. Such techniques make defining candidate relations easier and they significantly reduce the amount of work in proofs. Furthermore, they are increasingly becoming a crucial ingredient in the automated checking of bisimilarity.

In this talk, we present our experience in using the Abella theorem prover for the formalization of the meta theory of several major bisimulation-up-to techniques for the process calculi CCS and the pi-calculus. Our formalization is based on recent work on the proof theory of least and greatest fixpoints for accommodating the heavy use of coinductively defined relations and coinductive proofs about such relations. An important feature of our formalization is that our definitions and proofs are, in most cases, straightforward translations of published informal definitions, and our proofs clarify several technical details of the informal descriptions. The presence of binders, as in the pi-calculus, is notoriously a delicate aspect to treat in formal proofs but we show that the underlying proof theoretic foundations of Abella makes it possible to smoothly lift the results from CCS to the pi-calculus. This is thanks to the use of lambda-tree syntax and generic reasoning through the nabla quantifier.


À 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