The Why/Krakatoa/Caduceus Platform for Deductive Program Verification
By Jean-Christophe Filliâtre, Claude Marché. International Conference on Computer Aided Verification, 2007
426 citations recorded by the source corpus.
Subfields: Artificial Intelligence, Computational Theory and Mathematics
View Paper: https://www.semanticscholar.org/paper/929c485bcba7dc030d107aa5771bdf3bc0550715
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Artificial Intelligence
In Computational Theory and Mathematics
Citations in the corpus
- Challenging SMT solvers to verify neural networks (2012, neutral): “, ACL2 [22], Caduceus [10], software model checkers like SMT-CBMC [1], and unit test generators like CREST [15].”
- Why3: Shepherd Your Herd of Provers (2011, methodology): “We also plan to use WhyML as an intermediate language for program verification, in the spirit of the former Why platform [14] or Boogie [1].”
- ACSL: ANSI/ISO C Specification Language (2008, methodology): “The main inspiration for this language comes from the specification language of the CADUCEUS tool [8, 9] for deductive verification of behavioral properties of C programs.”