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