Part I presents a selection of techniques that combine automated and interactive theorem proving paradigms. On the automated side, a novel, type theoretic connection between interactive theorem provers and external theorem provers is theoretically developed and implemented for the interactive theorem prover Agda. Also, Part~I evaluates the technique against the current state-of-the-art techniques for integrating interactive and automated theorem provers. The greatest betterment is that it is more feasible to be applied to industrial problems, than existing techniques. When exploring problem sets -- mathematical and industrial -- we obtained promising results.

Two cases studies of the integration have been carried out. These are SAT solving and CTL model-checking. Then CTL model-checking is refined to symbolic model-checking, and subsequently further refined into a customised logic for verifying programs that are definable by decidable Boolean valued transition functions.

The part concludes by exploring, and implementing a more traditional integration. This is where the external theorem prover provides a certificate that Agda checks to be correct, and then converts into a proof-object. A numerical comparison between these implementations is presented.

Part II discusses the railway domain and developing verified interlocking systems. This involves applying interactive theorem proving to prove a selection of signalling principles (lemmata from the railway domain) is sufficient to guarantee high-level safety requirements. This reduces the validation problem by narrowing the gap between the verified statement and the requirements. Then for a given (concrete) interlocking system programmed using ladder logic, it is shown how to determine using automated theorem proving whether it fulfils the required signalling principles. This results in a proof that the interlocking system fulfils the safety requirements. Following the proofs-as-programs paradigm, verified, executable programs are obtained, which we used for simulation purposes.

All work is carried out inside Agda; thus the obtained proofs are tractable. Agda also extracts the verified programs from the proofs. Working within a single tool increases the soundness assurances when compared to the alternative, where there are questions about the correctness of translations between the tools.

This framework has been successfully applied to two different systems: a digital interlocking and a mechanical interlocking.

Board Room

Department of Computer Science