Program Synthesis for Program Analysis

Cristina David, Pascal Kesseli, Daniel Kroening, Matt Lewis

Research output: Contribution to journalArticle (Academic Journal)peer-review

83 Downloads (Pure)

Abstract

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.

Original languageEnglish
Article number5
Pages (from-to)1-45
JournalACM Transactions of Programming Languages and Systems
Volume40
Issue number2
DOIs
Publication statusPublished - 1 Jun 2018

Structured keywords

  • Programming Languages

Keywords

  • Program synthesis
  • program termination

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

Cite this