Foundations of Software Science and Computation Structures
DOI10.1007/11690634zbMATH Open1180.68131OpenAlexW2504714231MaRDI QIDQ5899082FDOQ5899082
Authors: Greta Yorsh, Alexander Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani
Publication date: 2 May 2007
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11690634
Recommendations
- A logic of reachable patterns in linked data-structures
- Datalog revisited for reasoning in linked data
- Predicate abstraction for linked data structures
- Simulating reachability using first-order logic with applications to verification of linked data structures
- Automated Deduction – CADE-20
- scientific article; zbMATH DE number 1499081
- Path logics for querying graphs: combining expressiveness and efficiency
Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)
Cited In (20)
- Verifying Heap-Manipulating Programs in an SMT Framework
- Title not available (Why is that?)
- Separation logics and modalities: a survey
- On the almighty wand
- Quantitative separation logic and programs with lists
- Title not available (Why is that?)
- Implication and Axiomatization of Functional Constraints on Patterns with an Application to the RDF Data Model
- Verification of multi-linked heaps
- Simulating reachability using first-order logic with applications to verification of linked data structures
- Program verification with interacting analysis plugins
- Static Analysis
- An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures
- PDL for structured data: a graph-calculus approach
- Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems
- On the Almighty Wand
- Modeling and verifying graph transformations in proof assistants
- Beyond Shapes: Lists with Ordered Data
- A logic of reachable patterns in linked data-structures
- Automated Deduction – CADE-20
- A Logic-Based Framework for Reasoning about Composite Data Structures
This page was built for publication: Foundations of Software Science and Computation Structures
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5899082)