Foundations of Software Science and Computation Structures

DOI10.1007/11690634MaRDI QIDQ5899082zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Data structures (68P05)

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

Cited in

(21)

• Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems
• Program verification with interacting analysis plugins
• A logic of reachable patterns in linked data-structures
• Modeling and verifying graph transformations in proof assistants
• A Logic-Based Framework for Reasoning about Composite Data Structures
• Verifying Heap-Manipulating Programs in an SMT Framework
• On the Almighty Wand
• Beyond Shapes: Lists with Ordered Data
• Simulating reachability using first-order logic with applications to verification of linked data structures
• On the almighty wand
• Verification of multi-linked heaps
• Separation logics and modalities: a survey
• PDL for structured data: a graph-calculus approach
• scientific article; zbMATH DE number 1841828 (Why is no real title available?)
• scientific article; zbMATH DE number 2090860 (Why is no real title available?)
• Automated Deduction – CADE-20
• Implication and Axiomatization of Functional Constraints on Patterns with an Application to the RDF Data Model
• Decidable logics combining heap structures and data
• An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures
• Static Analysis
• Quantitative separation logic and programs with lists

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)