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

Verification of Imperative Programs by Constraint Logic Program Transformation

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

 Alberto Pettorossi
Date
Le mercredi 12 février 2014 à 10:30
Lieu
Auditorium Daniel Chemla (Bât. Institut D'Alembert)
Orateur
Alberto Pettorossi (Università di Roma Tor Vergata)

We present a method for verifying partial correctness properties of imperative programs that manipulate integers and arrays by using techniques based on the transformation of constraint logic programs (CLP). We use CLP as a metalanguage for representing (i) imperative programs, (ii) their operational semantics, and (iii) their properties. Our method incorporates into the field of program verification many techniques which have been developed during the last years in the field of program transformation. We have implemented our method in a verification system. That system, called VeriMAP, is competitive with respect to state-of-the-art tools for program verification.


À propos du LSV

Agenda des séminaires

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

mar. 19 février

Les séminaires précédents