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
Verification of Imperative Programs by Constraint Logic Program Transformation
- Date
- Wednesday, February 12 2014 at 10:30AM
- Place
- Auditorium Daniel Chemla (Bât. Institut D'Alembert)
- Speaker
- 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.