Parallelizing an interactive theorem prover : functional programming and proofs with ACL2

dc.contributor.advisorHunt, Warren A., 1958-en
dc.contributor.committeeMemberBrowne, James Cen
dc.contributor.committeeMemberKaufmann, Matten
dc.contributor.committeeMemberMoore, J Sen
dc.contributor.committeeMemberSawada, Junen
dc.contributor.committeeMemberWitchel, Emmetten
dc.creatorRager, David Lawrenceen
dc.date.accessioned2013-02-15T17:33:23Zen
dc.date.issued2012-12en
dc.date.submittedDecember 2012en
dc.date.updated2013-02-15T17:33:23Zen
dc.descriptiontexten
dc.description.abstractMulti-core systems have become commonplace, however, theorem provers often do not take advantage of the additional computing resources in an interactive setting. This research explores automatically using these additional resources to lessen the delay between when users submit conjectures to the theorem prover and when they receive feedback from the prover that is useful in discovering how to successfully complete the proof of a particular theorem. This research contributes mechanisms that permit applicative programs to execute in parallel while simultaneously preparing these programs for verification by a semi-automatic reasoning system. It also contributes a parallel version of an automated theorem prover, with management of user interaction issues, such as output and how inherently single-threaded, user-level proof features can be configured for use with parallel computation. Finally, this dissertation investigates the types of proofs that are amenable to parallel execution. This investigation yields the result that almost all proof attempts that require a non-trivial amount of time can benefit from parallel execution. Proof attempts executed in parallel almost always provide the aforementioned feedback sooner than if they executed serially, and their execution time is often significantly reduced.en
dc.description.departmentComputer Sciencesen
dc.format.mimetypeapplication/pdfen
dc.identifier.urihttp://hdl.handle.net/2152/19482en
dc.language.isoen_USen
dc.subjectTheorem provingen
dc.subjectACL2en
dc.subjectParallelen
dc.subjectFunctional languagesen
dc.subjectParallel proof processen
dc.titleParallelizing an interactive theorem prover : functional programming and proofs with ACL2en
thesis.degree.departmentComputer Sciencesen
thesis.degree.disciplineComputer Scienceen
thesis.degree.grantorThe University of Texas at Austinen
thesis.degree.levelDoctoralen
thesis.degree.nameDoctor of Philosophyen
Files
Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
rager_dissertation_201291.pdf
Size:
2.75 MB
Format:
Adobe Portable Document Format
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
2.12 KB
Format:
Plain Text
Description: