VCC

swMATH7220MaRDI QIDQ19271FDOQ19271

Author name not available (Why is that?)

Cited In (61)

• A learning-based approach to synthesizing invariants for incomplete verification engines
• Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete
• Heaps and Data Structures: A Challenge for Automated Provers
• Verifying Whiley programs with Boogie
• Formal verification of a Java component using the RESOLVE framework
• Product programs in the wild: retrofitting program verifiers to check information flow security
• Loop Invariant Symbolic Execution for Parallel Programs
• HOL-Boogie -- an interactive prover-backend for the verifying C compiler
• Title not available (Why is that?)
• Automating Induction with an SMT Solver
• A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
• Bridging the Gap: Automatic Verified Abstraction of C
• On the relation between concurrent separation logic and concurrent Kleene algebra
• Cryptographic Verification by Typing for a Sample Protocol Implementation
• Dafny: An Automatic Program Verifier for Functional Correctness
• From Total Store Order to Sequential Consistency: A Practical Reduction Theorem
• A framework for the verification of certifying computations
• Region analysis for deductive verification of C programs
• Local Reasoning for Global Invariants, Part II
• Mostly Sound Type System Improves a Foundational Program Verifier
• Automated formal analysis and verification: an overview
• Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development
• System-level non-interference of constant-time cryptography. I: Model
• A perspective on specifying and verifying concurrent modules
• Automating deductive verification for weak-memory programs
• Concerned with the unprivileged: user programs in kernel refinement
• Modular inference of subprogram contracts for safety checking
• Instrumenting a weakest precondition calculus for counterexample generation
• Taking Satisfiability to the Next Level with Z3
• Verifying the conversion into CNF in dafny
• Behavioral interface specification languages
• On automation in the verification of software barriers: experience report
• A Formalization of the C99 Standard in HOL, Isabelle and Coq
• Real-time solving of computationally hard problems using optimal algorithm portfolios
• Extending Sledgehammer with SMT Solvers
• Verification of Concurrent Systems with VerCors
• Understanding parameters of deductive verification: an empirical investigation of KeY
• RustHorn: CHC-Based Verification for Rust Programs
• Traits: correctness-by-construction for free
• Model checking boot code from AWS data centers
• An Assertional Proof of the Stability and Correctness of Natural Mergesort
• Stepwise refinement of heap-manipulating code in Chalice
• Doomed program points
• Certifying algorithms
• Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction
• Extending Sledgehammer with SMT solvers
• Leveraging compiler intermediate representation for multi- and cross-language verification
• Abstraction and subsumption in modular verification of C programs
• Shape Analysis of Low-Level C with Overlapping Structures
• A verification-driven framework for iterative design of controllers
• Matching Logic
• More SPASS with Isabelle
• Towards Complete Reasoning about Axiomatic Specifications
• Automating Theorem Proving with SMT
• The spirit of ghost code
• From Rewriting Logic, to Programming Language Semantics, to Program Verification
• Expressive modular fine-grained concurrency specification
• Title not available (Why is that?)
• ExplainHoudini: Making Houdini Inference Transparent
• Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions
• Featherweight VeriFast

This page was built for software: VCC