Multi-prover verification of C programs

Jean-Christophe Filliâtre, Claude Marché
[doi] [Google Scholar] [DBLP] [Citeseer]
Read: 16 October 2019

Sixth International Conference on Formal Engineering Methods
LNCS, volume 3308
Pages 15-29
Topic(s): tools verification
Note(s): Why3 verifier
Papers: cuoq:sefm:2012

Describes “Caduceus”: a tool to translate C code to the WhyML specification language lowering imperative code to pure code and handling pointers. Introduced the specification notation that later became ACSL and a forerunner to Frama-C.

Given current understanding of undefined behaviour and implementation defined behaviour in C, the translation from C looks a bit naïve.