Show simple item record

dc.contributor.authorDavid, Cristina
dc.contributor.authorKesseli, Pascal
dc.contributor.authorKroening, Daniel
dc.contributor.authorLewis, Matt
dc.date.accessioned2018-05-16T09:48:30Z
dc.date.available2018-05-16T09:48:30Z
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/275832
dc.description.abstractIn 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 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. We provide instantiations of our framework for solving a diverse range of program verification tasks such as termination, non-termination, safety and bug finding, superoptimisation and refactoring. Our experimental results show that our program synthesiser compares positively with specialised tools in each area as well as with general-purpose synthesisers.
dc.titleProgram Synthesis for Program Analysis
dc.typeArticle
prism.publicationNameACM Transactions on Programming Languages and Systems
dc.identifier.doi10.17863/CAM.23098
dcterms.dateAccepted2017-12-03
rioxxterms.versionAM
rioxxterms.licenseref.urihttp://www.rioxx.net/licenses/all-rights-reserved
rioxxterms.licenseref.startdate2017-12-03
rioxxterms.typeJournal Article/Review
pubs.funder-project-idRoyal Society (UF160079)
rioxxterms.freetoread.startdate2019-05-16


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record