Program Synthesis for Program Analysis

Cristina David; Pascal  Kesseli; Daniel  Kroening; Matt  Lewis

doi:10.1145/3174802

Program Synthesis for Program Analysis

Cristina David, Pascal Kesseli, Daniel Kroening, Matt Lewis

Research output: Contribution to journal › Article (Academic Journal) › peer-review

7 Citations (Scopus)

383 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 language	English
Article number	5
Pages (from-to)	1-45
Journal	ACM Transactions of Programming Languages and Systems
Volume	40
Issue number	2
DOIs	https://doi.org/10.1145/3174802
Publication status	Published - 1 Jun 2018

Research Groups and Themes

Programming Languages

Keywords

Program synthesis
program termination

Access to Document

10.1145/3174802

Full-text PDF (author’s accepted manuscript)
This is the author accepted manuscript (AAM). The final published version (version of record) is available online via Association for Computing Machinery at https://doi.org/10.1145/3174802 . Please refer to any applicable terms of use of the publisher.
Accepted author manuscript, 987 KB

Handle.net

Persistent link

Dr Cristina David
- cristina.davidbristol.acuk
- School of Computer Science - Senior Lecturer
Person: Academic

Cite this

@article{7544772c1b6742ac96473487609655f0,

title = "Program Synthesis for Program Analysis",

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. ",

keywords = "Program synthesis, program termination",

author = "Cristina David and Pascal Kesseli and Daniel Kroening and Matt Lewis",

year = "2018",

month = jun,

day = "1",

doi = "10.1145/3174802",

language = "English",

volume = "40",

pages = "1--45",

journal = "ACM Transactions of Programming Languages and Systems",

issn = "0164-0925",

publisher = "Association for Computing Machinery",

number = "2",

}

TY - JOUR

T1 - Program Synthesis for Program Analysis

AU - David, Cristina

AU - Kesseli, Pascal

AU - Kroening, Daniel

AU - Lewis, Matt

PY - 2018/6/1

Y1 - 2018/6/1

N2 - 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.

AB - 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.

KW - Program synthesis

KW - program termination

U2 - 10.1145/3174802

DO - 10.1145/3174802

M3 - Article (Academic Journal)

SN - 0164-0925

VL - 40

SP - 1

EP - 45

JO - ACM Transactions of Programming Languages and Systems

JF - ACM Transactions of Programming Languages and Systems

IS - 2

M1 - 5

ER -

Program Synthesis for Program Analysis

Abstract

Research Groups and Themes

Keywords

Access to Document

Handle.net

Fingerprint

Profiles

Dr Cristina David

Cite this