Program Synthesis for Program Analysis
ACM Transactions on Programming Languages and Systems
MetadataShow full item record
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
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.
Royal Society (UF160079)
This record's DOI: https://doi.org/10.17863/CAM.23098
This record's URL: https://www.repository.cam.ac.uk/handle/1810/275832