Rob Arthan

[RDA's Ugly Mug]
I work in what they call formal methods, i.e., the use of rigorous mathematical methods in computer systems engineering. I am particularly interested in mechanized theorem-proving. I also get involved in developing secure systems and doing R&D in computer security and various other things.

For a little over 11 years, I worked for ICL (now part of the Fujitsu Group); the ProofPower web site will tell you a lot more about the work that was done there in the development of tools to support formal methods, particularly specification and proof in HOL and Z. There are several papers on the web site.

These tools were originally conceived for use in the certification of high assurance secure systems, but are now mainly used for specifying and verifying safety critical systems. I am now an independent consultant in this area - still working closely with my former colleagues from ICL. My company Lemma 1 has some WWW pages you might like to visit.

I also have a strong interest in using mechanized proof tools to formalise pure mathematics. There is a light-hearted report on one aspect of progress in this area, where you can also find useful links to the available systems.

For my sins, I was a member of the panel that produced the ISO standard Z notation I have a personal collection of papers concerned with the Z standard.

E-mail address

[rda at lemma-one dot com]

Note

This page is best viewed using a Web Browser. Although if you really have nothing better to do, the HTTP RFC will tell you what you need to know to get it with telnet!

Last Update: $Date: 2015/09/23 11:01:03 $.