Advanced search options

Advanced Search Options 🞨

Browse by author name (“Author name starts with…”).

Find ETDs with:

in
/  
in
/  
in
/  
in

Written in Published in Earliest date Latest date

Sorted by

Results per page:

Sorted by: relevance · author · university · dateNew search

You searched for +publisher:"University of Texas – Austin" +contributor:("Hunt, Jr. , Warren A."). Showing records 1 – 3 of 3 total matches.

Search Limiters

Last 2 Years | English Only

No search limiters apply to these results.

▼ Search Limiters

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

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

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

Page 1 Page 2 Page 3 Page 4 Page 5 Page 6 Page 7

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th 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 (16th Edition):

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

MLA Handbook (7th Edition):

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

Vancouver:

Davis JC. A self-verifying theorem prover. [Internet] [Doctoral dissertation]. University of Texas – Austin; 2009. [cited 2021 Feb 26]. 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

2. Govindan, Madhu Sarava. E³ : energy-efficient EDGE architectures.

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

Increasing power dissipation is one of the most serious challenges facing designers in the microprocessor industry. Power dissipation, increasing wire delays, and increasing design complexity have forced industry to embrace multi-core architectures or chip multiprocessors (CMPs). While CMPs mitigate wire delays and design complexity, they do not directly address single-threaded performance. Additionally, programs must be parallelized, either manually or automatically, to fully exploit the performance of CMPs. Researchers have recently proposed an architecture called Explicit Data Graph Execution (EDGE) as an alternative to conventional CMPs. EDGE architectures are designed to be technology-scalable and to provide good single-threaded performance as well as exploit other types of parallelism including data-level and thread-level parallelism. In this dissertation, we examine the energy efficiency of a specific EDGE architecture called TRIPS Instruction Set Architecture (ISA) and two microarchitectures called TRIPS and TFlex that implement the TRIPS ISA. TRIPS microarchitecture is a first-generation design that proves the feasibility of the TRIPS ISA and distributed tiled microarchitectures. The second-generation TFlex microarchitecture addresses key inefficiencies of the TRIPS microarchitecture by matching the resource needs of applications to a composable hardware substrate. First, we perform a thorough power analysis of the TRIPS microarchitecture. We describe how we develop architectural power models for TRIPS. We then improve power-modeling accuracy using hardware power measurements on the TRIPS prototype combined with detailed Register Transfer Level (RTL) power models from the TRIPS design. Using these refined architectural power models and normalized power modeling methodologies, we perform a detailed performance and power comparison of the TRIPS microarchitecture with two different processors: 1) a low-end processor designed for power efficiency (ARM/XScale) and 2) a high-end superscalar processor designed for high performance (a variant of Power4). This detailed power analysis provides key insights into the advantages and disadvantages of the TRIPS ISA and microarchitecture compared to processors on either end of the performance-power spectrum. Our results indicate that the TRIPS microarchitecture achieves 11.7 times better energy efficiency compared to ARM, and approximately 12% better energy efficiency than Power4, in terms of the Energy-Delay-Squared (ED²) metric. Second, we evaluate the energy efficiency of the TFlex microarchitecture in comparison to TRIPS, ARM, and Power4. TFlex belongs to a class of microarchitectures called Composable Lightweight Processors (CLPs). CLPs are distributed microarchitectures designed with simple cores and are highly configurable at runtime to adapt to resource needs of applications. We develop power models for the TFlex microarchitecture based on the validated TRIPS power models. Our quantitative results indicate that by better matching execution resources to the needs of… Advisors/Committee Members: Keckler, Stephen W. (advisor), Burger, Douglas C. (committee member), McKinley, Kathryn S. (committee member), Chiou, Derek (committee member), Hunt, Jr., Warren A. (committee member), Brooks, David (committee member).

Subjects/Keywords: Energy efficiency; EDGE architectures; Power efficiency; Composability; DVFS; Power management; Dynamic voltage and frequency scaling; Explicit Data Graph Execution architectures

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Govindan, M. S. (2010). E³ : energy-efficient EDGE architectures. (Doctoral Dissertation). University of Texas – Austin. Retrieved from http://hdl.handle.net/2152/ETD-UT-2010-08-1934

Chicago Manual of Style (16th Edition):

Govindan, Madhu Sarava. “E³ : energy-efficient EDGE architectures.” 2010. Doctoral Dissertation, University of Texas – Austin. Accessed February 26, 2021. http://hdl.handle.net/2152/ETD-UT-2010-08-1934.

MLA Handbook (7th Edition):

Govindan, Madhu Sarava. “E³ : energy-efficient EDGE architectures.” 2010. Web. 26 Feb 2021.

Vancouver:

Govindan MS. E³ : energy-efficient EDGE architectures. [Internet] [Doctoral dissertation]. University of Texas – Austin; 2010. [cited 2021 Feb 26]. Available from: http://hdl.handle.net/2152/ETD-UT-2010-08-1934.

Council of Science Editors:

Govindan MS. E³ : energy-efficient EDGE architectures. [Doctoral Dissertation]. University of Texas – Austin; 2010. Available from: http://hdl.handle.net/2152/ETD-UT-2010-08-1934

3. Harrison, Amelia J. Formal methods for answer set programming.

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

Answer set programming (ASP) is a declarative programming paradigm for the design and implementation of knowledge-intensive applications, particularly useful for modeling problems involving combinatorial search. The input languages of the first ASP software systems had the attractive property of a simple, fully specified declarative semantics, making it possible to use formal methods to analyze ASP programs  – to verify correctness, for example, or to show that two programs were equivalent. Since that time, many useful new constructs have been added to input languages. The increase in usability, however, has come at the expense of a fully specified semantics, as the semantics of newer constructs has not quite kept pace with the most general syntax that solvers can handle. In this thesis, we will describe one approach to bridging the gap between mathematical formulations of the semantics of ASP languages and the current state of the languages themselves. Our approach is to view ASP programs as corresponding to infinitary formulas (formulas with infinitely long conjunctions and disjunctions). Advisors/Committee Members: Lifschitz, Vladimir (advisor), Boyer, Robert S. (committee member), Dillig, Isil (committee member), Hunt, Jr. , Warren A. (committee member), Schaub, Torsten (committee member).

Subjects/Keywords: Logic programming; Formal methods

Page 1 Page 2 Page 3 Page 4 Page 5 Page 6 Page 7 Sample image

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Harrison, A. J. (2018). Formal methods for answer set programming. (Doctoral Dissertation). University of Texas – Austin. Retrieved from http://hdl.handle.net/2152/63692

Chicago Manual of Style (16th Edition):

Harrison, Amelia J. “Formal methods for answer set programming.” 2018. Doctoral Dissertation, University of Texas – Austin. Accessed February 26, 2021. http://hdl.handle.net/2152/63692.

MLA Handbook (7th Edition):

Harrison, Amelia J. “Formal methods for answer set programming.” 2018. Web. 26 Feb 2021.

Vancouver:

Harrison AJ. Formal methods for answer set programming. [Internet] [Doctoral dissertation]. University of Texas – Austin; 2018. [cited 2021 Feb 26]. Available from: http://hdl.handle.net/2152/63692.

Council of Science Editors:

Harrison AJ. Formal methods for answer set programming. [Doctoral Dissertation]. University of Texas – Austin; 2018. Available from: http://hdl.handle.net/2152/63692

.