swMATH4625MaRDI QIDQ16796FDOQ16796
Author name not available (Why is that?)
Official website: http://caduceus.lri.fr/
Cited In (only showing first 100 items - show all)
- Verifying Whiley programs with Boogie
- Formal verification of side-channel countermeasures using self-composition
- LCF-style Platform based on Multiway Decision Graphs
- Dynamic boundaries: information hiding by second order framing with first order assertions
- Hardware-Dependent Proofs of Numerical Programs
- Complete instantiation-based interpolation
- Reasoning about assignments in recursive data structures
- Trusting computations: a mechanized proof from partial differential equations to actual program
- Sufficient Preconditions for Modular Assertion Checking
- FM 2005: Formal Methods
- Practical Tactics for Separation Logic
- JMLAutoTest
- Handling Polymorphism in Automated Deduction
- A refinement methodology for object-oriented programs
- Challenging SMT solvers to verify neural networks
- A Machine Checked Soundness Proof for an Intermediate Verification Language
- Towards Modular Algebraic Specifications for Pointer Programs: A Case Study
- A rewriting logic semantics approach to modular program analysis
- Inferring Loop Invariants Using Postconditions
- Imperative Functional Programming with Isabelle/HOL
- Product programs in the wild: retrofitting program verifiers to check information flow security
- Faster and more complete extended static checking for the Java modeling language
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- Automating Induction with an SMT Solver
- Abstract Interpretation of Symbolic Execution with Explicit State Updates
- Collaborative verification and testing with explicit assumptions
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- A framework for the verification of certifying computations
- Matching logic: an alternative to Hoare/Floyd logic
- Automatic decidability and combinability
- A program logic for resources
- Combining Coq and Gappa for Certifying Floating-Point Programs
- Floats and Ropes: A Case Study for Formal Numerical Program Verification
- Modular inference of subprogram contracts for safety checking
- Instrumenting a weakest precondition calculus for counterexample generation
- Static contract checking with abstract interpretation
- HOL-Boogie
- ACSL
- distcc
- JML
- Frama-C
- Omnibus
- Why3
- Alt-Ergo
- cvc3
- Gappa
- ISP
- Spec#
- TASS_
- Rascal
- ESC/Java
- MUNCH
- SANTE
- VCC
- Verification conditions for source-level imperative programs
- JACK
- Boogie
- MARMOT
- SLAB
- KIV
- VeriCool
- LOOP
- jStar
- MDGs
- Jahob
- JCrasher
- Traffic 4
- ASTREE
- Octagon
- BVD
- Haskabelle
- Understanding parameters of deductive verification: an empirical investigation of KeY
- Correct code containing containers
- Grail
- LCLint
- BoogiePL
- Jessie
- ASMKeY
- KLEE-FP
- Camelot
- SPL Conqueror
- Maximum Cardinality Matching
- RVT
- PQL
- ShortestPath
- SILF
- STLlint
- Nagini
- Doomed program points
- Reasoning about memory layouts
- 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
- FEVS: a functional equivalence verification suite for high-performance scientific computing
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Multi-prover verification of floating-point programs
- Practical realisation and elimination of an ECC-related software bug attack
- Proving fairness and implementation correctness of a microkernel scheduler
- Dafny: an automatic program verifier for functional correctness
- MUNCH -- automated reasoner for sets and multisets
This page was built for software: Caduceus
