Introduction

Our work¹ is under-pinned by the concept of a proof plan [1], an automated reasoning technique for representing the common structure which defines a family of proofs. The technique is used to automate the search for particular proofs and provides a ``high-level'' explanation of formal reasoning. Techniques for automating the search for proofs represent an essential enabling technology for formal methods of design in both software and hardware. Such methods complement the conventional approaches to establishing the correctness of computer systems. Correctness is an important concern given the ever increasing demand for dependable computer systems, in particular within the avionics and semiconductor (System-On-Chip) industries. Meeting this demand calls for automated reasoning techniques which can be integrated within the conventional design process. Below we summarise our contribution to achieving this goal.