VeriFast
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Specification patterns for reasoning about recursion through the store
- Expressive modular fine-grained concurrency specification
- Unified reasoning about robustness properties of symbolic-heap separation logic
- Verifying array manipulating programs with full-program induction
- RGITL: a temporal logic framework for compositional reasoning about interleaved programs
- SeLoger
- Verifying Whiley programs with Boogie
- A theorem prover for Boolean BI
- Formal verification of a Java component using the RESOLVE framework
- Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
- Ghost signals: verifying termination of busy waiting
- Efficient verification of imperative programs using auto2
- Model checking for symbolic-heap separation logic with inductive predicates
- Considerate reasoning and the Composite design pattern
- Disproving inductive entailments in separation logic via base pair approximation
- Automating Induction with an SMT Solver
- Automatic verification of Java programs with dynamic frames
- Sound, modular and compositional verification of the input/output behavior of programs
- Formal verification of parallel prefix sum and stream compaction algorithms in CUDA
- Deductive verification of floating-point Java programs in KeY
- Automating theorem proving with SMT
- Two for the price of one: lifting separation logic assertions
- Shape neutral analysis of graph-based data-structures
- Symbolic execution proofs for higher order store programs
- A Basis for Verifying Multi-threaded Programs
- Viper: a verification infrastructure for permission-based reasoning
- A Shape Analysis for Non-linear Data Structures
- Concise read-only specifications for better synthesis of programs with pointers
- Local reasoning for global graph properties
- Simpler proofs with decentralized invariants
- Automated verification of parallel nested DFS
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
- Automating deductive verification for weak-memory programs
- On Symbolic Heaps Modulo Permission Theories
- MoSeL
- Instrumenting a weakest precondition calculus for counterexample generation
- Behavioral interface specification languages
- Dafny
- ArcAngel
- KRAKATOA
- RAISE
- 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
- coreStar
- Cyclist
- CacBDD
- MSV
- OpenJML
- Caper
- SPHIN
- Infer
- LARVA
- MarQ
- StaRVOOrS
- VACID-0
- Charge!
- Jessie
- GRASShopper
- AstraVer
- Slide
- GRace
This page was built for software: VeriFast
