swMATH7220MaRDI QIDQ19271FDOQ19271
Author name not available (Why is that?)
Official website: http://vcc.codeplex.com/
Cited In (only showing first 100 items - show all)
- Extending Sledgehammer with SMT solvers
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- Automating Induction with an SMT Solver
- Bridging the Gap: Automatic Verified Abstraction of C
- FeatherTrait
- A framework for the verification of certifying computations
- System-level non-interference of constant-time cryptography. I: Model
- Concerned with the unprivileged: user programs in kernel refinement
- Modular inference of subprogram contracts for safety checking
- Behavioral interface specification languages
- Error-tracing axiomatic semantics for C-kernel
- HOL-Boogie
- 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
- Bugs, moles and skeletons: symbolic reasoning for software development
- 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
- AutoProof
- RVT
- C-to-Isabelle
- ShortestPath
- Cascade
- Crust
- Rust2Viper
- Corral
- Nagini
- From rewriting logic, to programming language semantics, to program verification
- Doomed program points
- Certifying algorithms
- Extending Sledgehammer with SMT solvers
- Leveraging compiler intermediate representation for multi- and cross-language verification
- Abstraction and subsumption in modular verification of C programs
- 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
- 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
- TraitCbC
- Verifying Whiley programs with Boogie
- SableJBDD
This page was built for software: VCC
