Repository logo
 

Program Synthesis for Program Analysis

Accepted version
Peer-reviewed

Type

Article

Change log

Authors

David, CM 
Kesseli, Pascal 
Kroening, Daniel 
Lewis, Matt 

Abstract

In this paper, 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.

Description

Keywords

Journal Title

ACM Transactions on Programming Languages and Systems

Conference Name

Journal ISSN

Volume Title

Publisher

Publisher DOI

Publisher URL

Sponsorship
Royal Society (UF160079)