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 41 to 60 of 89.
Sorted by year (citations)
  1. Tafat, Asma; Boulmé, Sylvain; Marché, Claude: A refinement methodology for object-oriented programs (2011)
  2. Tamalet, Alejandro; Madlener, Ken: Reasoning about assignments in recursive data structures (2011)
  3. Ulbrich, Mattias: A dynamic logic for unstructured programs with embedded assertions (2011)
  4. Ayad, Ali; Marché, Claude: Multi-prover verification of floating-point programs (2010)
  5. Böhme, Sascha; Moskal, Michał; Schulte, Wolfram; Wolff, Burkhart: HOL-Boogie -- an interactive prover-backend for the verifying C compiler (2010)
  6. Collavizza, Hélène; Rueher, Michel; Van Hentenryck, Pascal: CPBPV: a constraint-programming framework for bounded program verification (2010)
  7. du Bousquet, Lydie; Ledru, Yves; Maury, Olivier; Oriat, Catherine; Lanet, Jean-Louis: Reusing a JML specification dedicated to verification for testing, and vice-versa: Case studies (2010) ioport
  8. Furia, Carlo Alberto; Meyer, Bertrand: Inferring loop invariants using postconditions (2010)
  9. Gast, Holger: Reasoning about memory layouts (2010)
  10. Hoenicke, Jochen; Leino, K. Rustan M.; Podelski, Andreas; Schäf, Martin; Wies, Thomas: Doomed program points (2010)
  11. Leino, K. Rustan M.: Dafny: an automatic program verifier for functional correctness (2010)
  12. Moy, Yannick; Marché, Claude: Modular inference of subprogram contracts for safety checking (2010)
  13. Piskac, Ruzica; Kuncak, Viktor: MUNCH -- automated reasoner for sets and multisets (2010)
  14. Abed, Sa’ed; Mohamed, Otmane Ait: LCF-style platform based on multiway decision graphs (2009)
  15. Barthe, Gilles; Kunz, César: An introduction to certificate translation (2009)
  16. Boldo, Sylvie; Filliâtre, Jean-Christophe; Melquiond, Guillaume: Combining Coq and Gappa for certifying floating-point programs (2009)
  17. Bubel, Richard; Hähnle, Reiner; Weiß, Benjamin: Abstract interpretation of symbolic execution with explicit state updates (2009)
  18. da Costa, Umberto Souza; Martins Moreira, Anamaria; Musicante, Martin A.; Souza Neto, Plácido A.: Specification and runtime verification of Java card programs (2009)
  19. Daum, Matthias; Dörrenbächer, Jan; Wolff, Burkhart: Proving fairness and implementation correctness of a microkernel scheduler (2009)
  20. Gladisch, Christoph: Could we have chosen a better loop invariant or method contract? (2009)