Download PDFOpen PDF in browser

Program Analysis is Harder than Verification: A Computability Perspective

EasyChair Preprint 365

18 pagesDate: July 20, 2018

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

Keyphrases: Rice's theorem, abstract interpretation, computability, program verification, static program analysis

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@booklet{EasyChair:365,
  author    = {Patrick Cousot and Roberto Giacobazzi and Francesco Ranzato},
  title     = {Program Analysis is Harder than Verification: A Computability Perspective},
  doi       = {10.29007/6psr},
  howpublished = {EasyChair Preprint 365},
  year      = {EasyChair, 2018}}
Download PDFOpen PDF in browser