The following pages link to Caduceus (Q16796):
Displayed 50 items.
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program (Q352952) (← links)
- Verification conditions for source-level imperative programs (Q465685) (← links)
- Automatic decidability and combinability (Q549666) (← links)
- Modular inference of subprogram contracts for safety checking (Q604392) (← links)
- Doomed program points (Q633286) (← links)
- Reasoning about memory layouts (Q633298) (← links)
- Product programs in the wild: retrofitting program verifiers to check information flow security (Q832225) (← links)
- Proving fairness and implementation correctness of a microkernel scheduler (Q835766) (← links)
- CPBPV: a constraint-programming framework for bounded program verification (Q968353) (← links)
- Instrumenting a weakest precondition calculus for counterexample generation (Q1648649) (← links)
- Understanding parameters of deductive verification: an empirical investigation of KeY (Q1791175) (← links)
- Formal verification of numerical programs: from C annotated programs to mechanical proofs (Q1949765) (← links)
- TASS: the toolkit for accurate scientific software (Q1949767) (← links)
- FEVS: a functional equivalence verification suite for high-performance scientific computing (Q1949768) (← links)
- A system for compositional verification of asynchronous objects (Q1951610) (← links)
- Verifying Whiley programs with Boogie (Q2102933) (← links)
- A framework for the verification of certifying computations (Q2351144) (← links)
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) (Q2351415) (← links)
- Trusting computations: a mechanized proof from partial differential equations to actual program (Q2398899) (← links)
- Formal verification of side-channel countermeasures using self-composition (Q2442950) (← links)
- A program logic for resources (Q2463560) (← links)
- Faster and more complete extended static checking for the Java modeling language (Q2655328) (← links)
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler (Q2655335) (← links)
- Practical Realisation and Elimination of an ECC-Related Software Bug Attack (Q2890003) (← links)
- Automating Induction with an SMT Solver (Q2891425) (← links)
- Reasoning about Assignments in Recursive Data Structures (Q2999318) (← links)
- Verification of the Schorr-Waite Algorithm – From Trees to Graphs (Q3003486) (← links)
- Correct Code Containing Containers (Q3012966) (← links)
- Dafny: An Automatic Program Verifier for Functional Correctness (Q3066108) (← links)
- Matching Logic: An Alternative to Hoare/Floyd Logic (Q3067473) (← links)
- Static Contract Checking with Abstract Interpretation (Q3067530) (← links)
- A Refinement Methodology for Object-Oriented Programs (Q3067544) (← links)
- A Dynamic Logic for Unstructured Programs with Embedded Assertions (Q3067545) (← links)
- Hardware-Dependent Proofs of Numerical Programs (Q3100216) (← links)
- Challenging SMT solvers to verify neural networks (Q3164970) (← links)
- Practical Tactics for Separation Logic (Q3183539) (← links)
- Imperative Functional Programming with Isabelle/HOL (Q3543655) (← links)
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier (Q3543656) (← links)
- Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions (Q3558212) (← links)
- Inferring Loop Invariants Using Postconditions (Q3586008) (← links)
- A Machine Checked Soundness Proof for an Intermediate Verification Language (Q3599104) (← links)
- Handling Polymorphism in Automated Deduction (Q3608778) (← links)
- Towards Modular Algebraic Specifications for Pointer Programs: A Case Study (Q3608820) (← links)
- Combining Coq and Gappa for Certifying Floating-Point Programs (Q3637269) (← links)
- Floats and Ropes: A Case Study for Formal Numerical Program Verification (Q3638088) (← links)
- Abstract Interpretation of Symbolic Execution with Explicit State Updates (Q3638994) (← links)
- Collaborative Verification and Testing with Explicit Assumptions (Q4647837) (← links)
- LCF-style Platform based on Multiway Decision Graphs (Q4982624) (← links)
- A Rewriting Logic Semantics Approach to Modular Program Analysis (Q5389141) (← links)
- Sufficient Preconditions for Modular Assertion Checking (Q5452717) (← links)