Abstract. We present the Why/Krakatoa/Caduceus set of tools for deductive verication of Java and C source code.
The Why/Krakatoa/Caduceus platform can produce VCs from annotated Java and C source code REF .
The Why/Krakatoa/Caduceus platform for deductive program verification
In CAV ’07
Computer Science