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
N1 - Publisher Copyright:
© The Author(s) 2018.
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 -