Abstract
This lecture is devoted to three supplements to the year's lectures, then to answering questions sent by e-mail during the year, and finally to answering those asked in the classroom. The first supplement concerns the proof of correctness of Esterel's parallel instruction synchronizer, based on 2-adic coding and central to the semantics and implementation of the language. The proof is formalized in the Why verification system developed at Orsay, which itself calls the two SMT solvers CVC and Alt-Ergo (see March 23, 2016 lectures and seminar). The second supplement takes a closer look at the CHAM chemical machine formalism developed in 1989 with Gérard Boudol to formalize asynchronous parallelism. The third supplement presents a CADP verification exercise on a drilling system, often used as an example for formal verification.
The written questions are as follows:
- Is it possible to design highly distributed and secure systems, or even "fault-tolerant" systems, a kind of hybrid between proof and dependability?
- On protocols: there are numerous initiatives for new standards. How can we exploit the theoretical advances presented in the lecture?
- With regard to circuit optimization, can we capitalize on operations already carried out, for example when we find logical sub-expressions seen elsewhere? Can we save optimizations already carried out in suitable formats?
