Although a wide variety of powerful theorem provers have emerged from the academic theorem proving community, and an increasing interest in proof in the software development community, take up of prover technology has been disappointing. One idea is that proof tools need to be introduced as a ``Trojan Horse'' into existing CASE tools in order to be accepted. A barrier to this could be the need to understand failing proofs in order for a proof tool to be at all useful. We examine a subset of interesting problems from the point of view of potential end-users, and describe a methodology using existing theorem provers which could be harnessed to solve such problems.

Over the last decade, symmetry reduction techniques have been shown to be successful in combating the state space explosion problem in model checking. Such reduction techniques usually assume that symmetries of a concurrent system are known in advance, and these symmetries are exploited when model checking the original system description. Two obvious questions are a) "can we automatically detect symmetries of a concurrent system from its textual description?", and b) "would it be possible to apply symmetry reduction directly to the textual description of a system so that a reduced textual description could be model checked in the usual way?". In my talk I will describe some preliminary work in attempting to answer these questions.

We present an account of rippling with proof critics suitable for use in higher order logic in Isabelle/IsaPlanner. We treat issues not previously examined, in particular regarding the existence of multiple annotations during rippling. This results in an efficient mechanism for rippling that can conjecture and prove needed lemmas automatically, and then present the resulting proof plans as Isar style proof scripts.

STPS homepage