KRAKATOA
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Grail
- HOL-Boogie
- KeY-C
- LARCH
- TVOC
- SPARK
- Eiffel
- ACSL
- Instrumenting a weakest precondition calculus for counterexample generation
- Daikon
- Why3
- JML
- Spec#
- Omnibus
- Caduceus
- Frama-C
- Gappa
- cvc3
- Alt-Ergo
- TASS_
- ISP
- SIMPLIFY
- Understanding parameters of deductive verification: an empirical investigation of KeY
- JCML
- Weakest pre-condition reasoning for Java programs with JML annotations
- The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
- MUNCH
- ESC/Java
- VCC
- SANTE
- JUnit
- Formal verification of numerical programs: from C annotated programs to mechanical proofs
- TASS: the toolkit for accurate scientific software
- FEVS: a functional equivalence verification suite for high-performance scientific computing
- A system for compositional verification of asynchronous objects
- Chalice
- VeriFast
- Boogie
- JACK
- Verifying Whiley programs with Boogie
- MARMOT
- WhyML
- VeriCool
- HighSpec
- SLAB
- KeY
- KIV
- LOOP
- Deductive verification of floating-point Java programs in KeY
- Exploiting pointer analysis in memory models for deductive verification
- jStar
- A framework for the verification of certifying computations
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Trusting computations: a mechanized proof from partial differential equations to actual program
- MDGs
- Jahob
- Formal verification of side-channel countermeasures using self-composition
- Traffic 4
- A program logic for resources
- Octagon
- ASTREE
- Grasshopper
- A proof outline logic for object-oriented programming
- BVD
- Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts
- Are the logical foundations of verifying compiler prototypes matching user expectations?
- Specification and verification challenges for sequential object-oriented programs
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- Viper: a verification infrastructure for permission-based reasoning
- Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
- Behavioral interface specification languages
- Haskabelle
- Practical realisation and elimination of an ECC-related software bug attack
- Automating Induction with an SMT Solver
- Reasoning about assignments in recursive data structures
- Verification of the Schorr-Waite algorithm -- from trees to graphs
- Correct code containing containers
- Splint
- coreStar
- Dafny: an automatic program verifier for functional correctness
- Matching logic: an alternative to Hoare/Floyd logic
- Static contract checking with abstract interpretation
- A refinement methodology for object-oriented programs
- A dynamic logic for unstructured programs with embedded assertions
- Hardware-Dependent Proofs of Numerical Programs
- Houdini
- OpenJML
- Practical Tactics for Separation Logic
- An Introduction to Certificate Translation
- BoogiePL
- Jessie
- A Hoare Logic for Call-by-Value Functional Programs
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- Imperative Functional Programming with Isabelle/HOL
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- Inferring Loop Invariants Using Postconditions
- A Machine Checked Soundness Proof for an Intermediate Verification Language
- Towards Modular Algebraic Specifications for Pointer Programs: A Case Study
- Could We Have Chosen a Better Loop Invariant or Method Contract?
- Combining Coq and Gappa for Certifying Floating-Point Programs
This page was built for software: KRAKATOA
