Program analysis is harder than verification: A computability perspective

Patrick Cousot, Roberto Giacobazzi, Francesco Ranzato

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish (US)
Title of host publicationComputer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings
EditorsGeorg Weissenbacher, Hana Chockler
PublisherSpringer Verlag
Pages75-95
Number of pages21
ISBN (Print)9783319961415
DOIs
StatePublished - Jan 1 2018
Event30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018 - Oxford, United Kingdom
Duration: Jul 14 2018Jul 17 2018

Publication series

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

Other

Other30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018
CountryUnited Kingdom
CityOxford
Period7/14/187/17/18

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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