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
- QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers
- Verified heap theorem prover by paramodulation
- Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic
- Foundations for Decision Problems in Separation Logic with General Inductive Predicates
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
- From Low-Level Pointers to High-Level Containers
- Taking Satisfiability to the Next Level with Z3
- Disproving Inductive Entailments in Separation Logic via Base Pair Approximation
- Predicate extension of symbolic memory graphs for the analysis of memory safety correctness
- Deciding Bit-Vector Formulas with mcSAT
- 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
- Automated mutual induction proof in separation logic
- Shape Neutral Analysis of Graph-based Data-structures
- Predicate Abstraction in Program Verification: Survey and Current Trends
- An adaptation-complete proof system for local reasoning about cloud storage systems
- Matching Logic
- Featherweight VeriFast
- Resourceful Reachability as HORN-LA
- Reasoning about block-based cloud storage systems via separation logic
This page was built for software: SLAyer
