Shape analysis by predicate abstraction

DOI10.1007/978-3-540-30579-8_12MaRDI QIDQ5711489zbMATH OpenOpenAlexFDO

Authors Ittai Balaban, Amir Pnueli, Lenore D. Zuck

Publication date 6 December 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b105073

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• Shape analysis through predicate abstraction and model checking
• Tools and Algorithms for the Construction and Analysis of Systems
• Automated Technology for Verification and Analysis
• Formal Techniques for Networked and Distributed Systems - FORTE 2005
• Static Analysis

Cited in

(31)

• Fragment abstraction for concurrent shape analysis
• A logic of reachable patterns in linked data-structures
• Predicate abstraction for linked data structures
• Inference of field-sensitive reachability and cyclicity
• Monotonic abstraction for programs with multiply-linked structures
• Relational inductive shape analysis
• Mind the Shapes: Abstraction Refinement Via Topology Invariants
• Verifying Heap-Manipulating Programs in an SMT Framework
• Abstracting Complex Data Structures by Hyperedge Replacement
• Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic
• Specialized 3-Valued Logic Shape Analysis Using Structure-Based Refinement and Loose Embedding
• MLAT: a tool for heap analysis based on predicate abstraction by modal logic
• Algorithmic Analysis of Array-Accessing Programs
• Shape Analysis in the Absence of Pointers and Structure
• Verification of multi-linked heaps
• Shape analysis through predicate abstraction and model checking
• Understanding as an interpretation in a shape understanding system
• Logical characterizations of heap abstractions
• Tools and Algorithms for the Construction and Analysis of Systems
• Programs with lists are counter automata
• Towards Abstraction-Based Verification of Shape Calculus
• Shape Analysis of Single-Parent Heaps
• An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures
• Partially disjunctive heap abstraction
• Formal Techniques for Networked and Distributed Systems - FORTE 2005
• Automated Technology for Verification and Analysis
• Predicate abstraction and canonical abstraction for singly-linked lists
• A Reachability Predicate for Analyzing Low-Level Software
• Static Analysis
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Shape analysis by predicate abstraction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5711489)