Caduceus
From MaRDI portal
Cited in
(only showing first 100 items - show all)- HOL-Boogie
- KeY-C
- TVOC
- KRAKATOA
- ACSL
- Instrumenting a weakest precondition calculus for counterexample generation
- Why3
- JML
- Spec#
- Omnibus
- distcc
- Frama-C
- Gappa
- cvc3
- Alt-Ergo
- TASS_
- ISP
- Rascal
- Understanding parameters of deductive verification: an empirical investigation of KeY
- MUNCH
- ESC/Java
- VCC
- SANTE
- 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
- Boogie
- JACK
- Verifying Whiley programs with Boogie
- MARMOT
- VeriCool
- SLAB
- KIV
- LOOP
- 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
- JCrasher
- Octagon
- ASTREE
- BVD
- Faster and more complete extended static checking for the Java modeling language
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- 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
- LCLint
- 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
- Challenging SMT solvers to verify neural networks
- Practical Tactics for Separation Logic
- BoogiePL
- Jessie
- 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
- Dynamic boundaries: information hiding by second order framing with first order assertions
- Inferring Loop Invariants Using Postconditions
- A Machine Checked Soundness Proof for an Intermediate Verification Language
- Handling Polymorphism in Automated Deduction
- Towards Modular Algebraic Specifications for Pointer Programs: A Case Study
- Combining Coq and Gappa for Certifying Floating-Point Programs
- Floats and Ropes: A Case Study for Formal Numerical Program Verification
- Abstract Interpretation of Symbolic Execution with Explicit State Updates
- KLEE-FP
- ASMKeY
- Grail
- Camelot
- SPL Conqueror
- Maximum Cardinality Matching
- RVT
- ShortestPath
- PQL
- SILF
- STLlint
- Collaborative verification and testing with explicit assumptions
- Verification conditions for source-level imperative programs
- LCF-style Platform based on Multiway Decision Graphs
- A rewriting logic semantics approach to modular program analysis
- Sufficient Preconditions for Modular Assertion Checking
- Automatic decidability and combinability
- Nagini
- FM 2005: Formal Methods
- Multi-prover verification of floating-point programs
- MUNCH -- automated reasoner for sets and multisets
- Complete instantiation-based interpolation
This page was built for software: Caduceus
