Shape analysis through predicate abstraction and model checking

DOI10.1007/3-540-36384-X_25MaRDI QIDQ4414398zbMATH OpenFDO

Authors Dennis Dams, Kedar S. Namjoshi

Publication date 25 July 2003

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

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2575/25750310.htm

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verification, Model Checking, and Abstract Interpretation
• Tools and Algorithms for the Construction and Analysis of Systems
• Compositional shape analysis by means of bi-abduction
• Model checking: from hardware to software.
• Shape Analysis for Composite Data Structures

Cited in

(21)

• Fragment abstraction for concurrent shape analysis
• Concrete memory models for shape analysis
• Shape analysis of sets
• Mind the Shapes: Abstraction Refinement Via Topology Invariants
• Thread Quantification for Concurrent Shape Analysis
• Abstracting Complex Data Structures by Hyperedge Replacement
• 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
• Learning shape analysis
• Compositional shape analysis by means of bi-abduction
• Tools and Algorithms for the Construction and Analysis of Systems
• Programming Languages and Systems
• Compositional shape analysis by means of bi-abduction
• Towards Abstraction-Based Verification of Shape Calculus
• Shape Analysis for Composite Data Structures
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Relational and Kleene-Algebraic Methods in Computer Science
• Static Analysis
• Verification, Model Checking, and Abstract Interpretation
• Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness

Describes a project that uses

Uses Software

• SLAM
• TVLA
• SPIN

This page was built for publication: Shape analysis through predicate abstraction and model checking

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