VCC
From MaRDI portal
Software:19271
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