P. Cousot, R. Giacobazzi, & F. Ranzato, Program Analysis Is Harder Than Verification: A Computability Perspective

Patrick Cousot, Roberto Giacobazzi, and Francesco Ranzato.
Program Analysis Is Harder Than Verification: A Computability Perspective.
In Conference on Computer-Aided Verification, 30th International Conference, CAV '2018, H. Chockler and G. Weissenbacher (Eds.), Oxford, UK. Lecture Notes in Computer Science 10982, pages 75-95. © Springer-Verlag, Berlin, Germany, July 14--17, 2018.
Paper: .pdf (262 KB)
Abstract: We study from a computability perspective static program analysis, namely detecting sound program assertions, and verification, namely sound check- ing of program assertions. We first design a general computability model for do- mains of program assertions and corresponding program analysers and verifiers. Next, we formalize and prove an instantiation of Rice’s theorem for static pro- gram 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.

\bibitem{DBLP:conf/cav/CousotGR18}
Patrick Cousot, Roberto Giacobazzi, and Francesco Ranzato.
\newblock Program Analysis is Harder than Verification: A Computability Perspective.
\newblock In \emph{30th Conference on Computer-Aided Verification, 
  CAV 2018}, H.~Chockler and G.~Weissenbacher (Eds.). Oxford, UK, Lecture Notes
  in Computer Science 10982, pages 75--95. Springer-Verlag, 
  Berlin, Germany, July 14--17, 2018.

@inproceedings{DBLP:conf/cav/CousotGR18,
  author    = {Patrick Cousot and
               Roberto Giacobazzi and
               Francesco Ranzato},
  editor    = {Hana Chockler and
               Georg Weissenbacher},
  title     = {Program Analysis Is Harder Than Verification: {A} Computability Perspective},
  booktitle = {Computer Aided Verification --- 30th International Conference, {CAV}
               2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
               UK, July 14--17, 2018, Proceedings, Part {II}},
  series    = {Lecture Notes in Computer Science},
  volume    = {10982},
  pages     = {75--95},
  publisher = {Springer},
  year      = {2018},
  url       = {https://doi.org/10.1007/978-3-319-96142-2\_8},
  doi       = {10.1007/978-3-319-96142-2\_8},
}

copyright notice, Springer-Verlag copyright notice
Last modified: Sun Sep 2 16:36:21 CEST 2018