VCC
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Dafny
- HOL-Boogie
- JDD
- BDD
- ArcAngel
- KRAKATOA
- Eiffel
- ACSL
- A perspective on specifying and verifying concurrent modules
- Instrumenting a weakest precondition calculus for counterexample generation
- Why3
- Spec#
- Caduceus
- Frama-C
- Alt-Ergo
- A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
- Understanding parameters of deductive verification: an empirical investigation of KeY
- SPARKSkein
- Rodin
- ESC/Java
- ESC4
- Stepwise refinement of heap-manipulating code in Chalice
- Chalice
- VeriFast
- Boogie
- Real-time solving of computationally hard problems using optimal algorithm portfolios
- Model checking boot code from AWS data centers
- Verifying Whiley programs with Boogie
- Abstraction and subsumption in modular verification of C programs
- Verifying the conversion into CNF in dafny
- Toolchain
- Traits: correctness-by-construction for free
- WhyML
- SLAyer
- VeriCool
- HighSpec
- InvGen
- VeriSmall
- ASPIER
- NaCl
- Checkfence
- FeaVer
- Amphion
- A learning-based approach to synthesizing invariants for incomplete verification engines
- Region analysis for deductive verification of C programs
- VerCors
- GPUVerify
- jStar
- Automating deductive verification for weak-memory programs
- A verification-driven framework for iterative design of controllers
- On the relation between concurrent separation logic and concurrent Kleene algebra
- A framework for the verification of certifying computations
- On automation in the verification of software barriers: experience report
- Extending Sledgehammer with SMT solvers
- System-level non-interference of constant-time cryptography. I: Model
- Jahob
- Traffic 4
- SatAbs
- SymDiff
- YOGI
- Joogie
- BVD
- GNATprove
- CoDeSe
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- Viper
- Automated formal analysis and verification: an overview
- Behavioral interface specification languages
- Proof pearl: proving a simple von Neumann machine Turing complete
- Automating Induction with an SMT Solver
- Loop invariant symbolic execution for parallel programs
- Taking satisfiability to the next level with Z3 (abstract)
- Bridging the Gap: Automatic Verified Abstraction of C
- More SPASS with Isabelle
- Mostly sound type system improves a foundational program verifier
- From rewriting logic, to programming language semantics, to program verification
- Error-tracing axiomatic semantics for C-kernel
- Two-level mixed verification method of C-light programs in terms of safety logic
- Dafny: an automatic program verifier for functional correctness
- Towards Complete Reasoning about Axiomatic Specifications
- ExplainHoudini: making Houdini inference transparent
- Cryptographic Verification by Typing for a Sample Protocol Implementation
- CacBDD
- c2i
- Houdini
- ExplainHoudini
- SPHIN
- OpenJML
- Featherweight VeriFast
- Coverity
- C-Light
- BoogiePL
- VACID-0
- Charge!
- SMACK
- Rocksalt
- Dynamic boundaries: information hiding by second order framing with first order assertions
- Shape analysis of low-level C with overlapping structures
- ANaConDA
- Klocwork
This page was built for software: VCC
