Friday January 31st 2014, 1:30pm - 5:00pm

Room 1.33b, School of Computer Science, University of St Andrews, KY16 9SX (map, directions)

1:30pm | Jonathan Heras | University of Dundee | Proof-Pattern Recognition and Lemma Discovery in ACL2 |

2:15pm | Brian Campbell | University of Edinburgh | Randomised testing of a HOL 4 microprocessor model |

3:00pm | Break | ||

3:30pm | Daniel Raggi | University of Edinburgh | Re-...-re-representation |

4:15pm | Steven Obua | University of Edinburgh | ProofPeer: Collaborative Theorem Proving |

5:00pm | Pub and dinner |

ACL2 is a theorem prover that has features of both Interactive Theorem Provers and Automatic Theorem Provers: it will try to prove given conjectures automatically, but strongly relies on the user having supplied the auxiliary lemmas required for rewriting. In this talk, we present a novel technique for combining statistical machine learning for proof-pattern recognition with symbolic methods for lemma discovery applied in ACL2. The resulting tool, ACL2(ml), gathers proof statistics and uses statistical pattern-recognition to pre-processes data from libraries, and then suggests auxiliary lemmas in new proofs by analogy with already seen examples. We will present the implementation of ACL2(ml) alongside theoretical descriptions of the proof-pattern recognition and lemma discovery methods involved in it.

We consider validating a HOL 4 model of the ARM Cortex-M0 microcontroller core by testing the model's behaviour on a randomly chosen instructions against a real chip.

The model and our intended application involve precise timing information about instruction execution, but the implementations are pipelined, so checking the behaviour of single instructions will not give us sufficient confidence in the model. Thus we test randomly chosen sequences of instructions at once.

This produces some interesting constraints on the initial and intermediate execution states: we must ensure that memory accesses are in range and that we respect restrictions on the instructions. I will talk about the relevant features of the model, how we synthesise tests, how we approach solving the constraints using an SMT solver, and what has happened in practice so far.

My main interest is the role of representation in reasoning. In this talk I'll present my work on formalising transformations (in Isabelle/HOL) and automating a method of reasoning in which the representation of the problem in question is transformed in the attempt to solve it. In the paradigm I'm working, any mapping between the types of a domain can be the basis for a transformation, provided that we can find sufficient matches between the functions and relations of the types of both domains, and that these matches respect the original mapping. For example, if we take the mapping that associates every list with the set of its elements, we can match the function 'append' of lists to 'union' of sets. Realising matches between domains establishes interesting logical relations between them (e.g., we can transform some problems about sets into problems about lists). I have identified and formalised a number of common transformations particularly useful in discrete mathematics. Some proofs using these have been fully formalised in an interactive manner. The next step is to do some experiments in which the transformations are incorporated in the automatic search of a proof.

ProofPeer is an EPSRC funded 3-year project which will start in March. Its topic is to research the foundations of what we call "Collaborative Theorem Proving". I’ll first outline the goals of this project (details about it can also be found at www.proofpeer.net), and then discuss the design considerations for ProofScript, which is the language we will create for interfacing between the proof peers and the ProofPeer system.

General information about STP is available from the STP page. For information about the event, please contact the organiser:

- Edwin Brady (ecb10@st-andrews.ac.uk)