MJK
27 August 2010 - 10h00
Automatic and formal certification of critical systems by instrumentation of abstract interpreters (Phd Defense)
by Manuel Garnacho from VERIMAG - DCS
27 August 2010 - 10h00
Automatic and formal certification of critical systems by instrumentation of abstract interpreters (Phd Defense)
by Manuel Garnacho from VERIMAG - DCS
Abstract: This thesis deals with certification of imperative programs embedded in critical systems. Certificates establish validity of some semantics properties of programs. In our approach certificates are machine-checkable formal proofs. The challenge raised in this thesis is to automatically generate correctness proofs of programs. We followed Floyd-Hoare method for proving that these semantics properties are invariants of programs and we used Coq system to check validity of proofs.
We consider that semantics properties are discovered by static analyzers based on abstract interpretation. We proposed to instrument static analyzers such that they automatically produce certificates of their results. Instrumentation consists in associating to some functions of an analyzer proof patterns which will generate the certificates at execution time. Such instrumented static analyzers are not certified because their correctness has not been established on all their input domain. Nevertheless they are able to justify by formal proofs that each of their results meet the specification.
This framework offers the possibility to certify with a very high level of confidence the results of existing tools, even at the prototype stage. To make it practical we sought to restrict the number of functions to instrument. We draw a limited set of functions to instrument in order to transform any existing static analyzer in an automatic certification tool.
We illustrate our instrumentation principle on an static analyzer that discovers invariants of array-processing programs. This analyzer uses nontrivial abstract domains on array programs content. Thanks to our instrumentation it produces Coq checkable certificates of discovered properties on arrays content. Finally we show how make use of this instrumented static analyzer in order to certify the correctness of an inter-tasks communication protocol used in critical systems.
Jury composé de:
Laurence Pierre (Professeur UJF), Présidente proposée
Thomas Jensen (DR IRISA), Rapporteur
Olga Kouchnarenko (Professeur Univ de Franche-Comté), Rapporteur
Solange Coupet-Grimal (Univ de Provence), Examinateur
Gilles Barthe (Professeur IMDEA Software Faculty), Examinateur
Michaël Périn (MCF UJF), Directeur de thèse
