Program Analysis is Harder than Verification: A Computability Perspective

EasyChair Preprint 365

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

@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}}