×

KRAKATOA

swMATH ID: 3159
Software Authors: Marché, C.; Paulin-Mohring, C.; Urbain, X.
Description: 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.
Homepage: http://krakatoa.lri.fr/
Related Software: Why3; Caduceus; JML; Boogie; Spec#; Coq; z3; ESC/Java; SIMPLIFY; VeriFast; VCC; Isabelle/HOL; KeY; Eiffel; ACSL; Frama-C; cvc3; LOOP; PVS; Dafny
Referenced in: 77 Publications
all top 5

Referenced by 149 Authors

10 Marché, Claude
7 Leino, K. Rustan M.
6 Filliâtre, Jean-Christophe
4 Boldo, Sylvie
3 Böhme, Sascha
3 Jacobs, Bart
3 Melquiond, Guillaume
3 Moy, Yannick
3 Müller, Peter
3 Pinto, Jorge Sousa
3 Schulte, Wolfram
3 Wies, Thomas
3 Wolff, Burkhart
2 Ahrendt, Wolfgang
2 Aspinall, David
2 Barbosa, Manuel
2 Barthe, Gilles
2 Beringer, Lennart
2 Clément, François
2 da Costa, Umberto Souza
2 Frade, Maria João
2 Hofmann, Martin
2 Kuncak, Viktor
2 Leavens, Gary T.
2 Logozzo, Francesco
2 Loidl, Hans-Wolfgang
2 Martins Moreira, Anamaria
2 Mayero, Micaela
2 Momigliano, Alberto
2 Musicante, Martin A.
2 Paulin-Mohring, Christine
2 Siegel, Stephen F.
2 Souza Neto, Plácido A.
2 Ulbrich, Mattias
2 Weis, Pierre
2 Zirkel, Timothy K.
1 Abbasi, Rosa
1 Abed, Sa’ed
1 Aït Mohamed, Otmane
1 Alkassar, Eyad
1 Ayad, Ali
1 Bacelar Almeida, José
1 Banerjee, Anindya
1 Beckert, Bernhard
1 Bobot, François
1 Böhl, Florian
1 Bouillaguet, Charles
1 Bouillaguet, Quentin
1 Boulmé, Sylvain
1 Bouquet, Fabrice
1 Brumley, Billy Bob
1 Bubel, Richard
1 Bulwahn, Lukas
1 Capretta, Venanzio
1 Chalin, Patrice
1 Ciaffaglione, Alberto
1 Collavizza, Hélène
1 Conchon, Sylvain
1 Dadeau, Frédéric
1 Dailler, Sylvain
1 Darulova, Eva
1 Daum, Matthias
1 de Boer, Frank S.
1 Dörrenbächer, Jan
1 Dross, Claire
1 Dylla, Maximilian
1 Eilers, Marco
1 Ellison, Chucky
1 Erkök, Levent
1 Fähndrich, Manuel
1 Felty, Amy P.
1 Furia, Carlo Alberto
1 Gast, Holger
1 Giorgino, Mathieu
1 Gladisch, Christoph D.
1 Grandy, Holger
1 Greiner, Simon
1 Groslambert, Julien
1 Haftmann, Florian
1 Hähnle, Reiner
1 Hatcliff, John
1 Hauzar, David
1 Hernádvölgyi, István T.
1 Hoenicke, Jochen
1 Jaffar, Joxan
1 Kaliszyk, Cezary
1 Klebanov, Vladimir
1 Knüppel, Alexander
1 Krauss, Alexander
1 Kunz, César
1 Liquori, Luigi
1 Lourenço, Cláudio Belo
1 Madlener, Ken
1 Matthes, Ralph
1 Matwin, Stan
1 McCreight, Andrew
1 Mehlhorn, Kurt
1 Meier, Severin
1 Meyer, Bertrand
1 Miculan, Marino
...and 49 more Authors

Referencing Publications by Year