SLAyer
From MaRDI portal
Software:21691
swMATH9712MaRDI QIDQ21691FDOQ21691
Author name not available (Why is that?)
Cited In (21)
- Model checking for symbolic-heap separation logic with inductive predicates
- Disproving inductive entailments in separation logic via base pair approximation
- From low-level pointers to high-level containers
- Taking satisfiability to the next level with Z3 (abstract)
- QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers
- Shape neutral analysis of graph-based data-structures
- Verified heap theorem prover by paramodulation
- Matching logic
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
- Predicate extension of symbolic memory graphs for the analysis of memory safety correctness
- Deciding Bit-Vector Formulas with mcSAT
- Foundations for decision problems in separation logic with general inductive predicates
- An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning
- Automatically proving termination and memory safety for programs with pointer arithmetic
- Resourceful reachability as HORN-LA
- Automated mutual induction proof in separation logic
- Predicate Abstraction in Program Verification: Survey and Current Trends
- An adaptation-complete proof system for local reasoning about cloud storage systems
- Featherweight VeriFast
- Reasoning about block-based cloud storage systems via separation logic
- Unified reasoning about robustness properties of symbolic-heap separation logic
This page was built for software: SLAyer
