Program analysis is harder than verification: A computability perspective

Patrick Cousot; Roberto Giacobazzi; Francesco Ranzato

doi:10.1007/978-3-319-96142-2_8

Program analysis is harder than verification: A computability perspective

Patrick Cousot, Roberto Giacobazzi, Francesco Ranzato

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

We study from a computability perspective static program analysis, namely detecting sound program assertions, and verification, namely sound checking of program assertions. We first design a general computability model for domains of program assertions and corresponding program analysers and verifiers. Next, we formalize and prove an instantiation of Rice’s theorem for static program analysis and verification. Then, within this general model, we provide and show a precise statement of the popular belief that program analysis is a harder problem than program verification: we prove that for finite domains of program assertions, program analysis and verification are equivalent problems, while for infinite domains, program analysis is strictly harder than verification.

Original language	English (US)
Title of host publication	Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings
Editors	Georg Weissenbacher, Hana Chockler
Publisher	Springer Verlag
Pages	75-95
Number of pages	21
ISBN (Print)	9783319961415
DOIs	https://doi.org/10.1007/978-3-319-96142-2_8
State	Published - 2018
Event	30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018 - Oxford, United Kingdom Duration: Jul 14 2018 → Jul 17 2018

Publication series

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

Other

Other	30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018
Country	United Kingdom
City	Oxford
Period	7/14/18 → 7/17/18

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-319-96142-2_8

Fingerprint Dive into the research topics of 'Program analysis is harder than verification: A computability perspective'. Together they form a unique fingerprint.

Cite this

Cousot, P., Giacobazzi, R., & Ranzato, F. (2018). Program analysis is harder than verification: A computability perspective. In G. Weissenbacher, & H. Chockler (Eds.), Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings (pp. 75-95). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10982 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-96142-2_8

Program analysis is harder than verification : A computability perspective. / Cousot, Patrick; Giacobazzi, Roberto; Ranzato, Francesco.

Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. ed. / Georg Weissenbacher; Hana Chockler. Springer Verlag, 2018. p. 75-95 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10982 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Cousot, P, Giacobazzi, R & Ranzato, F 2018, Program analysis is harder than verification: A computability perspective. in G Weissenbacher & H Chockler (eds), Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10982 LNCS, Springer Verlag, pp. 75-95, 30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018, Oxford, United Kingdom, 7/14/18. https://doi.org/10.1007/978-3-319-96142-2_8

Cousot P, Giacobazzi R, Ranzato F. Program analysis is harder than verification: A computability perspective. In Weissenbacher G, Chockler H, editors, Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Springer Verlag. 2018. p. 75-95. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-96142-2_8

Cousot, Patrick ; Giacobazzi, Roberto ; Ranzato, Francesco. / Program analysis is harder than verification : A computability perspective. Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. editor / Georg Weissenbacher ; Hana Chockler. Springer Verlag, 2018. pp. 75-95 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{dc3137c297fe466c99339f1c6e45373f,

title = "Program analysis is harder than verification: A computability perspective",

abstract = "We study from a computability perspective static program analysis, namely detecting sound program assertions, and verification, namely sound checking of program assertions. We first design a general computability model for domains of program assertions and corresponding program analysers and verifiers. Next, we formalize and prove an instantiation of Rice{\textquoteright}s theorem for static program analysis and verification. Then, within this general model, we provide and show a precise statement of the popular belief that program analysis is a harder problem than program verification: we prove that for finite domains of program assertions, program analysis and verification are equivalent problems, while for infinite domains, program analysis is strictly harder than verification.",

author = "Patrick Cousot and Roberto Giacobazzi and Francesco Ranzato",

note = "Publisher Copyright: {\textcopyright} The Author(s) 2018. Copyright: Copyright 2018 Elsevier B.V., All rights reserved.; 30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018 ; Conference date: 14-07-2018 Through 17-07-2018",

year = "2018",

doi = "10.1007/978-3-319-96142-2_8",

language = "English (US)",

isbn = "9783319961415",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "75--95",

editor = "Georg Weissenbacher and Hana Chockler",

booktitle = "Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings",

}

TY - GEN

T1 - Program analysis is harder than verification

T2 - 30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018

AU - Cousot, Patrick

AU - Giacobazzi, Roberto

AU - Ranzato, Francesco

PY - 2018

Y1 - 2018

N2 - We study from a computability perspective static program analysis, namely detecting sound program assertions, and verification, namely sound checking of program assertions. We first design a general computability model for domains of program assertions and corresponding program analysers and verifiers. Next, we formalize and prove an instantiation of Rice’s theorem for static program analysis and verification. Then, within this general model, we provide and show a precise statement of the popular belief that program analysis is a harder problem than program verification: we prove that for finite domains of program assertions, program analysis and verification are equivalent problems, while for infinite domains, program analysis is strictly harder than verification.

AB - We study from a computability perspective static program analysis, namely detecting sound program assertions, and verification, namely sound checking of program assertions. We first design a general computability model for domains of program assertions and corresponding program analysers and verifiers. Next, we formalize and prove an instantiation of Rice’s theorem for static program analysis and verification. Then, within this general model, we provide and show a precise statement of the popular belief that program analysis is a harder problem than program verification: we prove that for finite domains of program assertions, program analysis and verification are equivalent problems, while for infinite domains, program analysis is strictly harder than verification.

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

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

U2 - 10.1007/978-3-319-96142-2_8

DO - 10.1007/978-3-319-96142-2_8

M3 - Conference contribution

AN - SCOPUS:85051135661

SN - 9783319961415

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

SP - 75

EP - 95

BT - Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings

A2 - Weissenbacher, Georg

A2 - Chockler, Hana

PB - Springer Verlag

Y2 - 14 July 2018 through 17 July 2018

ER -