Program Synthesis for Program Analysis
View / Open Files
Authors
David, Cristina
Kesseli, Pascal
Kroening, Daniel
Lewis, Matt
Journal Title
ACM Transactions on Programming Languages and Systems
Type
Article
This Version
AM
Metadata
Show full item recordCitation
David, C., Kesseli, P., Kroening, D., & Lewis, M. Program Synthesis for Program Analysis. ACM Transactions on Programming Languages and Systems https://doi.org/10.17863/CAM.23098
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.
Sponsorship
Royal Society (UF160079)
Identifiers
This record's DOI: https://doi.org/10.17863/CAM.23098
This record's URL: https://www.repository.cam.ac.uk/handle/1810/275832
Rights
Licence:
http://www.rioxx.net/licenses/all-rights-reserved
Statistics
Total file downloads (since January 2020). For more information on metrics see the
IRUS guide.