VCC

swMATH7220MaRDI QIDQ19271FDOQ19271

Author name not available (Why is that?)

Cited In (61)

• Dynamic boundaries: information hiding by second order framing with first order assertions
• Featherweight VeriFast
• ExplainHoudini: making Houdini inference transparent
• A learning-based approach to synthesizing invariants for incomplete verification engines
• RustHorn: CHC-based verification for Rust programs
• Heaps and Data Structures: A Challenge for Automated Provers
• Extending Sledgehammer with SMT solvers
• 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
• Mostly sound type system improves a foundational program verifier
• HOL-Boogie -- an interactive prover-backend for the verifying C compiler
• 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
• Taking satisfiability to the next level with Z3 (abstract)
• On the relation between concurrent separation logic and concurrent Kleene algebra
• Cryptographic Verification by Typing for a Sample Protocol Implementation
• Automating theorem proving with SMT
• A framework for the verification of certifying computations
• Matching logic
• Region analysis for deductive verification of C programs
• Automated formal analysis and verification: an overview
• Two-level mixed verification method of C-light programs in terms of safety logic
• System-level non-interference of constant-time cryptography. I: Model
• Shape analysis of low-level C with overlapping structures
• 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
• Verifying the conversion into CNF in dafny
• Behavioral interface specification languages
• Error-tracing axiomatic semantics for C-kernel
• On automation in the verification of software barriers: experience report
• From total store order to sequential consistency: a practical reduction theorem
• Real-time solving of computationally hard problems using optimal algorithm portfolios
• Understanding parameters of deductive verification: an empirical investigation of KeY
• Bugs, moles and skeletons: symbolic reasoning for software development
• Traits: correctness-by-construction for free
• Model checking boot code from AWS data centers
• Local reasoning for global invariants. II: Dynamic boundaries
• From rewriting logic, to programming language semantics, to program verification
• 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
• Proof pearl: proving a simple von Neumann machine Turing complete
• Abstraction and subsumption in modular verification of C programs
• A verification-driven framework for iterative design of controllers
• Loop invariant symbolic execution for parallel programs
• A formalization of the C99 standard in HOL, Isabelle and Coq
• More SPASS with Isabelle
• Dafny: an automatic program verifier for functional correctness
• Towards Complete Reasoning about Axiomatic Specifications
• Verification of concurrent systems with VerCors
• The spirit of ghost code
• Expressive modular fine-grained concurrency specification
• An assertional proof of the stability and correctness of Natural Mergesort

This page was built for software: VCC