Pointer analysis, conditional soundness, and proving the absence of errors

Christopher L. Conway, Dennis Dams, Kedar S. Namjoshi, Clark Barrett

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationStatic Analysis - 15th International Symposium, SAS 2008, Proceedings
Pages62-77
Number of pages16
DOIs
StatePublished - Aug 13 2008
Event15th International Static Analysis Symposium, SAS 2008 - Valencia, Spain
Duration: Jul 16 2008Jul 18 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5079 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other15th International Static Analysis Symposium, SAS 2008
CountrySpain
CityValencia
Period7/16/087/18/08

    Fingerprint

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Conway, C. L., Dams, D., Namjoshi, K. S., & Barrett, C. (2008). Pointer analysis, conditional soundness, and proving the absence of errors. In Static Analysis - 15th International Symposium, SAS 2008, Proceedings (pp. 62-77). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5079 LNCS). https://doi.org/10.1007/978-3-540-69166-2_5