Program synthesis for program analysis

Journal article

In this article, we propose a unified framework for designing static analysers based on program synthesis. For this purpose, we identify a fragment of second-order logic with restricted quantification that is expressive enough to model numerous static analysis problems (e.g., safety proving, bug finding, termination and non-termination proving, refactoring). As our focus is on programs that use bit-vectors, we build a decision procedure for this fragment over finite domains in the form of a program synthesiser. We provide instantiations of our framework for solving a diverse range of program verification tasks such as termination, non-termination, safety and bug finding, superoptimisation, and refactoring. Our experimental results show that our program synthesiser compares positively with specialised tools in each area as well as with general-purpose synthesisers.

Authors: David, C; Kesseli, P; Kroening, D; Lewis, M

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Association for Computing Machinary
• Journal: ACM Transactions on Programming Languages and Systems
• Volume: 40
• Issue: 2
• Article number: 5
• Publication date: 2018-05-28
• Acceptance date: 2017-12-03
• DOI: 10.1145/3174802
• EISSN: 1558-4593
• ISSN: 0164-0925
• Keywords: program synthesis; program termination