|
|
On Friday March 17th 2006, a Scottish Theorem Proving meeting will take place at Heriot-Watt University. The meeting will be hosted by the School of Mathematical and Computer Sciences and will take place in Room 2.33 on the 2nd floor of the Earl Mountbatten Building - building 3 on the Edinburgh Campus Map. If you wish advice on how to reach the Heriot-Watt campus by train, taxi, bus, car, bike, etc, then click here. For all organizational issues, please contact Andrew Ireland. In particular, if you wish a visitors' car park permit then please contact Andrew as soon as possible. A visitors' car park permit will allow you to park in the parking bays close to the Earl Mountbatten Building. Without a visitors' car park permit you will have to park in the vistors' car park (near the main entrance) or risk a nasty sticker being placed on a side window of your car.
Abstract
Symmetry reduction techniques were suggested over a decade ago as a means to ease the problem of model checking a system composed of many replicated components. Such replication often induces a great deal of symmetry on the state space modelling a system, and if a model checking algorithm can be adapted to search a single state from each equivalence class of symmetric states then significant savings in verification time and memory requirements may be obtained. Implementing symmetry reduction techniques in practice has proved surprisingly difficult, and over a decade since their proposal they are rarely included in popular model checkers. Those model checkers, e.g. Murphi, which do include symmetry reduction facilities can only handle a limited class of symmetries. The major problems which must be solved by any symmetry reduction method are a) how to detect symmetries of a model before search, and b) how to efficiently exploit a group of symmetries during search. In this talk we present TopSPIN, a symmetry reduction package for the SPIN model checker which performs automatic symmetry detection from the source code of a specification, and uses the computational group theory package GAP to choose an effective symmetry reduction strategy for an arbitrary group. We will give a high level overview of the techniques used by TopSPIN, and describe a study of real source code examples which we are using to assess the viability of our methods.
Abstract
We propose a bounded model checking procedure for programs manipulating dynamically allocated pointer structures. We express error conditions by formulae in the 2-variable fragment of Bernays-Schonfinkel class with equality and initial conditions by unary relations which are defined by monadic Datalog programs. We show that the extension of the 2-variable fragment of Bernays-Schoenfinkel class with fixpoints expressible by certain monadic Datalog programs is decidable. This decidability result allows for bounded model checking of infinite state transition systems.
Abstract
PIN blocks are 64-bit strings that encode a PIN ready for encryption and secure transmission in banking networks. PIN block attacks exploit feedback from error messages during PIN block manipulation operations, to allow an attacker to guess a PIN in far fewer operations than would be required by a brute-force attack. This talk will describe a framework for formal analysis of such attacks. Our analysis is probabilistic, and is automated using constraint logic programming and probabilistic model checking.
Abstract
Girard's Linear Logic and O'Hearn and Pym's Bunched Implications are
two important logics currently in circulation which mix additive and
multiplicative conjunction and implication.
Whereas linear logic `explains' additive implication using
multiplicative implication and a modality ! (bang), bunched
implications `explain' them as essentially independent but interleaved
sections of the logic.
To our knowledge no model (or logic) has managed to bridge this gap
and give a common account of what these logics are talking about.
In this talk we will present a very simple concrete model which we
believe interprets, in a relatively elementary and compositional way,
both bunched implications and linear logic.
The corresponding logic has one kind of implication (mixing both
additive and multiplicative parts), and three modalities.
Further details, including slides of the talk, can be found on my homepage.