Caduceus

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

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 63 articles )

Showing results 61 to 63 of 63.
Sorted by year (citations)
  1. Filliâtre, Jean-Christophe; Marché, Claude: The Why/Krakatoa/Caduceus platform for deductive program verification (2007) ioport
  2. Marché, Claude: Towards modular algebraic specifications for pointer programs: A case study (2007)
  3. Andronick, June; Chetali, Boutheina; Paulin-Mohring, Christine: Formal verification of security properties of smart card embedded source code (2005)