Inference of Field-Sensitive Reachability and Cyclicity

DOI10.1145/2629478zbMath1354.68035arXiv1306.6526OpenAlexW1987635382MaRDI QIDQ2946745

Samir Genaim, Damiano Zanardini

Publication date: 17 September 2015

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1306.6526

zbMATH Keywords

data structuresstatic analysispointer analysisshape analysisabstract interpretationheap manipulationtermination analysiscyclicity analysis

Mathematics Subject Classification ID

Theory of programming languages (68N15) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Data structures (68P05)

Related Items (1)

Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic

Uses Software

• GC

Cites Work

• Unnamed Item
• Unnamed Item
• Cost analysis of object-oriented bytecode programs
• Reachability-based acyclicity analysis by abstract interpretation
• On the Inference of Resource Usage Upper and Lower Bounds
• Cyclic proofs of program termination in separation logic
• Mechanical program analysis
• The s-semantics approach: Theory and applications
• Interprocedural Shape Analysis for Effectively Cutpoint-Free Programs
• Systematic design of program transformation frameworks by abstract interpretation
• A semantics for procedure local heaps and its abstractions
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Automatic Termination Proofs for Programs with Shape-Shifting Heaps
• Static Analysis
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Inference of Field-Sensitive Reachability and Cyclicity