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
On the Formal Analysis of Physical Systems using Theorem Proving
- Date
- Tuesday, December 18 2012 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- Vincent Aravantinos (Concordia University, Montréal)
Formal methods have been used classically for the verification of software, circuits or protocols. In most cases, verification deals with an abstraction of the underlying physical system (e.g., software verification does not involve the modelization of a computer, circuit verification does not model semi-conductors). We propose to try to verify such physical systems, focusing in particular on optical systems which have several applications (from fiber optics to quantum computer implementations). This requires the formalization of physical concepts (e.g. ray of light, lens, electromagnetic wave or photon), of the physical principles that govern them (e.g., Fermat's principle or Maxwell equations), and the derivation, from these principles, of various laws that are useful for the verification of concrete systems (e.g., Snell's law or the Uncertainty principle). We will explain how these concepts and principles can be successfully formalized (in HOL-Light) as well as the limitations of this approach.