Smallfoot
From MaRDI portal
Cited in
(93)- Oclgrind
- Proof tactics for assertions in separation logic
- Compositional entailment checking for a fragment of separation logic
- Unifying separation logic and region logic to allow interoperability
- Predator
- VeriFast
- Crowfoot
- Formal verification of parallel prefix sum and stream compaction algorithms in CUDA
- SMCHR
- VeriStar
- LLBMC
- Toolchain
- SLAyer
- cminor
- HIP
- VeriSmall
- TVLA
- VerCors
- GPUVerify
- jStar
- Separation logic with one quantified variable
- Ynot
- GKLEE
- ModuRes
- Juggrnaut
- Grasshopper
- Viper
- THOR
- Completeness for recursive procedures in separation logic
- Viper: a verification infrastructure for permission-based reasoning
- Local reasoning about data update
- Symbolic execution proofs for higher order store programs
- Crowfoot: A Verifier for Higher-Order Store Programs
- Effective interactive proofs for higher-order imperative programs
- Temporary read-only permissions for separation logic
- Caper
- Unified reasoning about robustness properties of symbolic-heap separation logic
- Reasoning about assignments in recursive data structures
- coreStar
- Specification patterns and proofs for recursion through the store
- Tractable Reasoning in a Fragment of Separation Logic
- Completeness for a first-order abstract separation logic
- Practical Tactics for Separation Logic
- A Formalisation of Smallfoot in HOL
- Featherweight VeriFast
- Caper
- Infer
- Automatic Parallelization and Optimization of Programs by Proof Rewriting
- Tableaux and resource graphs for separation logic
- CSimpl
- Charge!
- Automated theorem proving for assertions in separation logic with all connectives
- GRASShopper
- Lightweight Separation
- REFINER
- Automatic Parallelization with Separation Logic
- A Basis for Verifying Multi-threaded Programs
- Beyond Shapes: Lists with Ordered Data
- Verifying Reference Counting Implementations
- QAGen
- C32SAT
- Z34Bio
- Gallina
- Specification patterns for reasoning about recursion through the store
- Slide
- GRace
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Shape neutral analysis of graph-based data-structures
- Separation logics and modalities: a survey
- Matching logic
- A first-order logic with frames
- On temporal and separation logics
- Verified heap theorem prover by paramodulation
- Verification of concurrent systems with VerCors
- Decision procedures. An algorithmic point of view
- Disjoint-union partial algebras
- Compositional shape analysis by means of bi-abduction
- A proof system for separation logic with magic wand
- Automated Verification of Shape and Size Properties Via Separation Logic
- Static Analysis
- Separation Logic Tutorial
- WebAssembly
- Loopy
- Proof automation for functional correctness in separation logic
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
- SeLoger
- MoSeL
- Reasoning about memory layouts
- Reasoning about sequences of memory states
- A shape graph logic and a shape system
- Juggrnaut: using graph grammars for abstracting unbounded heap structures
- Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms
- Certifying low-level programs with hardware interrupts and preemptive threads
This page was built for software: Smallfoot
