Caduceus used to be a verification tool for C programs built on top of the Why tool, in the ProVal team, by Jean-Christophe Filliâtre and Claude Marché. Caduceus is now obsolete and fully subsumed by Frama-C.
Keywords for this software
References in zbMATH (referenced in 63 articles )
Showing results 61 to 63 of 63.
- Filliâtre, Jean-Christophe; Marché, Claude: The Why/Krakatoa/Caduceus platform for deductive program verification (2007) ioport
- Marché, Claude: Towards modular algebraic specifications for pointer programs: A case study (2007)
- Andronick, June; Chetali, Boutheina; Paulin-Mohring, Christine: Formal verification of security properties of smart card embedded source code (2005)