KRAKATOA

swMATH3159MaRDI QIDQ15691FDOQ15691

Author name not available (Why is that?)

Official website: http://krakatoa.lri.fr/

Cited In (only showing first 100 items - show all)

• Inferring Loop Invariants Using Postconditions
• Automating Induction with an SMT Solver
• Abstract Interpretation of Symbolic Execution with Explicit State Updates
• HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
• Matching logic: an alternative to Hoare/Floyd logic
• Automatic decidability and combinability
• Using First-Order Theorem Provers in the Jahob Data Structure Verification System
• Combining Coq and Gappa for Certifying Floating-Point Programs
• Static contract checking with abstract interpretation
• Grail
• HOL-Boogie
• KeY-C
• LARCH
• TVOC
• SPARK
• Eiffel
• ACSL
• Daikon
• Caduceus
• JML
• Frama-C
• Omnibus
• Why3
• Alt-Ergo
• cvc3
• Gappa
• ISP
• Spec#
• SIMPLIFY
• TASS_
• JCML
• ESC/Java
• MUNCH
• JUnit
• SANTE
• VCC
• Verification conditions for source-level imperative programs
• A dynamic logic for deductive verification of multi-threaded programs
• JACK
• Boogie
• Chalice
• VeriFast
• MARMOT
• HighSpec
• KeY
• SLAB
• KIV
• WhyML
• VeriCool
• LOOP
• jStar
• MDGs
• Jahob
• Traffic 4
• ASTREE
• Grasshopper
• Octagon
• BVD
• Haskabelle
• Correct code containing containers
• Grail
• coreStar
• Splint
• Houdini
• OpenJML
• BoogiePL
• Jessie
• ASMKeY
• AstraVer
• Cibai
• Camelot
• SPL Conqueror
• Maximum Cardinality Matching
• AutoProof
• Jass
• ShortestPath
• SCiFI
• STLlint
• Specification and runtime verification of Java card programs
• JCML: A specification language for the runtime verification of Java card programs
• The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
• ANNA
• Nagini
• Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes
• Weakest pre-condition reasoning for Java programs with JML annotations
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• A system for compositional verification of asynchronous objects
• CPBPV: a constraint-programming framework for bounded program verification
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Multi-prover verification of floating-point programs
• One logic to use them all
• Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts
• Specification and verification challenges for sequential object-oriented programs
• A proof outline logic for object-oriented programming
• Dafny: an automatic program verifier for functional correctness
• MUNCH -- automated reasoner for sets and multisets
• TASS: the toolkit for accurate scientific software
• Verification, Model Checking, and Abstract Interpretation
• Verifying Whiley programs with Boogie
• Imperative Functional Programming with Isabelle/HOL

This page was built for software: KRAKATOA