Using program synthesis for program analysis
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 find...
| Main Authors: | , , |
|---|---|
| Other Authors: | |
| Format: | Conference item |
| Published: |
Springer
2015
|
| _version_ | 1826274527125962752 |
|---|---|
| author | David, C Kroening, D Lewis, M |
| author2 | Davis, M |
| author_facet | Davis, M David, C Kroening, D Lewis, M |
| author_sort | David, C |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-06T22:44:47Z |
| format | Conference item |
| id | oxford-uuid:5ccc0433-c5d1-4989-b1d6-658e18e4885a |
| institution | University of Oxford |
| last_indexed | 2024-03-06T22:44:47Z |
| publishDate | 2015 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:5ccc0433-c5d1-4989-b1d6-658e18e4885a2022-03-26T17:30:23ZUsing program synthesis for program analysisConference itemhttp://purl.org/coar/resource_type/c_5794uuid:5ccc0433-c5d1-4989-b1d6-658e18e4885aSymplectic Elements at OxfordSpringer2015David, CKroening, DLewis, MDavis, MFehnker, AMcIver, AVoronkov, AIn 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. |
| spellingShingle | David, C Kroening, D Lewis, M Using program synthesis for program analysis |
| title | Using program synthesis for program analysis |
| title_full | Using program synthesis for program analysis |
| title_fullStr | Using program synthesis for program analysis |
| title_full_unstemmed | Using program synthesis for program analysis |
| title_short | Using program synthesis for program analysis |
| title_sort | using program synthesis for program analysis |
| work_keys_str_mv | AT davidc usingprogramsynthesisforprogramanalysis AT kroeningd usingprogramsynthesisforprogramanalysis AT lewism usingprogramsynthesisforprogramanalysis |