# 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.