+publisher:"University of Texas – Austin" +contributor:("Emerson, E. Allen")

1. Samanta, Roopsha. Program reliability through algorithmic design and analysis.

Degree: PhD, Electrical and Computer Engineering, 2013, University of Texas – Austin

► Software systems are ubiquitous in today's world and yet, remain vulnerable to the fallibility of human programmers as well as the unpredictability of their operating… (more)

▼ Software systems are ubiquitous in today's world and yet, remain vulnerable to the fallibility of human programmers as well as the unpredictability of their operating environments. The overarching goal of this dissertation is to develop algorithms to enable automated and efficient design and analysis of reliable programs. In the first and second parts of this dissertation, we focus on the development of programs that are free from programming errors. The intent is not to eliminate the human programmer, but instead to complement his or her expertise, with sound and efficient computational techniques, when possible. To this end, we make contributions in two specific domains. Program debugging – the process of fault localization and error elimination from a program found to be incorrect – typically relies on expert human intuition and experience, and is often a lengthy, expensive part of the program development cycle. In the first part of the dissertation, we target automated debugging of sequential programs. A broad and informal statement of the (automated) program debugging problem is to suitably modify an erroneous program, say P, to obtain a correct program, say P'. This problem is undecidable in general; it is hard to formalize; moreover, it is particularly challenging to assimilate and mechanize the customized, expert programmer intuition involved in the choices made in manual program debugging. Our first contribution in this domain is a methodical formalization of the program debugging problem, that enables automation, while incorporating expert programmer intuition and intent. Our second contribution is a solution framework that can debug infinite-state, imperative, sequential programs written in higher-level programming languages such as C. Boolean programs, which are smaller, finite-state abstractions of infinite-state or large, finite-state programs, have been found to be tractable for program verification. In this dissertation, we utilize Boolean programs for program debugging. Our solution framework involves two main steps: (a) automated debugging of a Boolean program, corresponding to an erroneous program P, and (b) translation of the corrected Boolean program into a correct program P'. Shared-memory concurrent programs are notoriously difficult to write, verify and debug; this makes them excellent targets for automated program completion, in particular, for synthesis of synchronization code. Extant work in this domain has focused on either propositional temporal logic specifications with simplistic models of concurrent programs, or more refined program models with the specifications limited to just safety properties. Moreover, there has been limited effort in developing adaptable and fully-automatic synthesis frameworks that are capable of generating synchronization at different levels of abstraction and granularity. In the second part of this dissertation, we present a framework for synthesis of synchronization for shared-memory concurrent programs with respect to temporal logic… Advisors/Committee Members: Emerson, E. Allen (advisor), Garg, Vijay K. (Vijay Kumar), 1963- (advisor).

Subjects/Keywords: Automated program repair; Automated program debugging; Automated program synthesis; Automated synchronization synthesis; Robustness analysis

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Samanta, R. (2013). Program reliability through algorithmic design and analysis. (Doctoral Dissertation). University of Texas – Austin. Retrieved from http://hdl.handle.net/2152/23103

Chicago Manual of Style (16^th Edition):

Samanta, Roopsha. “Program reliability through algorithmic design and analysis.” 2013. Doctoral Dissertation, University of Texas – Austin. Accessed February 27, 2021. http://hdl.handle.net/2152/23103.

MLA Handbook (7^th Edition):

Samanta, Roopsha. “Program reliability through algorithmic design and analysis.” 2013. Web. 27 Feb 2021.

Vancouver:

Samanta R. Program reliability through algorithmic design and analysis. [Internet] [Doctoral dissertation]. University of Texas – Austin; 2013. [cited 2021 Feb 27]. Available from: http://hdl.handle.net/2152/23103.

Council of Science Editors:

Samanta R. Program reliability through algorithmic design and analysis. [Doctoral Dissertation]. University of Texas – Austin; 2013. Available from: http://hdl.handle.net/2152/23103

University of Texas – Austin

2. Wahl, Thomas, 1973-. Exploiting replication in automated program verification.

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

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

► This dissertation shows how systems of many concurrent components, which naively engender intractably large state spaces, can nevertheless be successfully subject to exhaustive formal verification,… (more)

▼ This dissertation shows how systems of many concurrent components, which naively engender intractably large state spaces, can nevertheless be successfully subject to exhaustive formal verification, provided the components can be classified into a few types. It therefore addresses an instance of the state explosion problem: a finite-state model of a system can be much larger than a high-level description of this system. Model checking, the technique to which this dissertation is primarily devoted, inherently relies on state space exploration and thus suffers from this problem more than other formal verification methods. The state explosion phenomenon persists even if the system consists of components that are simply replicated instances of a generic behavioral description. Examples of such systems abound; they include processes executing concurrently according to some common protocol, clusters of processors executing a parallel provii gram, and hardware with replicated physical devices in a uniform arrangement. Fortunately, models of such systems often exhibit a regular structure, known as symmetry, which can be exploited in verification, sometimes to the extent of an exponential reduction in model size. The first contribution of this dissertation is to show how reductions based on symmetry can be performed with state-of-the-art system representations. Many of today’s computing systems induce astronomically large state spaces whose formal models require a symbolic encoding using boolean formulas. Such succinct representations call for new algorithms that can process entire sets of objects at once. How to detect symmetry quickly during symbolic model checking, so that redundancy in the exploration can be avoided, was an open problem for some time. In this dissertation we provide an efficient and flexible solution to this problem by using symbolic data structures in a somewhat unconventional way. The second contribution is to extend symmetry reduction techniques to more realistic and general scenarios. We establish that the principal ideas still apply if symmetry is violated in parts of the state space. Such scenarios are common in practice, for instance when priorities determine which of several competing processes can access a resource first. In these situations it is beneficial to exploit symmetry where it exists and watch out for the (few) violations, rather than to ignore it altogether. We also demonstrate how symmetry can help us solve a practically significant instance of parameterized verification of system families. This technique traditionally attempts to prove properties about systems independently of the size parameter, but requires models of a special structure. We show that by restricting the parameter to a finite range we can solve this problem efficiently, can do so without any conditions on the models’ structure, and can take advantage of symmetry in the individual systems of the family if it exists. Advisors/Committee Members: Emerson, E. Allen (advisor).

Subjects/Keywords: Computer software – Verification; Formal methods (Computer science)

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Wahl, Thomas, 1. (2007). Exploiting replication in automated program verification. (Doctoral Dissertation). University of Texas – Austin. Retrieved from http://hdl.handle.net/2152/3338

Chicago Manual of Style (16^th Edition):

Wahl, Thomas, 1973-. “Exploiting replication in automated program verification.” 2007. Doctoral Dissertation, University of Texas – Austin. Accessed February 27, 2021. http://hdl.handle.net/2152/3338.

MLA Handbook (7^th Edition):

Wahl, Thomas, 1973-. “Exploiting replication in automated program verification.” 2007. Web. 27 Feb 2021.

Vancouver:

Wahl, Thomas 1. Exploiting replication in automated program verification. [Internet] [Doctoral dissertation]. University of Texas – Austin; 2007. [cited 2021 Feb 27]. Available from: http://hdl.handle.net/2152/3338.

Council of Science Editors:

Wahl, Thomas 1. Exploiting replication in automated program verification. [Doctoral Dissertation]. University of Texas – Austin; 2007. Available from: http://hdl.handle.net/2152/3338

University of Texas – Austin

3. Iyer, Subramanian Krishnan. Efficient and effective symbolic model checking.

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

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

► The main bottleneck in practical symbolic model checking is that it is restricted by the ability to efficiently represent and perform operations on sets of… (more)

▼ The main bottleneck in practical symbolic model checking is that it is restricted by the ability to efficiently represent and perform operations on sets of states. Symbolic representations, like Binary Decision Diagrams, grow very large quickly due to their necessity to cover the state space in a breadth first fashion. Satisfiability based techniques result in a proliferation of clauses, one reason being that they have to replicate the transition relation numerous times. We propose techniques to increase the capacity of automatic state-based verification as applied to sequential designs, i.e., symbolic model checking. Firstly, we propose the use of dynamically partitioned ordered Binary Decision Diagrams as a capable data structure. This leads to vast improvements in state space traversal in general and error detection in buggy designs, in particular. Secondly, we propose a partitioned approach to model checking, which splits the problem into multiple partitions handled independently of each other. State space partitioning-based approaches have been proposed in the literature to address the state explosion problem in model checking. These approaches, whether sequential or distributed, perform a large amount of work in the form of inter-partition (cross-over) image computations, which can be expensive. We present a model checking algorithm that aggregates these expensive cross-over images by localizing computation to individual partitions. This algorithm is more suited to parallelization than existing model checking approaches. It reduces the number of cross-over images and drastically outperforms extant approaches in terms of cross-over image computation cost as well as total model checking time, often by two orders of magnitude. We address the issue of time scalability in verification, whereby the availability of larger amounts of computation time enables greater exploration of the state space. From a practical standpoint, we observe that extant verification approaches are unable to proceed very deep into the state space. It is our conjecture that partitioning can help in this context and we explore this issue further. Finally, we study the combination of partitioned binary decision diagrams with bounded model checking for more scalable and efficient model checking. We give a technique to scale formal verification to a large grid of processors that demonstrates marked superiority over existing approaches. The contributions of this dissertation are in improving the capacity of symbolic model checking approaches to formal verification, in terms of time and memory requirements, as well as in the development of techniques that are more readily amenable to parallel and distributed model checking. Advisors/Committee Members: Emerson, E. Allen (advisor).

Subjects/Keywords: Computer programs – Verification; State-space methods; Formal methods (Computer science)

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Iyer, S. K. (2006). Efficient and effective symbolic model checking. (Doctoral Dissertation). University of Texas – Austin. Retrieved from http://hdl.handle.net/2152/2888

Chicago Manual of Style (16^th Edition):

Iyer, Subramanian Krishnan. “Efficient and effective symbolic model checking.” 2006. Doctoral Dissertation, University of Texas – Austin. Accessed February 27, 2021. http://hdl.handle.net/2152/2888.

MLA Handbook (7^th Edition):

Iyer, Subramanian Krishnan. “Efficient and effective symbolic model checking.” 2006. Web. 27 Feb 2021.

Vancouver:

Iyer SK. Efficient and effective symbolic model checking. [Internet] [Doctoral dissertation]. University of Texas – Austin; 2006. [cited 2021 Feb 27]. Available from: http://hdl.handle.net/2152/2888.

Council of Science Editors:

Iyer SK. Efficient and effective symbolic model checking. [Doctoral Dissertation]. University of Texas – Austin; 2006. Available from: http://hdl.handle.net/2152/2888

University of Texas – Austin

4. Amla, Nina. Efficient model checking for timing diagrams.

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

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

Subjects/Keywords: Computer systems; Computer software

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Amla, N. (2001). Efficient model checking for timing diagrams. (Doctoral Dissertation). University of Texas – Austin. Retrieved from http://hdl.handle.net/2152/1681

Chicago Manual of Style (16^th Edition):

Amla, Nina. “Efficient model checking for timing diagrams.” 2001. Doctoral Dissertation, University of Texas – Austin. Accessed February 27, 2021. http://hdl.handle.net/2152/1681.

MLA Handbook (7^th Edition):

Amla, Nina. “Efficient model checking for timing diagrams.” 2001. Web. 27 Feb 2021.

Vancouver:

Amla N. Efficient model checking for timing diagrams. [Internet] [Doctoral dissertation]. University of Texas – Austin; 2001. [cited 2021 Feb 27]. Available from: http://hdl.handle.net/2152/1681.

Council of Science Editors:

Amla N. Efficient model checking for timing diagrams. [Doctoral Dissertation]. University of Texas – Austin; 2001. Available from: http://hdl.handle.net/2152/1681

University of Texas – Austin

5. Kahlon, Vineet. Model checking: beyond the finite.

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

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

Subjects/Keywords: Computer programs – Verification

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Kahlon, V. (2004). Model checking: beyond the finite. (Doctoral Dissertation). University of Texas – Austin. Retrieved from http://hdl.handle.net/2152/1158

Chicago Manual of Style (16^th Edition):

Kahlon, Vineet. “Model checking: beyond the finite.” 2004. Doctoral Dissertation, University of Texas – Austin. Accessed February 27, 2021. http://hdl.handle.net/2152/1158.

MLA Handbook (7^th Edition):

Kahlon, Vineet. “Model checking: beyond the finite.” 2004. Web. 27 Feb 2021.

Vancouver:

Kahlon V. Model checking: beyond the finite. [Internet] [Doctoral dissertation]. University of Texas – Austin; 2004. [cited 2021 Feb 27]. Available from: http://hdl.handle.net/2152/1158.

Council of Science Editors:

Kahlon V. Model checking: beyond the finite. [Doctoral Dissertation]. University of Texas – Austin; 2004. Available from: http://hdl.handle.net/2152/1158

6. 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… (more)

▼ 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 Cite « Share

❌

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 27, 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. 27 Feb 2021.

Vancouver:

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

7. Wehrman, Ian Anthony. Weak-memory local reasoning.

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

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

► Program logics are formal logics designed to facilitate specification and correctness reasoning for software programs. Separation logic, a recent program logic for C-like programs, has… (more)

Subjects/Keywords: Programming; Formal methods; Concurrency; Memory models

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Wehrman, I. A. (2012). Weak-memory local reasoning. (Doctoral Dissertation). University of Texas – Austin. Retrieved from http://hdl.handle.net/2152/19475

Chicago Manual of Style (16^th Edition):

Wehrman, Ian Anthony. “Weak-memory local reasoning.” 2012. Doctoral Dissertation, University of Texas – Austin. Accessed February 27, 2021. http://hdl.handle.net/2152/19475.

MLA Handbook (7^th Edition):

Wehrman, Ian Anthony. “Weak-memory local reasoning.” 2012. Web. 27 Feb 2021.

Vancouver:

Wehrman IA. Weak-memory local reasoning. [Internet] [Doctoral dissertation]. University of Texas – Austin; 2012. [cited 2021 Feb 27]. Available from: http://hdl.handle.net/2152/19475.

Council of Science Editors:

Wehrman IA. Weak-memory local reasoning. [Doctoral Dissertation]. University of Texas – Austin; 2012. Available from: http://hdl.handle.net/2152/19475

University of Texas – Austin

8. Deshmukh, Jyotirmoy Vinay. Verification of sequential and concurrent libraries.

Degree: PhD, Electrical and Computer Engineering, 2010, University of Texas – Austin

URL: http://hdl.handle.net/2152/ETD-UT-2010-08-1771

► The goal of this dissertation is to present new and improved techniques for fully automatic verification of sequential and concurrent software libraries. In most cases,… (more)

▼ The goal of this dissertation is to present new and improved techniques for fully automatic verification of sequential and concurrent software libraries. In most cases, automatic software verification is plagued by undecidability, while in many others it suffers from prohibitively high computational complexity. Model checking – a highly successful technique used for verifying finite state hardware circuits against logical specifications – has been less widely adapted for software, as software verification tends to involve reasoning about potentially infinite state-spaces. Two of the biggest culprits responsible for making software model checking hard are heap-allocated data structures and concurrency. In the first part of this dissertation, we study the problem of verifying shape properties of sequential data structure libraries. Such libraries are implemented as collections of methods that manipulate the underlying data structure. Examples of such methods include: methods to insert, delete, and update data values of nodes in linked lists, binary trees, and directed acyclic graphs; methods to reverse linked lists; and methods to rotate balanced trees. Well-written methods are accompanied by documentation that specifies the observational behavior of these methods in terms of pre/post-conditions. A pre-condition [phi] for a method M characterizes the state of a data structure before the method acts on it, and the post-condition [psi] characterizes the state of the data structure after the method has terminated. In a certain sense, we can view the method as a function that operates on an input data structure, producing an output data structure. Examples of such pre/post-conditions include shape properties such as acyclicity, sorted-ness, tree-ness, reachability of particular data values, and reachability of pointer values, and data structure-specific properties such as: "no red node has a red child'', and "there is no node with data value 'a' in the data structure''. Moreover, methods are often expected not to violate certain safety properties such as the absence of dangling pointers, absence of null pointer dereferences, and absence of memory leaks. We often assume such specifications as implicit, and say that a method is incorrect if it violates such specifications. We model data structures as directed graphs, and use the two terms interchangeably. Verifying correctness of methods operating on graphs is an instance of the parameterized verification problem: for every input graph that satisfies [phi], we wish to ensure that the corresponding output graph satisfies [psi]. Control structures such as loops and recursion allow an arbitrary method to simulate a Turing Machine. Hence, the parameterized verification problem for arbitrary methods is undecidable. One of the main contributions of this dissertation is in identifying mathematical conditions on a programming language fragment for which parameterized verification is not only decidable, but also efficient from a complexity perspective. The decidable fragment we… Advisors/Committee Members: Emerson, E. Allen (advisor), Aziz, Adnan (advisor), Garg, Vijay K. (committee member), Chase, Craig M. (committee member), Khurshid, Sarfraz (committee member), Mok, Aloysius K. (committee member).

Subjects/Keywords: Computer software; Verification; Static analysis; Shape analysis; Data structures; Deadlocks; Deadlock detection; Concurrency; Concurrent libraries; Multi-threaded; Wait-notify; Synchronization

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Deshmukh, J. V. (2010). Verification of sequential and concurrent libraries. (Doctoral Dissertation). University of Texas – Austin. Retrieved from http://hdl.handle.net/2152/ETD-UT-2010-08-1771

Chicago Manual of Style (16^th Edition):

Deshmukh, Jyotirmoy Vinay. “Verification of sequential and concurrent libraries.” 2010. Doctoral Dissertation, University of Texas – Austin. Accessed February 27, 2021. http://hdl.handle.net/2152/ETD-UT-2010-08-1771.

MLA Handbook (7^th Edition):

Deshmukh, Jyotirmoy Vinay. “Verification of sequential and concurrent libraries.” 2010. Web. 27 Feb 2021.

Vancouver:

Deshmukh JV. Verification of sequential and concurrent libraries. [Internet] [Doctoral dissertation]. University of Texas – Austin; 2010. [cited 2021 Feb 27]. Available from: http://hdl.handle.net/2152/ETD-UT-2010-08-1771.

Council of Science Editors:

Deshmukh JV. Verification of sequential and concurrent libraries. [Doctoral Dissertation]. University of Texas – Austin; 2010. Available from: http://hdl.handle.net/2152/ETD-UT-2010-08-1771

		in
And / Or
		in
And / Or
		in
And / Or
		in

Open Access Theses and Dissertations