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 | |
Publication status | Published - 1 Jun 2018 |
Research Groups and Themes
- Programming Languages
Keywords
- Program synthesis
- program termination