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
Volume5079 LNCS
DOIs
StatePublished - 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)03029743
ISSN (Electronic)16113349

Other

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

Fingerprint

Soundness
Acoustic waves
Data storage equipment
Program Analysis
Static Analysis
Safety
Verify
Sound
Computing

ASJC Scopus subject areas

  • Computer Science(all)
  • Biochemistry, Genetics and Molecular Biology(all)
  • Theoretical Computer Science

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 (Vol. 5079 LNCS, 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

Pointer analysis, conditional soundness, and proving the absence of errors. / Conway, Christopher L.; Dams, Dennis; Namjoshi, Kedar S.; Barrett, Clark.

Static Analysis - 15th International Symposium, SAS 2008, Proceedings. Vol. 5079 LNCS 2008. p. 62-77 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5079 LNCS).

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

Conway, CL, Dams, D, Namjoshi, KS & Barrett, C 2008, Pointer analysis, conditional soundness, and proving the absence of errors. in Static Analysis - 15th International Symposium, SAS 2008, Proceedings. vol. 5079 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5079 LNCS, pp. 62-77, 15th International Static Analysis Symposium, SAS 2008, Valencia, Spain, 7/16/08. https://doi.org/10.1007/978-3-540-69166-2_5
Conway CL, Dams D, Namjoshi KS, Barrett C. Pointer analysis, conditional soundness, and proving the absence of errors. In Static Analysis - 15th International Symposium, SAS 2008, Proceedings. Vol. 5079 LNCS. 2008. p. 62-77. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-540-69166-2_5
Conway, Christopher L. ; Dams, Dennis ; Namjoshi, Kedar S. ; Barrett, Clark. / Pointer analysis, conditional soundness, and proving the absence of errors. Static Analysis - 15th International Symposium, SAS 2008, Proceedings. Vol. 5079 LNCS 2008. pp. 62-77 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{a71a3a3c1875465299a1c5a059854b96,
title = "Pointer analysis, conditional soundness, and proving the absence of errors",
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.",
author = "Conway, {Christopher L.} and Dennis Dams and Namjoshi, {Kedar S.} and Clark Barrett",
year = "2008",
doi = "10.1007/978-3-540-69166-2_5",
language = "English (US)",
isbn = "3540691634",
volume = "5079 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "62--77",
booktitle = "Static Analysis - 15th International Symposium, SAS 2008, Proceedings",

}

TY - GEN

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

AU - Conway, Christopher L.

AU - Dams, Dennis

AU - Namjoshi, Kedar S.

AU - Barrett, Clark

PY - 2008

Y1 - 2008

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=48949104171&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=48949104171&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-69166-2_5

DO - 10.1007/978-3-540-69166-2_5

M3 - Conference contribution

SN - 3540691634

SN - 9783540691631

VL - 5079 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 62

EP - 77

BT - Static Analysis - 15th International Symposium, SAS 2008, Proceedings

ER -