jStar
From MaRDI portal
Software:23207
swMATH11261MaRDI QIDQ23207FDOQ23207
Author name not available (Why is that?)
Cited In (30)
- Specification patterns for reasoning about recursion through the store
- A theorem prover for Boolean BI
- A Unified Display Proof Theory for Bunched Logic
- Automatic verification of Java programs with dynamic frames
- Two for the price of one: lifting separation logic assertions
- Verified heap theorem prover by paramodulation
- Symbolic execution proofs for higher order store programs
- A Shape Analysis for Non-linear Data Structures
- A proof system for separation logic with magic wand
- Matching logic: an alternative to Hoare/Floyd logic
- Local Reasoning for Global Invariants, Part II
- Automated Theorem Proving for Assertions in Separation Logic with All Connectives
- Generalized arrays for Stainless frames
- A shape graph logic and a shape system
- Static contract checking with abstract interpretation
- Verification of Concurrent Systems with VerCors
- Specification patterns and proofs for recursion through the store
- Automated cyclic entailment proofs in separation logic
- Certificates and Separation Logic
- Separation Logic Tutorial
- Automatic Parallelization and Optimization of Programs by Proof Rewriting
- Tractable Reasoning in a Fragment of Separation Logic
- Undecidability of Propositional Separation Logic and Its Neighbours
- Classical BI: Its Semantics and Proof Theory
- Matching Logic
- Bunched logics displayed
- Featherweight VeriFast
- Temporary Read-Only Permissions for Separation Logic
- A Program Construction and Verification Tool for Separation Logic
- Compositional Shape Analysis by Means of Bi-Abduction
This page was built for software: jStar
