KRAKATOA
From MaRDI portal
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