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
- Automated Cyclic Entailment Proofs in Separation 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
- Verification of Concurrent Systems with VerCors
- Matching Logic: An Alternative to Hoare/Floyd 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
- Static Contract Checking with Abstract Interpretation
- Featherweight VeriFast
- Specification Patterns and Proofs for Recursion through the Store
- 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
