Conclusions

Summary

Today’s automated theorem provers are restricted “more by general usability than by raw deductive power” ¹. In this book we have studied the application of automated theorem provers in the area of software engineering. Whenever formal methods (or formal methods tools) are used in a software development process, proof tasks arise which have to be processed by means of deduction, for example by an automated theorem prover.

Practical application of an automated theorem prover poses quite different requirements on the prover than traditional mathematical problems or benchmarks (e.g., the TPTP library [Sutcliffe et al.,1994]). In particular, a prover should be capable of solving (straightforward) inductive problems, handling sorted logic and logic with equality in an efficient way. An ATP must be able to process large formulas, a task which requires simplification and selection of axioms. When a proof can be found, the automated system should return a proof (possibly human-readable) or answer substitutions. Otherwise, at least trivial and obvious non-theorems should be recognized as such and additional feedback on what went wrong should be provided upon request. Because applications usually pose severe restrictions upon answer times and computing resources, the prover must be controlled in such a way that many problems can be solved within short run-times. Furthermore, prover-specific details of control need to be hidden from the user. Finally, a practical usable theorem prover must conform to strict software engineering criteria with respect to stability, robustness, clean interfaces, and documentation.

In this book we have investigated these requirements in detail. They are imposed by central characteristics of the application’s proof tasks to be solved. Typically, we can distinguish between proving in the large (many large proof tasks) or proving in the small, and deep or shallow proving. Deep proofs are long and have a complex structure, whereas shallow proofs only require few inference steps. Further important criteria concern the expected answer time (“results-while-u-wait” or batch operation), the source logic and its relation to first-order logic, and expected results.

We have demonstrated in this book that current technology automated theorem provers can be applied successfully in key-areas of software engineering. These areas include verification of protocols,analysis and verification of authentication protocols, and logic-based software reuse. Several successful case studies carried out by the author are presented in detail. These areas are top-of-the-line topics with respect to formal methods usage. Current trends in computing lead towards distributed computing and fast, yet reliable software development. The introduction of automated theorem proving in this area is a promising way to achieve security, safety and reliability of large software systems. The application of automated theorem provers will push forward the development of formal methods tools which show a higher degree of automated processing.

Our selection of case studies is aimed towards diversity of addressed topics. Whereas one case study required handling of formulas in a modal logic, others had to deal with inductive problems. The number of processed proof tasks strongly varied between the case studies (from about 15 to more than 14,000). Two of the case studies were carried out with respect to a formal methods tool: for software reuse, the theorem prover was integrated into the existing tool NORA/HAMMR. On the other hand, the tool PIL/SETHEO for protocol analysis was developed by the author within the case study. All case studies had in common that the proof tasks which had to be processed were non-trivial. The global aim was to elucidate requirements and meet these requirements with further development both of the ATP (control, handling of non-theorems, preselection of axioms) and of the ATP-embedded system interface (preprocessing, logical translation, human-readable proofs).

A generic system architecture and implementations of key-techniques leading to success have been described in this book. The main original contributions concern control of the prover for optimal performance by combination of search paradigms and parallel execution (SiCoTHEO*), and detection of non-theorems by generative methods and extended counterexample generation. Other key-techniques include translation of non first-order proof tasks and inductive proof tasks into first-order logic, simplification, handling of sorts, and postprocessing in order to generate answer substitutions and human-readable proofs. Furthermore, a variety of methods and practical solutions were developed to increase general usability of the automated prover within embedded systems.

In this book we have given a (as far as possible hands-on) methodology for approaching new applications of automated provers, opening up many possibilities for useful integration of automated theorem provers in formal methods tools. However, automated theorem provers for first-order logic cannot be used for each and every proof task — their deductive power is still too limited to handle real complex proof obligations (e.g., finding invariants). In order to push forward these limits, we will discuss the following important questions.