VeriFast
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Dafny
- Oclgrind
- JDD
- BDD
- ArcAngel
- KRAKATOA
- RAISE
- ACSL
- Instrumenting a weakest precondition calculus for counterexample generation
- Why3
- Spec#
- Caduceus
- Frama-C
- Alt-Ergo
- Backwards and forwards with separation logic
- Unifying separation logic and region logic to allow interoperability
- SPARKSkein
- Rodin
- ESC/Java
- VCC
- Pex
- Stepwise refinement of heap-manipulating code in Chalice
- Predator
- Chalice
- Crowfoot
- Boogie
- JACK
- Simpler proofs with decentralized invariants
- A relational shape abstract domain
- Verifying Whiley programs with Boogie
- Formal verification of parallel prefix sum and stream compaction algorithms in CUDA
- SMCHR
- Abstraction and subsumption in modular verification of C programs
- Toolchain
- Generalized arrays for Stainless frames
- Traits: correctness-by-construction for free
- WhyML
- SLAyer
- VeriCool
- HighSpec
- HIP
- Smallfoot
- VeriSmall
- TVLA
- KeY
- KIV
- FixBag
- Predicate extension of symbolic memory graphs for the analysis of memory safety correctness
- Deductive verification of floating-point Java programs in KeY
- RGITL: a temporal logic framework for compositional reasoning about interleaved programs
- Exploiting pointer analysis in memory models for deductive verification
- VerCors
- GPUVerify
- jStar
- Efficient verification of imperative programs using auto2
- Automating deductive verification for weak-memory programs
- A verification-driven framework for iterative design of controllers
- Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
- Ynot
- ModuRes
- FunArray
- Grasshopper
- FreeRTOS
- RGITL
- BVD
- Viper
- THOR
- Viper: a verification infrastructure for permission-based reasoning
- Sound, modular and compositional verification of the input/output behavior of programs
- Model checking for symbolic-heap separation logic with inductive predicates
- Invariants synthesis over a combined domain for automated program verification
- Symbolic execution proofs for higher order store programs
- Behavioral interface specification languages
- Crowfoot: A Verifier for Higher-Order Store Programs
- Automatic inference of access permissions
- Automating Induction with an SMT Solver
- Two for the price of one: lifting separation logic assertions
- Charge! A framework for higher-order separation logic in Coq
- A theorem prover for Boolean BI
- A program construction and verification tool for separation logic
- Caper
- Unified reasoning about robustness properties of symbolic-heap separation logic
- Cyclist
- coreStar
- Dafny: an automatic program verifier for functional correctness
- Interleaving symbolic execution and partial evaluation
- Static contract checking with abstract interpretation
- Specification patterns and proofs for recursion through the store
- Tractable Reasoning in a Fragment of Separation Logic
- A machine-checked framework for relational separation logic
- MSV
- CacBDD
- SPHIN
- OpenJML
- Featherweight VeriFast
- Model Checking MSVL Programs Based on Dynamic Symbolic Execution
- Caper
- Infer
- StaRVOOrS
- LARVA
This page was built for software: VeriFast
