The growing demand for high quality, safety, and security of software systems can only be met by rigorous application of formal methods during software design. Tools for formal methods in general, however, do not provide a sufficient level of automatic processing. This book methodically investigates the potential of first-order logic automated theorem provers for applications in software engineering.
Illustrated by complete case studies on verification of communication and security protocols and logic-based component reuse, the book characterizes proof tasks to allow an assessment of the prover's capabilities. Necessary techniques and extensions, e.g., for handling inductive and modal proof tasks, or for controlling the prover, are covered in detail.
The book demonstrates that state-of-the-art automated theorem provers are capable of automatically handling important tasks during the development of high-quality software and it provides many helpful techniques for increasing practical usability of automated theorem proving for successful applications.
Foreword by Prof. Don Loveland
Foreword to: Automated Theorem Proving in Software Engineering by Don Loveland
This book can mark the coming of age of automated theorem proving (ATP). The process to maturity has been a continuum, as it is for humans, but this book serves to mark the emergence of ATP into the marketplace. For this book is arguably the first to present for the general computer scientist or mathematician in some technical depth the ability of automated theorem provers to function in the realm where they will earn their living. That realm is as the reasoning engines of verifiers and generators of computer programs, hardware and related products. (We do note some excellent edited collections exist; one of the best is by Bibel and Schmitt, 1998: see this book's bibliography.) As we note below, this book does not simply document a brilliant but isolated undertaking. Rather, the book makes clear that a small but steady, and increasing, stream of real-world applications is now appearing.
The childhood and adolescence of ATP was both prolonged and spiked with brilliance. The birth year of the field should probably be set as 1956, when the Logic Theorist paper was published by Newell, Shaw and Simon. (However, most likely the first computer generated mathematical proof appeared in 1954 as output of a program for Pressburger arithmetic, written by Martin Davis. The work was not published at the time.) Thus the ATP field is at least 45 years old, well time for passage into the workplace of the world. Some superb accomplishments marked the period of adolescence, the Robbins algebra conjecture proof discovered by McCune's OTTER program and the sophisticated geometry provers of Chou et al. being perhaps most notable. (The discovery of a proof for the Robbins algebra conjecture closed a famous open problem.) But, despite the above and other accomplishments, it will never be possible to live up to the visions of the 1950s for the infant discipline of ATP. The first visions of the artificial intelligence (AI) world had ATP at the core of automated intelligence, for it seemed natural to assert that human reasoning could not be simulated without a central deductive engine of substantial power. Though many had moved away from this envisioned architecture by the late 1960s, the thesis got a shot in the arm from the work of Cordell Green who showed how proof could be converted to computation, and devised robot plans using a theorem prover. By 1970, however, the explosive cost of search through proof space was apparent to all users of automated provers. This lead to a clouded, if not dark, adolescence from which ATP is just now emerging.
Ever since the end of the early illusions of ATP and AI, the focus of opportunity has been the use of ATP in program and hardware verification. Much time and funds were invested in the 1970s and early 1980s in the attempt to bring general verifiers into practical use. This failed, although multiple developmental efforts continue with increasing success. Many people feel the future lies with semi-automated provers; that is, computer systems where the human and machine constantly interact. But in recent years a number of ATP groups have developed applications admittedly modest but with real-world workplace importance.
In fairness we must note that earlier points in time could have been se\-lec\-t\-ed as the ''coming of age''. The important AI programming language Prolog incorporates an automated theorem prover. Bob Boyer and J. Moore published a book in 1988 that documented their interactive theorem prover, which has been used to verify significant parts of commercial chips. But these and a few other accomplishments have been isolated accomplishments. The important difference is that now there is a flow of applications, however thin, that clearly will increase.
Both the ATP and the software engineering fields are fortunate to have a book such as prepared by Johann Schumann to document this coming of age. The ATP technology is presented in depth but with the software engineer as target. Careful analysis is given of the methodologies of ATP and related disciplines and what features are applicable to formal methods in software engineering. The case studies give excellent detail of current applications. Johann spent several years in industry prior to writing this treatise, and presently is engaged in just the type of software applications which he treats here. No one is better qualified to document this coming of age of ATP, and coming of a new age in software engineering. It is a pleasure to recommend this unique book to all interested in this corner of the future.
September 2000 Donald Loveland
, $Id: book.html,v 1.1 2003/01/22 18:10:13 schumann Exp $