LSV Seminar
The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Past Seminars
Proving Theorems by Program Transformation
- Date
- Tuesday, February 11 2014 at 02:00PM
- Place
- Auditorium Daniel Chemla (Bât. Institut D'Alembert)
- Speaker
- Maurizio Proietti (IASI-CNR Rome)
In this talk I will present an overview of the unfold/fold proof method, a method for proving theorems about programs based on program transformation. As a metalanguage for specifying programs and program properties we adopt constraint logic programming (CLP) and we consider a set of transformation rules (including the familiar unfolding and folding rules) that preserve the semantics of CLP programs. Then, we show how program transformation strategies can be used, similarly to theorem proving tactics, for guiding the application of the transformation rules and inferring the properties to be proved. We work out three examples: (i) the proof of predicate equivalences, applied to the verification of equality between CCS processes, (ii) the proof of first order formulas via an extension of the quantifier elimination method, and (iii) the proof of temporal properties of infinite state concurrent systems, by using a transformation strategy that performs program specialization.