Point of contact
Virgile Prevosto, CEA List
Summary
Formal software verification tools are themselves programs, hence can contain bugs. Therefore,they should themselves be verified as much as possible, to minimize the Trusted Computing Base of the system. Efforts in this direction include in particular:
- The formalization of the semantics of existing programming languages (e.g. C) within proof assistants such as Coq
- The development of certified implementation of software analyzers
- Generating proof certificates from automated theorem provers, that can be independently checked
A few references
- B. Ekici et al. SMTCoq: A plug-in for integrating SMT solvers into Coq. In Computer Aided Verification (CAV), 2017.
- F. Tuong, B. Wolff. Deeply Integrating C11 Code Support into Isabelle/PIDE. In Workshop on Formal Integrated Development Environments (F-IDE), 2019
- Martin Clochard, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich. Formalizing Semantics with an Automatic Program Verifier. In 6th International Conference on Verified Software: Theories, Tools and Experiments (VSTTE), 2014.
- CompCert project