A relational shape abstract domain

DOI10.1007/s10703-021-00366-4OpenAlexW3157261828MaRDI QIDQ2058389

Xavier Rival, Matthieu Lemerre, Hugo Illous

Publication date: 8 December 2021

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://hal-cea.archives-ouvertes.fr/cea-03218896/file/main.pdf

zbMATH Keywords

static analysisshape analysisabstract interpretationseparation logicrelational properties

Mathematics Subject Classification ID

Computer science (68-XX)

Related Items (2)

Relational string abstract domains ⋮ Lifting numeric relational domains to algebraic data types

Uses Software

• ACSL
• JML
• Frama-C
• VeriFast
• HIP
• Charge!

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Resources, concurrency, and local reasoning
• A relational framework for higher-order shape analysis
• Charge!
• Temporary Read-Only Permissions for Separation Logic
• Relational inductive shape analysis
• Bottom-Up Shape Analysis
• Reasoning about Optimistic Concurrency Using a Program Logic for History
• Safety and Liveness in Concurrent Pointer Programs
• Grammar Analysis and Parsing by Abstract Interpretation
• Systematic design of program transformation frameworks by abstract interpretation
• Compositional shape analysis by means of bi-abduction
• Semantic-directed clumping of disjunctive abstract states
• Comparison Under Abstraction for Verifying Linearizability
• Automated Verification of Shape and Size Properties Via Separation Logic
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Static Analysis
• Tools and Algorithms for the Construction and Analysis of Systems

This page was built for publication: A relational shape abstract domain