The Merriam-Webster dictionnary defines an assumption as “a fact or statement (as a proposition, axiom, postulate, or notion) taken for granted”. This is indeed the role that assumptions play in formal verification of programs, as performed in Frama-C platform or GNATprove. Assumptions may either be related to the proof of a single function (like “this other function called should respect its contract”) or related to the proof methodology and tools used (like “the type system of the program should not be bypassed”). The problem is that the overall verification of a software, as done in certification, should ultimately discharge such assumptions, either by some other automatic verification activity, or by manual review. Because assumptions are not taken for granted in software certification.
Researchers have started taking assumptions seriously, in particular for certification. See for example this paper at FM 2012, and the paper “Tool Integration with the Evidential Tool Bus” (or ETB) from SRI. The Frama-C platform already has a built-in mechanism for storing the assumptions on which individual proofs of properties depend (see their paper “Combining Analyses for C Program Verification”). The SPARK technology also provides a way to summarize how all properties of interest were checked, inclusing manual review, so that there are no pending assumptions besides the implicit ones depending on the approach.
What we have been discussing last Monday with Simon Cruanes (a coauthor of the SRI paper above) and Frama-C team members Julien Signoles and Virgile Prevosto, is how to combine verification results from different tools (some doing formal verification, some doing dynamic verification like testing) on different languages (Ada and C) in a way that no assumption is forgotten. The Datalog language used to express constraints in the ETB seems a good start. We are now going to experiment with the ETB and its Datalog language to see if that allows us to express and check the verification constraints mandated by various certification standards, for our tools.
Note that the CEA will host soon Maria Christakis (a coauthor of the FM 2012 paper above) and SRI researchers Natarajan Shankar and Sam Owre, which whom we’ll discuss this topic. To be continued.
