Cited in
(42)- Specification patterns for reasoning about recursion through the store
- Automated theorem proving for assertions in separation logic with all connectives
- A theorem prover for Boolean BI
- Automatic verification of Java programs with dynamic frames
- Two for the price of one: lifting separation logic assertions
- Symbolic execution proofs for higher order store programs
- Verified heap theorem prover by paramodulation
- A Shape Analysis for Non-linear Data Structures
- Matching logic: an alternative to Hoare/Floyd logic
- Matching logic
- A proof system for separation logic with magic wand
- Undecidability of propositional separation logic and its neighbours
- JACK
- Crowfoot
- VeriFast
- SLAyer
- VeriStar
- Smallfoot
- VeriSmall
- Ynot
- THOR
- A shape graph logic and a shape system
- Java Jr
- Charge!
- Gallina
- Generalized arrays for Stainless frames
- Static contract checking with abstract interpretation
- Specification patterns and proofs for recursion through the store
- Temporary read-only permissions for separation logic
- Automated cyclic entailment proofs in separation logic
- A program construction and verification tool for separation logic
- Local reasoning for global invariants. II: Dynamic boundaries
- Certificates and Separation Logic
- Separation Logic Tutorial
- Automatic Parallelization and Optimization of Programs by Proof Rewriting
- Tractable Reasoning in a Fragment of Separation Logic
- A unified display proof theory for bunched logic
- Classical BI: Its Semantics and Proof Theory
- Bunched logics displayed
- Featherweight VeriFast
- Verification of concurrent systems with VerCors
- Compositional shape analysis by means of bi-abduction
This page was built for software: jStar
