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