KRAKATOA

The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML. We describe the basic structure of an environment for proving JAVA programs annotated with JML specifications. Our method is generic with respect to the API, and thus well suited for JAVACARD applets certification. It involves three distinct components: the WHY tool, which computes proof obligations for a core imperative language annotated with pre- and post-conditions, the CQQ proof assistant for modeling the program semantics and conducting the development of proofs, and finally the KRAKATOA tool, a translator of our own, which reads the JAVA files and produces specifications for COQ and a representation of the JAVA semantics of the JAVA program into WHY’s input language.


References in zbMATH (referenced in 89 articles )

Showing results 61 to 80 of 89.
Sorted by year (citations)
  1. McCreight, Andrew: Practical tactics for separation logic (2009)
  2. Vogels, Frédéric; Jacobs, Bart; Piessens, Frank: A machine checked soundness proof for an intermediate verification language (2009)
  3. Böhme, Sascha; Leino, K. Rustan M.; Wolff, Burkhart: HOL-Boogie -- an interactive prover for the Boogie program-verifier (2008)
  4. Bulwahn, Lukas; Krauss, Alexander; Haftmann, Florian; Erkök, Levent; Matthews, John: Imperative functional programming with Isabelle/HOL (2008)
  5. Conchon, Sylvain; Filliâtre, Jean-Christophe: Semi-persistent data structures (2008)
  6. Régis-Gianas, Yann; Pottier, François: A Hoare logic for call-by-value functional programs (2008)
  7. Stenzel, Kurt; Grandy, Holger; Reif, Wolfgang: Verification of Java programs with generics (2008)
  8. Aspinall, David; Beringer, Lennart; Hofmann, Martin; Loidl, Hans-Wolfgang; Momigliano, Alberto: A program logic for resources (2007)
  9. Barthe, Gilles; Pichardie, David; Rezk, Tamara: A certified lightweight non-interference Java bytecode verifier (2007)
  10. Bouillaguet, Charles; Kuncak, Viktor; Wies, Thomas; Zee, Karen; Rinard, Martin: Using first-order theorem provers in the Jahob data structure verification system (2007)
  11. Chalin, Patrice: Are the logical foundations of verifying compiler prototypes matching user expectations? (2007)
  12. Ciaffaglione, Alberto; Liquori, Luigi; Miculan, Marino: Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts (2007)
  13. Filliâtre, Jean-Christophe; Marché, Claude: The Why/Krakatoa/Caduceus platform for deductive program verification (2007) ioport
  14. Leavens, Gary T.; Leino, K. Rustan M.; Müller, Peter: Specification and verification challenges for sequential object-oriented programs (2007)
  15. Leino, K. Rustan M.; Schulte, Wolfram: A verifying compiler for a multi-threaded object-oriented language (2007)
  16. Logozzo, Francesco: Cibai: An abstract interpretation-based static analyzer for modular analysis and verification of Java classes (2007)
  17. Marché, Claude: Towards modular algebraic specifications for pointer programs: A case study (2007)
  18. Jaffar, Joxan; Santosa, Andrew E.; Voicu, Răzvan: A CLP method for compositional and intermittent predicate abstraction (2006)
  19. Bouquet, Fabrice; Dadeau, Frédéric; Groslambert, Julien: Checking JML specifications with B machines (2005)
  20. Burdy, Lilian; Cheon, Yoonsik; Cok, David R.; Ernst, Michael D.; Kiniry, Joseph R.; Leavens, Gary T.; Leino, K. Rustan M.; Poll, Erik: An overview of JML tools and applications (2005) ioport