Symmetry in CNFs
Jim Moloney
Department of Artificial Intelligence
The University of Edinburgh
Apathy and Successful Leadership
in the Tree Identify Protocol of the Firewire.
Carron Shankland
Department of Mathematics and Computing
The University of Stirling
We present an abstract model of computer memory, in the form of directed, labelled graphs with simple transitions corresponding to valid memory operations. We also introduce a refinement of this basic model of memory that incorporates features of memory management. After giving some examples of how this refined model captures various garbage collection algorithms, we discuss a proof under development that the two representations are behaviorally equivalent.
This will be an informal presentation of proofs that are being carried out in the theorem prover Coq.
The talk is an overview of work in progress on memory management by the LEGO project, including John Longley, Rod Burstall, Paul Jackson and me, together with Richard Brooksby and David Jones at Harlequin Ltd.
Jim Molony: Symmetry in CNFs
The existence of symmetry in propositional formulas can lead to improvements in satisfiability checking efficiency. Research in this area appears from time to time in the automated reasoning literature. The treatments given for the symmetry side of things are generally minimal in respect of the particular implementations and are never very illuminating. There seems to be a lot of mathematical structure behind the idea of groups acting on conjunctive normal form equations (CNFs) which has not been adequately explored. I will present a framework for reasoning about symmetries in CNFs and show how results from group theory suggest a number of interesting conjectures about the relationships between various flavours of stabilisers and orderings on the formulas. At the moment this research has an empirical, exploratory nature. I will summarise the state of these investigations.
Carron Shankland: Apathy and Successful Leadership in the Tree Identify Protocol of the Firewire.
In formal methods we are always searching for new and interesting examples to which we can apply our techniques. In this talk I will introduce a case study based on the Philips "firewire". (More specifically, the tree identify protocol of a high performance serial multimedia bus (IEEE standard 1394)). The description, given using muCRL, is made in varying levels of detail and I show, using the cones and foci technique of Groote and Springintveldt that these different descriptions are all equivalent under branching bisimulation. I'll also talk about the techniques used, and make some observations about properties of the protocol.
| Return to Scottish Theorem Proving page. |