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 56 articles )

Showing results 1 to 20 of 56.
Sorted by year (citations)

1 2 3 next

  1. Müller, Peter; Schwerhoff, Malte; Summers, Alexander J.: Viper: a verification infrastructure for permission-based reasoning (2016)
  2. Totla, Nishant; Wies, Thomas: Complete instantiation-based interpolation (2016)
  3. Kirchner, Florent; Kosmatov, Nikolai; Prevosto, Virgile; Signoles, Julien; Yakobowski, Boris: Frama-C: a software analysis perspective (2015) ioport
  4. Alkassar, Eyad; Böhme, Sascha; Mehlhorn, Kurt; Rizkallah, Christine: A framework for the verification of certifying computations (2014)
  5. Betelin, V.; Galatenko, V.; Kostyukhin, K.: Controlled execution with explicit model (2014) ioport
  6. Boldo, Sylvie; Clément, François; Filli^atre, Jean-Christophe; Mayero, Micaela; Melquiond, Guillaume; Weis, Pierre: Trusting computations: a mechanized proof from partial differential equations to actual program (2014)
  7. Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with $\mathsfFlyspeck$ (2014)
  8. Almeida, J.Bacelar; Barbosa, Manuel; Pinto, Jorge S.; Vieira, Bárbara: Formal verification of side-channel countermeasures using self-composition (2013)
  9. Banerjee, Anindya; Naumann, David A.: Local reasoning for global invariants. II: Dynamic boundaries (2013)
  10. Boldo, Sylvie; Clément, François; Filli^atre, Jean-Christophe; Mayero, Micaela; Melquiond, Guillaume; Weis, Pierre: Wave equation numerical resolution: a comprehensive mechanized proof of a C program (2013)
  11. Filli^atre, Jean-Christophe: One logic to use them all (2013)
  12. Heras, Jónathan; Mata, Gadea; Romero, Ana; Rubio, Julio; Sáenz, Rubén: Verifying a plaftorm for digital imaging: a multi-tool strategy (2013)
  13. Ahrendt, Wolfgang; Dylla, Maximilian: A system for compositional verification of asynchronous objects (2012)
  14. Brumley, Billy B.; Barbosa, Manuel; Page, Dan; Vercauteren, Frederik: Practical realisation and elimination of an ECC-related software bug attack (2012)
  15. da Costa, Umberto Souza; Moreira, Anamaria Martins; Musicante, Martin A.; Souza Neto, Plácido A.: JCML: A specification language for the runtime verification of Java card programs (2012)
  16. Hatcliff, John; Leavens, Gary T.; Leino, K.Rustan M.; Müller, Peter; Parkinson, Matthew: Behavioral interface specification languages (2012)
  17. Boldo, Sylvie; Marché, Claude: Formal verification of numerical programs: from C annotated programs to mechanical proofs (2011)
  18. Frade, Maria João; Pinto, Jorge Sousa: Verification conditions for source-level imperative programs (2011)
  19. Le Goues, Claire; Leino, K.Rustan M.; Moskal, Michał: The Boogie verification debugger (tool paper) (2011) ioport
  20. Lynch, Christopher; Ranise, Silvio; Ringeissen, Christophe; Tran, Duc-Khanh: Automatic decidability and combinability (2011)

1 2 3 next