Thesis (Ph. D.)--University of Washington, 2006. / Vita. Includes bibliographical references (p. 129-140).

Our work focuses on bringing the first-order reasoning closer to practicalapplications, particularly in software and hardware verification. The aim is to develop techniques that make first-order reasoners more scalablefor large problems and suitable for the applications. In pursuit of this goal the work focuses in three main directions. First, wedevelop an algorithm for an efficient pre-selection of axioms. This algorithmis already being widely used by the community and enables off-the-shelf theoremprovers to work with problems having millions of axioms that would otherwisebe overwhelming for them. Secondly, we focus on the saturation algorithm itself, and develop anew calculus for separate handling of propositional predicates. We also do anextensive research on various ways of clause splitting within the saturationalgorithm. The third main block of our work is focused on the use of saturation basedfirst-order theorem provers for software verification, particularly forgenerating invariants and computing interpolants. We base our work on theoretical results of Kovacs and Voronkov published in2009 on the CADE and FASE conferences. We develop a practical implementationwhich embraces all the extensions of the basic resolution and superposition calculus that are contained in the theorem prover Vampire. We have also developed a unique proof transforming algorithm which optimizes the computed interpolantswith respect to a user specified cost function.

The discovery of unknown lemmas, case-splits and other so called eureka steps are challenging problems for automated theorem proving and have generally been assumed to require user intervention. This thesis is mainly concerned with the automated discovery of inductive lemmas. We have explored two approaches based on failure recovery and theory formation, with the aim of improving automation of firstand higher-order inductive proofs in the IsaPlanner system. We have implemented a lemma speculation critic which attempts to find a missing lemma using information from a failed proof-attempt. However, we found few proofs for which this critic was applicable and successful. We have also developed a program for inductive theory formation, which we call IsaCoSy. IsaCoSy was evaluated on different inductive theories about natural numbers, lists and binary trees, and found to successfully produce many relevant theorems and lemmas. Using a background theory produced by IsaCoSy, it was possible for IsaPlanner to automatically prove more new theorems than with lemma speculation. In addition to the lemma discovery techniques, we also implemented an automated technique for case-analysis. This allows IsaPlanner to deal with proofs involving conditionals, expressed as if- or case-statements.

In this thesis we describe an approach to automatically invent/explore new mathematical theories, with the goal of producing results comparable to those produced by humans, as represented, for example, in the libraries of the Isabelle proof assistant. Our approach is based on ‘schemes’, which are formulae in higher-order logic. We show that it is possible to automate the instantiation process of schemes to generate conjectures and definitions. We also show how the new definitions and the lemmata discovered during the exploration of a theory can be used, not only to help with the proof obligations during the exploration, but also to reduce redundancies inherent in most theory-formation systems. We exploit associative-commutative (AC) operators using ordered rewriting to avoid AC variations of the same instantiation. We implemented our ideas in an automated tool, called IsaScheme, which employs Knuth-Bendix completion and recent automatic inductive proof tools. We have evaluated our system in a theory of natural numbers and a theory of lists.

Modern computer systems are advancing from multi-core to many-core designs and System-on-chips (SoC) are becoming increasingly complex while integrating a great variety of components, thus constituting complex distributed systems. Such architectures rely on extremely complex communication protocols to exchange data with required performance. Arguing formally about the correctness of communication is an acknowledged verification challenge. This thesis presents a generic framework that formalises the idea of incremental modelling and step-wise verification to tackle this challenge: to control the overall complexity, features are added incrementally to a simple initial model and the complexity of each feature is encapsulated into an independent modelling step. Two main strategies reduce the verification effort. First, models are constructed with verification support in mind and the verification process is spread over the modelling process. Second, generic correctness results for framework components allow the verification to be reduced to discharging local assumptions when a component is instantiated. Models in the framework are based on abstract state machines formalised in higher order logic using the Isabelle theorem prover. Two case studies show the utility and breadth of the approach: the ARM AMBA Advanced High-performance Bus protocol, an arbiter-based master-slave bus protocol, represents the family of SoC protocols; the PCI Express protocol, an off-chip point-to-point protocol, illustrates the application of the framework to sophisticated, performance-related features of current and future on-chip protocols. The presented methodology provides an alternative to the traditional monolithic and post-hoc verification approach.

The role of representation in reasoning has been long and widely regarded as crucial. It has remained one of the fundamental considerations in the design of information-processing systems and, in particular, for computer systems that reason. However, the process of change and choice of representation has struggled to achieve a status as a task for the systems themselves. Instead, it has mostly remained a responsibility for the human designers and programmers. Many mathematical problems have the characteristic of being easy to solve only after a unique choice of representation has been made. In this thesis we examine two classes of problems in discrete mathematics which follow this pattern, in the light of automated and interactive mechanical theorem provers. We present a general notion of structural transformation, which accounts for the changes of representation seen in such problems, and link this notion to the existing Transfer mechanism in the interactive theorem prover Isabelle/HOL. We present our mechanisation in Isabelle/HOL of some specific transformations identified as key in the solutions of the aforementioned mathematical problems. Furthermore, we present some tools that we developed to extend the functionalities of the Transfer mechanism, designed with the specific purpose of searching efficiently the space of representations using our set of transformations. We describe some experiments that we carried out using these tools, and analyse these results in terms of how close the tools lead us to a solution, and how desirable these solutions are. The thorough qualitative analysis we present in this thesis reveals some promise as well as some challenges for the far-reaching problem of representation in reasoning, and the automation of the processes of change and choice of representation.

In this thesis we propose a formal framework for specifying and validating properties of software system architectures. The framework is founded on a model of software architecture description languages (ADLs) and uses a theorem-proving based approach to formally and mechanically establish properties of architectures. Our approach allows models defined using existing ADLs to be validated against properties that may not be expressible using the original notation and tool-set. The central component of the framework is a conceptual model of architecture description languages. The model formalizes a salient, shared set of design categories, relationships and constraints that are fundamental to these notations. An advantage of an approach based on a conceptual model is that it provides a uniform view of design information across a selection of languages. This allows us to construct alternate formal representations of design information specified using existing ADLs. These representations can then be mechanically validated to ensure they meet their specific formal requirements. After defining the model we embed it in the logic of the PVS theorem-proving environment and illustrate its utility with a case study. We first demonstrate how the elements of a design are specified using the model, and then show how this representation is validated using machine-assisted proof. Our approach allows the correctness of a design to be established against a wide range of properties. We illustrate with structural properties, behavioural properties, relationships between the structural and behavioural specification, and dynamic, or evolving aspects of a system's topology.

In this thesis we propose a formal framework for specifying and validating properties of software system architectures. The framework is founded on a model of software architecture description languages (ADLs) and uses a theorem-proving based approach to formally and mechanically establish properties of architectures. Our approach allows models defined using existing ADLs to be validated against properties that may not be expressible using the original notation and tool-set. The central component of the framework is a conceptual model of architecture description languages. The model formalizes a salient, shared set of design categories, relationships and constraints that are fundamental to these notations. An advantage of an approach based on a conceptual model is that it provides a uniform view of design information across a selection of languages. This allows us to construct alternate formal representations of design information specified using existing ADLs. These representations can then be mechanically validated to ensure they meet their specific formal requirements. After defining the model we embed it in the logic of the PVS theorem-proving environment and illustrate its utility with a case study. We first demonstrate how the elements of a design are specified using the model, and then show how this representation is validated using machine-assisted proof. Our approach allows the correctness of a design to be established against a wide range of properties. We illustrate with structural properties, behavioural properties, relationships between the structural and behavioural specification, and dynamic, or evolving aspects of a system's topology.

Thesis (Ph. D.)--University of Texas at Austin, 1999. / Vita. Includes bibliographical references (leaves 195-204). Available also in a digital version from Dissertation Abstracts.

Thesis (M.S.)--Worcester Polytechnic Institute. / Keywords: theorem proving; modular verification; software verification; feature-oriented programming; feature interaction. Includes bibliographical references (p. 131-136).