Advanced search options

Sorted by: relevance · author · university · date | New search

You searched for `+publisher:"University of Texas – Austin" +contributor:("Kaufmann, Matt")`

.
Showing records 1 – 3 of
3 total matches.

▼ Search Limiters

1. -8037-0201. Formal verification of application and system programs based on a validated x86 ISA model.

Degree: PhD, Computer science, 2016, University of Texas – Austin

URL: http://hdl.handle.net/2152/46437

Two main kinds of tools available for formal software verification are point tools and general-purpose tools. Point tools are targeted towards bug-hunting or proving a fixed set of properties, such as establishing the absence of buffer overflows. These tools have become a practical choice in the development and analysis of serious software systems, largely because they are easy to use. However, point tools are limited in their scope because they are pre-programmed to reason about a fixed set of behaviors. In contrast, general-purpose tools,like theorem provers, have a wider scope. Unfortunately, they also have a higher user overhead. These tools often use incomplete and/or unrealistic software models, in part to reduce this overhead. Formal verification based on such a model can be restrictive because it does not account for program behaviors that rely on missing features in the model. The results of such formal verification undertakings may be unreliable – consequently, they can offer a false sense of security. This dissertation demonstrates that formal verification of complex program properties can be made practical, without any loss of accuracy or expressiveness, by employing a machine-code analysis framework implemented using a mechanical theorem prover. To this end, we constructed a formal and executable model of the x86 Instruction-Set Architecture using the ACL2 theorem-proving system. This model includes a specification of 400+ x86 opcodes and architectural features like segmentation and paging. The model's high execution speed allows it to be validated routinely by performing co-simulations against a physical x86 processor – thus, formal analysis based on this model is reliable. We also developed a general framework for x86 machine-code analysis that can lower the overhead associated with the verification of a broad range of program properties, including correctness with respect to behavior, security, and resource requirements. We illustrate the capabilities of our framework by describing the verification of two application programs, population count and word count, and one system program, zero copy.
*Advisors/Committee Members: Hunt, Warren A., 1958- (advisor), Alvisi, Lorenzo (committee member), Kaufmann, Matt (committee member), Lin, Calvin (committee member), Moore, J S (committee member), Watson, Robert (committee member).*

Subjects/Keywords: Formal verification; x86 Machine-code analysis; x86 ISA; ACL2; Theorem proving; Program verification

Record Details Similar Records

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^{th} Edition):

-8037-0201. (2016). Formal verification of application and system programs based on a validated x86 ISA model. (Doctoral Dissertation). University of Texas – Austin. Retrieved from http://hdl.handle.net/2152/46437

Note: this citation may be lacking information needed for this citation format:

Author name may be incomplete

Chicago Manual of Style (16^{th} Edition):

-8037-0201. “Formal verification of application and system programs based on a validated x86 ISA model.” 2016. Doctoral Dissertation, University of Texas – Austin. Accessed February 28, 2021. http://hdl.handle.net/2152/46437.

Note: this citation may be lacking information needed for this citation format:

Author name may be incomplete

MLA Handbook (7^{th} Edition):

-8037-0201. “Formal verification of application and system programs based on a validated x86 ISA model.” 2016. Web. 28 Feb 2021.

Note: this citation may be lacking information needed for this citation format:

Author name may be incomplete

Vancouver:

-8037-0201. Formal verification of application and system programs based on a validated x86 ISA model. [Internet] [Doctoral dissertation]. University of Texas – Austin; 2016. [cited 2021 Feb 28]. Available from: http://hdl.handle.net/2152/46437.

Author name may be incomplete

Council of Science Editors:

-8037-0201. Formal verification of application and system programs based on a validated x86 ISA model. [Doctoral Dissertation]. University of Texas – Austin; 2016. Available from: http://hdl.handle.net/2152/46437

Author name may be incomplete

2. Davis, Jared Curran. A self-verifying theorem prover.

Degree: PhD, Computer Sciences, 2009, University of Texas – Austin

URL: http://hdl.handle.net/2152/ETD-UT-2009-12-435

Programs have precise semantics, so we can use mathematical proof to establish their properties. These proofs are often too large to validate with the usual "social process" of mathematics, so instead we create and check them with theorem-proving software. This software must be advanced enough to make the proof process tractable, but this very sophistication casts doubt upon the whole enterprise: who verifies the verifier?
We begin with a simple proof checker, Level 1, that only accepts proofs composed of the most primitive steps, like Instantiation and Cut. This program is so straightforward the ordinary, social process can establish its soundness and the consistency of the logical theory it implements (so we know theorems are "always true").
Next, we develop a series of increasingly capable proof checkers, Level 2, Level 3, etc. Each new proof checker accepts new kinds of proof steps which were not accepted in the previous levels. By taking advantage of these new proof steps, higher-level proofs can be written more concisely than lower-level proofs, and can take less time to construct and check. Our highest-level proof checker, Level 11, can be thought of as a simplified version of the ACL2 or NQTHM theorem provers. One contribution of this work is to show how such systems can be verified.
To establish that the Level 11 proof checker can be trusted, we first use it, without trusting it, to prove the fidelity of every Level n to Level 1: whenever Level n accepts a proof of some phi, there exists a Level 1 proof of phi. We then mechanically translate the Level 11 proof for each Level n into a Level n - 1 proof – that is, we create a Level 1 proof of Level 2's fidelity, a Level 2 proof of Level 3's fidelity, and so on. This layering shows that each level can be trusted, and allows us to manage the sizes of these proofs.
In this way, our system proves its own fidelity, and trusting Level 11 only requires us to trust Level 1.
*Advisors/Committee Members: Moore, J Strother, 1947- (advisor), Emerson, E. Allen (committee member), Harrison, John (committee member), Hunt, Jr., Warren A. (committee member), Kaufmann, Matt (committee member), Lifschitz, Vladimir (committee member).*

Subjects/Keywords: Milawa; mathematical logic; formal verification; Lisp; proof checking; theorem proving; automated reasoning; reflection; soundness; fidelity; faithfulness; rewriting; proof building; tactics; first-order logic; verified verifier

Record Details Similar Records

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^{th} Edition):

Davis, J. C. (2009). A self-verifying theorem prover. (Doctoral Dissertation). University of Texas – Austin. Retrieved from http://hdl.handle.net/2152/ETD-UT-2009-12-435

Chicago Manual of Style (16^{th} Edition):

Davis, Jared Curran. “A self-verifying theorem prover.” 2009. Doctoral Dissertation, University of Texas – Austin. Accessed February 28, 2021. http://hdl.handle.net/2152/ETD-UT-2009-12-435.

MLA Handbook (7^{th} Edition):

Davis, Jared Curran. “A self-verifying theorem prover.” 2009. Web. 28 Feb 2021.

Vancouver:

Davis JC. A self-verifying theorem prover. [Internet] [Doctoral dissertation]. University of Texas – Austin; 2009. [cited 2021 Feb 28]. Available from: http://hdl.handle.net/2152/ETD-UT-2009-12-435.

Council of Science Editors:

Davis JC. A self-verifying theorem prover. [Doctoral Dissertation]. University of Texas – Austin; 2009. Available from: http://hdl.handle.net/2152/ETD-UT-2009-12-435

3. Rager, David Lawrence. Parallelizing an interactive theorem prover : functional programming and proofs with ACL2.

Degree: PhD, Computer Science, 2012, University of Texas – Austin

URL: http://hdl.handle.net/2152/19482

Multi-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.
*Advisors/Committee Members: Hunt, Warren A., 1958- (advisor), Browne, James C (committee member), Kaufmann, Matt (committee member), Moore, J S (committee member), Sawada, Jun (committee member), Witchel, Emmett (committee member).*

Subjects/Keywords: Theorem proving; ACL2; Parallel; Functional languages; Parallel proof process

Record Details Similar Records

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^{th} Edition):

Rager, D. L. (2012). Parallelizing an interactive theorem prover : functional programming and proofs with ACL2. (Doctoral Dissertation). University of Texas – Austin. Retrieved from http://hdl.handle.net/2152/19482

Chicago Manual of Style (16^{th} Edition):

Rager, David Lawrence. “Parallelizing an interactive theorem prover : functional programming and proofs with ACL2.” 2012. Doctoral Dissertation, University of Texas – Austin. Accessed February 28, 2021. http://hdl.handle.net/2152/19482.

MLA Handbook (7^{th} Edition):

Rager, David Lawrence. “Parallelizing an interactive theorem prover : functional programming and proofs with ACL2.” 2012. Web. 28 Feb 2021.

Vancouver:

Rager DL. Parallelizing an interactive theorem prover : functional programming and proofs with ACL2. [Internet] [Doctoral dissertation]. University of Texas – Austin; 2012. [cited 2021 Feb 28]. Available from: http://hdl.handle.net/2152/19482.

Council of Science Editors:

Rager DL. Parallelizing an interactive theorem prover : functional programming and proofs with ACL2. [Doctoral Dissertation]. University of Texas – Austin; 2012. Available from: http://hdl.handle.net/2152/19482