Using Program Synthesis for Program Analysis

Cristina David*, Daniel Kroening, Matt Lewis

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)

59 Downloads (Pure)

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 capture numerous static analysis problems (e.g. safety proving, bug finding, termination and non-termination proving, superoptimisation). We call this fragment the synthesis fragment. We build a decision procedure for the synthesis fragment over finite domains in the form of a program synthesiser. Given our initial motivation to solve static analysis problems, this synthesiser is specialised for such analyses. Our experimental results show that, on benchmarks capturing static analysis problems, our program synthesiser compares positively with other general purpose synthesisers.
Original languageEnglish
Title of host publicationLogic for Programming, Artificial Intelligence, and Reasoning
Subtitle of host publication20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings
EditorsMartin Davis, Ansgar Fehnker, Annabelle McIver, Andrei Voronkov
Pages483-498
Number of pages16
ISBN (Electronic)978-3-662-48899-7
DOIs
Publication statusE-pub ahead of print - 22 Nov 2015

Structured keywords

  • Programming Languages

Fingerprint Dive into the research topics of 'Using Program Synthesis for Program Analysis'. Together they form a unique fingerprint.

Cite this