Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors

Autor:	Clark Barrett, Kedar S. Namjoshi, Christopher L. Conway, Dennis Dams
Rok vydání:	2008
Předmět:	Statement (computer science) Soundness Theoretical computer science Property (programming) Computer science Static program analysis Abstract interpretation Memory safety Algorithm Pointer analysis
Zdroj:	Static Analysis ISBN: 9783540691631 SAS
DOI:	10.1007/978-3-540-69166-2_5
Popis:	It is well known that the use of points-to information can substantially improve the accuracy of a static program analysis. Commonly used algorithms for computing points-to information are known to be sound only for memory-safe programs. Thus, it appears problematic to utilize points-to information to verify the memory safety property without giving up soundness. We show that a sound combination is possible, even if the points-to information is computed separately and only conditionally sound. This result is based on a refined statement of the soundness conditions of points-to analyses and a general mechanism for composing conditionally sound analyses.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::50f4d99f070b1b3d91e1759c44e9d5ff https://doi.org/10.1007/978-3-540-69166-2_5 Zobrazit plný text záznamu