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

heap analysiscontainer analysissymbolic heap

Mathematics Subject Classification ID

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

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)

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

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)