Show simple item record

Finding Kernels in Non-Linear Data-Driven CHC Solving

dc.contributor.advisorHarris, William R.
dc.contributor.advisorHarris, William R.
dc.contributor.authorEden, Michael
dc.date.accessioned2018-08-20T19:11:06Z
dc.date.available2018-08-20T19:11:06Z
dc.date.created2018-08
dc.date.submittedAugust 2018
dc.identifier.urihttp://hdl.handle.net/1853/60382
dc.description.abstractProgram verification has seen a lot of progress, but its still unable to automatically find proofs for industry programs. This paper builds on data-driven approaches from previous work [11] to provide a more robust automatic prover for programs with non-linear loop invariants. It does so by attempting to find the correct kernel for the relation that makes the invariant linear. This is an easy addition to existing systems and can be used with any data-driven approach, allowing it to be easily implemented on top of them. By finding a suitable kernel, many difficult non-linear invariants are easily found.
dc.format.mimetypeapplication/pdf
dc.language.isoen_US
dc.publisherGeorgia Institute of Technology
dc.subjectCHC
dc.subjectZ3
dc.subjectHorn Clause
dc.subjectStatic Analysis
dc.subjectVerification
dc.subjectCHC
dc.subjectZ3
dc.subjectHorn Clause
dc.subjectStatic Analysis
dc.subjectVerification
dc.titleFinding Kernels in Non-Linear Data-Driven CHC Solving
dc.titleFinding Kernels in Non-Linear Data-Driven CHC Solving
dc.typeUndergraduate Research Option Thesis
dc.description.degreeUndergraduate
dc.contributor.departmentComputer Science
thesis.degree.levelUndergraduate
dc.contributor.committeeMemberOrso, Alessandro
dc.contributor.committeeMemberOrso, Alessandro
dc.date.updated2018-08-20T19:11:06Z


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record