Caduceus

swMATH4625MaRDI QIDQ16796

No author found.

Related Items (54)

Practical Realisation and Elimination of an ECC-Related Software Bug Attack ⋮ Automating Induction with an SMT Solver ⋮ Challenging SMT solvers to verify neural networks ⋮ Product programs in the wild: retrofitting program verifiers to check information flow security ⋮ Proving fairness and implementation correctness of a microkernel scheduler ⋮ Practical Tactics for Separation Logic ⋮ Instrumenting a weakest precondition calculus for counterexample generation ⋮ Wave equation numerical resolution: a comprehensive mechanized proof of a C program ⋮ Trusting computations: a mechanized proof from partial differential equations to actual program ⋮ Faster and more complete extended static checking for the Java modeling language ⋮ HOL-Boogie -- an interactive prover-backend for the verifying C compiler ⋮ Modular inference of subprogram contracts for safety checking ⋮ Doomed program points ⋮ Reasoning about memory layouts ⋮ 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 ⋮ Formal verification of side-channel countermeasures using self-composition ⋮ Complete instantiation-based interpolation ⋮ Verification conditions for source-level imperative programs ⋮ Imperative Functional Programming with Isabelle/HOL ⋮ HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier ⋮ Reasoning about Assignments in Recursive Data Structures ⋮ Verification of the Schorr-Waite Algorithm – From Trees to Graphs ⋮ A program logic for resources ⋮ Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions ⋮ Correct Code Containing Containers ⋮ FM 2005: Formal Methods ⋮ Collaborative Verification and Testing with Explicit Assumptions ⋮ CPBPV: a constraint-programming framework for bounded program verification ⋮ Inferring Loop Invariants Using Postconditions ⋮ Automatic decidability and combinability ⋮ Multi-Prover Verification of Floating-Point Programs ⋮ MUNCH - Automated Reasoner for Sets and Multisets ⋮ 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 ⋮ Understanding parameters of deductive verification: an empirical investigation of KeY ⋮ 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 ⋮ Sufficient Preconditions for Modular Assertion Checking ⋮ 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 ⋮ LCF-style Platform based on Multiway Decision Graphs ⋮ Hardware-Dependent Proofs of Numerical Programs ⋮ Verifying Whiley programs with Boogie ⋮ A Rewriting Logic Semantics Approach to Modular Program Analysis ⋮ A framework for the verification of certifying computations ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)

This page was built for software: Caduceus