Cited in
(only showing first 100 items - show all)- Expressive modular fine-grained concurrency specification
- An assertional proof of the stability and correctness of Natural Mergesort
- 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
- On the relation between concurrent separation logic and concurrent Kleene algebra
- Taking satisfiability to the next level with Z3 (abstract)
- Cryptographic Verification by Typing for a Sample Protocol Implementation
- Automating theorem proving with SMT
- A framework for the verification of certifying computations
- Matching logic
- Dynamic boundaries: information hiding by second order framing with first order assertions
- 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
- Dafny
- HOL-Boogie
- ArcAngel
- KRAKATOA
- Eiffel
- ACSL
- Caduceus
- Frama-C
- Why3
- Alt-Ergo
- Spec#
- SPARKSkein
- Rodin
- ESC/Java
- ESC4
- Boogie
- Chalice
- VeriFast
- ASPIER
- HighSpec
- InvGen
- Amphion
- Checkfence
- SLAyer
- FeaVer
- NaCl
- Toolchain
- WhyML
- VeriCool
- VeriSmall
- Viper
- GPUVerify
- jStar
- VerCors
- Jahob
- SatAbs
- Traffic 4
- SymDiff
- YOGI
- Joogie
- BVD
- GNATprove
- CoDeSe
- CacBDD
- c2i
- ExplainHoudini
- Houdini
- OpenJML
- Coverity
- SPHIN
- C-Light
- BoogiePL
- VACID-0
- Charge!
- SMACK
- Rocksalt
- ANaConDA
- Klocwork
- Rust
- POSIX Lexing
- VST-Floyd
- Finite Automata HF
- Hereditarily Finite Sets
- SPL Conqueror
- Maximum Cardinality Matching
- Robbins Conjecture
This page was built for software: VCC
