The following pages link to VCC (Q19271):
Displayed 50 items.
- Certifying algorithms (Q465678) (← links)
- The spirit of ghost code (Q518394) (← links)
- Modular inference of subprogram contracts for safety checking (Q604392) (← links)
- Doomed program points (Q633286) (← links)
- Concerned with the unprivileged: user programs in kernel refinement (Q736848) (← links)
- Leveraging compiler intermediate representation for multi- and cross-language verification (Q784116) (← links)
- Formal verification of a Java component using the RESOLVE framework (Q831953) (← links)
- Product programs in the wild: retrofitting program verifiers to check information flow security (Q832225) (← links)
- A perspective on specifying and verifying concurrent modules (Q1648035) (← links)
- Instrumenting a weakest precondition calculus for counterexample generation (Q1648649) (← links)
- A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data (Q1739908) (← links)
- Understanding parameters of deductive verification: an empirical investigation of KeY (Q1791175) (← links)
- Stepwise refinement of heap-manipulating code in Chalice (Q1941869) (← links)
- Real-time solving of computationally hard problems using optimal algorithm portfolios (Q2043446) (← links)
- Model checking boot code from AWS data centers (Q2050104) (← links)
- Verifying Whiley programs with Boogie (Q2102933) (← links)
- Abstraction and subsumption in modular verification of C programs (Q2147702) (← links)
- Verifying the conversion into CNF in dafny (Q2148786) (← links)
- Traits: correctness-by-construction for free (Q2165220) (← links)
- A learning-based approach to synthesizing invariants for incomplete verification engines (Q2208307) (← links)
- Region analysis for deductive verification of C programs (Q2216720) (← links)
- Automating deductive verification for weak-memory programs (Q2324213) (← links)
- A verification-driven framework for iterative design of controllers (Q2335947) (← links)
- On the relation between concurrent separation logic and concurrent Kleene algebra (Q2347904) (← links)
- A framework for the verification of certifying computations (Q2351144) (← links)
- On automation in the verification of software barriers: experience report (Q2351145) (← links)
- Extending Sledgehammer with SMT solvers (Q2351158) (← links)
- System-level non-interference of constant-time cryptography. I: Model (Q2417947) (← links)
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler (Q2655335) (← links)
- Automated formal analysis and verification: an overview (Q2871577) (← links)
- Behavioral interface specification languages (Q2875082) (← links)
- Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete (Q2879266) (← links)
- Automating Induction with an SMT Solver (Q2891425) (← links)
- Loop Invariant Symbolic Execution for Parallel Programs (Q2891433) (← links)
- Taking Satisfiability to the Next Level with Z3 (Q2908472) (← links)
- Bridging the Gap: Automatic Verified Abstraction of C (Q2914735) (← links)
- More SPASS with Isabelle (Q2914754) (← links)
- Mostly Sound Type System Improves a Foundational Program Verifier (Q2938037) (← links)
- From Rewriting Logic, to Programming Language Semantics, to Program Verification (Q2945730) (← links)
- (Q2979813) (← links)
- (Q2979840) (← links)
- Dafny: An Automatic Program Verifier for Functional Correctness (Q3066108) (← links)
- Towards Complete Reasoning about Axiomatic Specifications (Q3075488) (← links)
- ExplainHoudini: Making Houdini Inference Transparent (Q3075491) (← links)
- Cryptographic Verification by Typing for a Sample Protocol Implementation (Q3092172) (← links)
- Featherweight VeriFast (Q3196351) (← links)
- Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions (Q3558212) (← links)
- Shape Analysis of Low-Level C with Overlapping Structures (Q3656885) (← links)
- (Q4600770) (← links)
- Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction (Q4647844) (← links)