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