Browsing by Subject "Computer programs--Verification"
Now showing items 1-9 of 9
-
Efficient and effective symbolic model checking
(2006)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, ... -
Formal verification of computer controlled systems
(2007-05)This dissertation discusses the application of formal verification methods to reasoning about the correctness of computer controlled systems. Due to the switching that is introduced by the computer controller, the ... -
Generalization, lemma generation, and induction in ACL2
(2008-05)Formal verification is becoming a critical tool for designing software and hardware today. Rising complexity, along with software's pervasiveness in the global economy have meant that errors are becoming more difficult to ... -
Model checking: beyond the finite
(2004) -
Specification and analysis of timing properties in real-time systems
(1988)This dissertation proposes a formalism for the specification and verification of timing properties of real-time systems. Reasoning about properties of a real-time system requires one to consider both relative and absolute ... -
Symbolic model checking techniques for BDD-based planning in distributed environments
(2002-05)Effective plan specification, solution extraction and plan execution are critical to the ability of single- and multi-agent systems to operate given the dynamism and uncertainties that exist in real-world domains. While ... -
Techniques for formal verification of concurrent and distributed program traces
(2004)Traditional approaches for eliminating errors in concurrent and distributed programs include formal methods and testing. This dissertation presents an approach toward combining formal methods and testing, while avoiding ... -
Three essays on the interface of computer science, economics and information systems
(2007)This thesis looks at three aspects related to the design of E-commerce systems, online auctions and distributed grid computing systems. We show how formal verification techniques from computer science can be applied to ... -
Using theorem proving and algorithmic decision procedures for large-scale system verification
(2005)The goal of formal verification is to use mathematical methods to prove that a computing system meets its specifications. When applicable, it provides a higher assurance than simulation and testing in correct system ...
