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.

Français