Caduceus

swMATH4625MaRDI QIDQ16796FDOQ16796

Author name not available (Why is that?)

Cited In (54)

• Inferring Loop Invariants Using Postconditions
• Verifying Whiley programs with Boogie
• Imperative Functional Programming with Isabelle/HOL
• Product programs in the wild: retrofitting program verifiers to check information flow security
• Formal verification of side-channel countermeasures using self-composition
• Practical Realisation and Elimination of an ECC-Related Software Bug Attack
• A Refinement Methodology for Object-Oriented Programs
• 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
• Dafny: An Automatic Program Verifier for Functional Correctness
• A Dynamic Logic for Unstructured Programs with Embedded Assertions
• Abstract Interpretation of Symbolic Execution with Explicit State Updates
• HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
• A framework for the verification of certifying computations
• Automatic decidability and combinability
• A program logic for resources
• Hardware-Dependent Proofs of Numerical Programs
• Complete instantiation-based interpolation
• 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
• Trusting computations: a mechanized proof from partial differential equations to actual program
• Multi-Prover Verification of Floating-Point Programs
• Verification conditions for source-level imperative programs
• Sufficient Preconditions for Modular Assertion Checking
• Understanding parameters of deductive verification: an empirical investigation of KeY
• Matching Logic: An Alternative to Hoare/Floyd Logic
• MUNCH - Automated Reasoner for Sets and Multisets
• 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
• Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions
• A Rewriting Logic Semantics Approach to Modular Program Analysis
• CPBPV: a constraint-programming framework for bounded program verification
• FEVS: a functional equivalence verification suite for high-performance scientific computing
• Reasoning about Assignments in Recursive Data Structures
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Practical Tactics for Separation Logic
• Handling Polymorphism in Automated Deduction
• Collaborative Verification and Testing with Explicit Assumptions
• Static Contract Checking with Abstract Interpretation
• Challenging SMT solvers to verify neural networks
• Verification of the Schorr-Waite Algorithm – From Trees to Graphs
• Proving fairness and implementation correctness of a microkernel scheduler
• Correct Code Containing Containers
• A Machine Checked Soundness Proof for an Intermediate Verification Language
• TASS: the toolkit for accurate scientific software
• Formal verification of numerical programs: from C annotated programs to mechanical proofs
• Towards Modular Algebraic Specifications for Pointer Programs: A Case Study
• LCF-style Platform based on Multiway Decision Graphs
• FM 2005: Formal Methods

This page was built for software: Caduceus