Precise reasoning for programs using containers

DOI10.1145/1926385.1926407MaRDI QIDQ5408543zbMATH OpenOpenAlexFDO

Authors Isil Dillig, Thomas Dillig, Alex Aiken

Publication date 10 April 2014

Published in Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1926385.1926407

zbMATH Keywords

container analysisheap analysissymbolic heap

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Data structures (68P05)

Recommendations

• Correct code containing containers
• Abstract domains and solvers for sets reasoning
• Reasoning about heap manipulating programs using automata techniques
• From low-level pointers to high-level containers
• Logical Interpretation: Static Program Analysis Using Theorem Proving

Cited in

(7)

• From low-level pointers to high-level containers
• Optimization modulo theories with linear rational costs
• Correct code containing containers
• Generic abstraction of dictionaries and arrays
• Proving Properties about Lists Using Containers
• An array content static analysis based on non-contiguous partitions
• Under-approximating loops in C programs for fast counterexample detection

This page was built for publication: Precise reasoning for programs using containers

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