VeriFast
From MaRDI portal
swMATH7705MaRDI QIDQ19722FDOQ19722
Author name not available (Why is that?)
Official website: http://people.cs.kuleuven.be/~bart.jacobs/verifast/
Cited In (only showing first 100 items - show all)
- Verifying array manipulating programs with full-program induction
- Specification patterns for reasoning about recursion through the store
- RGITL: a temporal logic framework for compositional reasoning about interleaved programs
- Efficient verification of imperative programs using auto2
- Automating Induction with an SMT Solver
- BDD
- JDD
- Automatic verification of Java programs with dynamic frames
- FeatherTrait
- Symbolic execution proofs for higher order store programs
- A Basis for Verifying Multi-threaded Programs
- Viper: a verification infrastructure for permission-based reasoning
- Concise read-only specifications for better synthesis of programs with pointers
- Local reasoning for global graph properties
- Automated verification of parallel nested DFS
- Simpler proofs with decentralized invariants
- Automating deductive verification for weak-memory programs
- Behavioral interface specification languages
- Static contract checking with abstract interpretation
- ACSL
- Caduceus
- Frama-C
- Why3
- Alt-Ergo
- Spec#
- SPARKSkein
- Rodin
- ESC/Java
- Pex
- Predator
- VCC
- JACK
- Boogie
- Chalice
- Crowfoot
- SMCHR
- HighSpec
- HIP
- SLAyer
- Smallfoot
- KeY
- Toolchain
- FixBag
- KIV
- WhyML
- VeriCool
- VeriSmall
- TVLA
- Viper
- GPUVerify
- jStar
- VerCors
- Ynot
- ModuRes
- FunArray
- FreeRTOS
- Grasshopper
- BVD
- RGITL
- THOR
- Specification patterns and proofs for recursion through the store
- coreStar
- Cyclist
- CacBDD
- MSV
- OpenJML
- Caper
- SPHIN
- Infer
- LARVA
- MarQ
- StaRVOOrS
- VACID-0
- Charge!
- Jessie
- GRASShopper
- AstraVer
- Slide
- GRace
- VST-Floyd
- AutoProof
- Auto2_Imperative_HOL
- SCiFI
- CIVL
- KeYmaera X
- A program construction and verification tool for separation logic
- A generic framework for symbolic execution: a coinductive approach
- Practical abstractions for automated verification of shared-memory concurrency
- One logic to use them all
- Tractable Reasoning in a Fragment of Separation Logic
- Abstraction and subsumption in modular verification of C programs
- Crowfoot: A Verifier for Higher-Order Store Programs
- Dafny: an automatic program verifier for functional correctness
- Verification of concurrent systems with VerCors
- Caper
- Expressive modular fine-grained concurrency specification
- TraitCbC
- A theorem prover for Boolean BI
- Verifying Whiley programs with Boogie
- IronFleet
This page was built for software: VeriFast
