swMATH9712MaRDI QIDQ21691FDOQ21691
Author name not available (Why is that?)
Official website: http://link.springer.com/chapter/10.1007/978-3-642-22110-1_15
Cited In (44)
- 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
- Predator
- VeriFast
- SMCHR
- LLBMC
- HIP
- VeriStar
- Smallfoot
- FixBag
- Quicr
- VeriSmall
- jStar
- ModuRes
- Ctrl
- THOR
- Foundations for decision problems in separation logic with general inductive predicates
- coreStar
- Cyclist
- Sparrow
- Infer
- MemPick
- GRASShopper
- Gallina
- Slide
- 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
- Juliet Test Suite
- 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
