Journal article icon

Journal article

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

Expand abstract
Publication status:
Published
Peer review status:
Peer reviewed

Actions


Access Document


Files:
  • (Accepted manuscript, pdf, 906.9KB)
Publisher copy:
10.1145/3174802

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Role:
Author
More from this funder
Grant:
H2020 FET OPEN project 712689 SC2
Publisher:
Association for Computing Machinary Publisher's website
Journal:
ACM Transactions on Programming Languages and Systems Journal website
Volume:
40
Issue:
2
Article number:
5
Publication date:
2018-05-28
Acceptance date:
2017-12-03
DOI:
EISSN:
1558-4593
ISSN:
0164-0925
Source identifiers:
807765
Keywords:
Pubs id:
pubs:807765
UUID:
uuid:85fc101f-0c8b-46bf-99b7-58277636198b
Local pid:
pubs:807765
Deposit date:
2017-12-04

Terms of use


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP