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

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

doi:10.1007/978-3-540-69166-2_5

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

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

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Static Analysis - 15th International Symposium, SAS 2008, Proceedings
Pages	62-77
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-540-69166-2_5
State	Published - 2008
Event	15th International Static Analysis Symposium, SAS 2008 - Valencia, Spain Duration: Jul 16 2008 → Jul 18 2008

Publication series

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

Other

Other	15th International Static Analysis Symposium, SAS 2008
Country/Territory	Spain
City	Valencia
Period	7/16/08 → 7/18/08

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

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

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

Pointer analysis, conditional soundness, and proving the absence of errors. / Conway, Christopher L.; Dams, Dennis; Namjoshi, Kedar S. et al.
Static Analysis - 15th International Symposium, SAS 2008, Proceedings. 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 proceeding › Conference 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. 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. 2008. p. 62-77. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-540-69166-2_5

@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",

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",

note = "15th International Static Analysis Symposium, SAS 2008 ; Conference date: 16-07-2008 Through 18-07-2008",

}

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

AN - SCOPUS:48949104171

SN - 3540691634

SN - 9783540691631

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

T2 - 15th International Static Analysis Symposium, SAS 2008

Y2 - 16 July 2008 through 18 July 2008

ER -

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

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this