Scottish Theorem Proving

Friday 22nd October 2004, 2.00pm - 5.00pm

Room 4.03, Appleton Tower, University of Edinburgh

This meeting of the Scottish Theorem Proving seminar has been organised by Graham Steel. Please contact Graham Steel for further details or clarification.

Travel information, maps etc. can be found here.

More information about Scottish Theorem Proving can be found here.


1.00pm - 2.00pm: Lunch (optional).

Meet in Appleton Tower, Level 3 coffee room. Bring your own sandwiches; tea and coffee will be provided.

2.00pm - 2.40pm: Hardware Security Module APIs

Graham Steel


A hardware security module, or HSM, is a tamper-proof piece of computer hardware used to carry out a small set of cryptographic operations. HSMs are used in various security-critical applications such as banking systems, electronic payment devices and cash machines (ATMs). Typically, such devices have a restricted application program interface (API) that prescribes how an application program can make requests of the module to carry out commands. Various attacks have been found on these APIs in recent times by a combination of 'by-hand' analysis and ad-hoc formal methods. We are just starting work on a project to develop more generic formal tools for analysing these APIs. This talk will introduce APIs, give some examples of attacks, and some ideas we have about how their analysis might be formalised.

2.40pm - 3.20pm: Model Checking Hw-Hume

Gudmund Grov


High integrity software systems call for various levels of static analysis. Hume is a functional programming language, targeted at safety-critical systems, which supports static analysis for time and space. However, formal verification is not part of the current Hume static analysis tool set. This gap is addressed by exploring the use of Hume with an off-the-shelf design verification system called Spin. The rules for translating a subset of Hume into the notation required by Spin are investigated. An empirical analysis targeted at the translation and verification of the translated programs is conducted.

3.20pm - 3.40pm: Coffee Break

3.40pm - 4.20pm: Generating and Identifying Mathematical Theorems: Separating the Wheat from the Chaff

Roy McCasland


There are several automated systems capable of generating, in certain mathematical domains, thousands upon thousands of true statements -- "theorems", from a logical point of view. However, most likely, only a small handful of these statements would be considered "theorems", from a mathematical point of view. We describe our approach, from a work in progress, to distinguish between those true statements which mathematicians would deem worthy of the name "Theorem", and those which they would not. We also present a brief demonstration of the system we are developing, which implements this approach.

4.20pm - 5.00pm: Demos

Sean Wilson, Lucas Dixon, and others to be confirmed.

5.00pm (approx) End

Move to bar "Centraal", West Nicholson Street.