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.
Papers related to Multi-prover verification of C programs
- Boogie: A modular reusable verifier for object-oriented programs [barnett:fmco:2005]
- Software verification with VeriFast: Industrial case studies [philippaerts:scp:2014]