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 1 to 20 of 89.
Sorted by year (citations)

1 2 3 4 5 next

  1. Abbasi, Rosa; Schiffl, Jonas; Darulova, Eva; Ulbrich, Mattias; Ahrendt, Wolfgang: Deductive verification of floating-point Java programs in KeY (2021)
  2. Bouillaguet, Quentin; Bobot, François; Sighireanu, Mihaela; Yakobowski, Boris: Exploiting pointer analysis in memory models for deductive verification (2019)
  3. Dailler, Sylvain; Hauzar, David; Marché, Claude; Moy, Yannick: Instrumenting a weakest precondition calculus for counterexample generation (2018)
  4. Grigoriy Volkov, Mikhail Mandrykin, Denis Efremov: Lemma Functions for Frama-C: C Programs as Proofs (2018) arXiv
  5. Knüppel, Alexander; Thüm, Thomas; Pardylla, Carsten Immanuel; Schaefer, Ina: Understanding parameters of deductive verification: an empirical investigation of key (2018)
  6. Belo Lourenço, Cláudio; João Frade, Maria; Sousa Pinto, Jorge: Formalizing single-assignment program verification: an adaptation-complete approach (2016)
  7. Müller, Peter; Schwerhoff, Malte; Summers, Alexander J.: Viper: a verification infrastructure for permission-based reasoning (2016)
  8. Totla, Nishant; Wies, Thomas: Complete instantiation-based interpolation (2016)
  9. Kirchner, Florent; Kosmatov, Nikolai; Prevosto, Virgile; Signoles, Julien; Yakobowski, Boris: Frama-C: a software analysis perspective (2015) ioport
  10. Tschannen, J.; Furia, CA; Nordio, M.; Polikarpova, N.: AutoProof: Auto-active Functional Verification of Object-oriented Programs (2015) arXiv
  11. Alkassar, Eyad; Böhme, Sascha; Mehlhorn, Kurt; Rizkallah, Christine: A framework for the verification of certifying computations (2014)
  12. Betelin, V.; Galatenko, V.; Kostyukhin, K.: Controlled execution with explicit model (2014) ioport
  13. Böhl, Florian; Greiner, Simon; Scheidecker, Patrik: Proving correctness and security of two-party computation implemented in Java in presence of a semi-honest sender (2014)
  14. Boldo, Sylvie; Clément, François; Filliâtre, Jean-Christophe; Mayero, Micaela; Melquiond, Guillaume; Weis, Pierre: Trusting computations: a mechanized proof from partial differential equations to actual program (2014)
  15. de Boer, Frank S.; de Gouw, Stijn: Combining monitoring with run-time assertion checking (2014) ioport
  16. Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with (\mathsfFlyspeck) (2014)
  17. Almeida, J. Bacelar; Barbosa, Manuel; Pinto, Jorge S.; Vieira, Bárbara: Formal verification of side-channel countermeasures using self-composition (2013)
  18. Banerjee, Anindya; Naumann, David A.: Local reasoning for global invariants. II: Dynamic boundaries (2013)
  19. Beckert, Bernhard; Klebanov, Vladimir: A dynamic logic for deductive verification of multi-threaded programs (2013)
  20. Boldo, Sylvie; Clément, François; Filliâtre, Jean-Christophe; Mayero, Micaela; Melquiond, Guillaume; Weis, Pierre: Wave equation numerical resolution: a comprehensive mechanized proof of a C program (2013)

1 2 3 4 5 next