Room 206 (2nd floor, badged access)
9 November 2023 - 14h00
Automating software verification with respect to strong specifications
by Gidon Ernst from Ludwig-Maximilians-University of Munich
Abstract: Proving functional correctness of software with respect to specifications of application-specific requirements requires one to define these specifications in the first place, to come up with coupling relations that connect the concrete state space of the implementation to its abstract counterpart, and to prove that this correspondence is maintained by the computation of the system.
In this talk I will sketch ideas how to automate this process. In the main technical part of the talk I will present an approach that quickly and fully automatically discovers (distributive) lemmas typically needed for the core part of the proofs. The approach, called LemmaCalc, leverages well-known transformations, originally conceived for the optimization of functional programs (such as fusion and accumulator removal), to that purpose.
Gidon is a potential candidate to a CNRS research position at Verimag.
