Formal Method Sites

A number of other research laboratories in formal methods have made information available on the web. This page collects references to those I know about.

• It's not a WWW site, but it is useful: click here to get a Postscript document containing a (complete?) Z glossary, with definitions of symbols. It's taken from the Z Standard.

• The Laboratory for Applied Logic at Brigham Young Unviersity.

• The Laboratory for Applied Logic at the University of Idaho has a WWW page describing their research and activities.

• A Summary of New Results in Mathematics Obtained with Argonne's Automated Deduction Software An excellent WWW page of results in automated theorem proving by the folks who brought you Otter and MACE.

• The Irish Formal Methods Special Interest Group maintain a home page regarding their research.

• Bibliographies on Software Engineering and Formal Methods might contain valuable references for your research.

• SDCR Formal Methods Working Group contains some interesting reports and discussion papers on the future of formal methods and formal method research.

• Dick Botting's Home Page. It's not a purely formal methods page, to any degree, but it contains many good links, including links to numerous software engineering-related topics.

• ProofPower is a commercial tool, developed and marketed by ICL, supporting development and checking of specifications and formal proofs in Higher Order Logic and/or Z. Support for Z uses a deep(ish) embedding of Z into HOL, but includes syntax and type checking customised for Z. Information is available from WWW pages (still under transformation) or an email server. To use the email server send "help" to: ProofPower-server@win.icl.co.uk

• The Hardware Verification Group at the Institute of Computer Design and Fault Tolerance, University of Karlsruhe, Germany has a page describing their activities and research. They maintain a copy of the IFIP WG10.2 Hardware-Verification Benchmarks.

• Jonathan Bowen of the Oxford University Computing Laboratory has put together a page of information on the Z specification language.

• The Computational Logic Inc. home page provides pointers to information on
  • Nqthm, the theorem prover for the Boyer-Moore logic,
  • CLI Technical Reports,
  • current CLI research, and
  • a summary and slides from the Computational Logic 1994 Research Review.

• Tim Bull of Durham University maintains pages on The Maintainer's Assistant and The Bylands Project.

• Ruby is a notation and design discipline intended for the development of regular integrated circuits and similar hardware and software architectures. The intention is to formalise the design techniques already used by practising engineers, making it easier to document design decisions, to compare alternative designs, and to produce proof of the correctness of an implementation.

• Larry Paulson has written a page describing the Isabelle Theorem Prover.

• Andrew Butterfield has put together a WWW page about Formal Method group at Trinity College, Ireland. The major focus of this group seems to be VDM.

• Peter Gorm Larsen (peter@ifad.dk) maintains a page with pointers to information about VDM.

• NASA Langley Research Lab has a Formal Methods Program that is documented on the web. The major goals of NASA Langley's research program are to make formal methods practical for use on life-critical systems developed in the United States, and to orchestrate the transfer of this technology to industry through use of carefully designed demonstration projects.

• The Virtual Library has a page on formal methods and particularly on HOL maintained by Jonathan Bowen, (Jonathan.Bowen@comlab.ox.ac.uk). It is an excellent reference to formal methods and sites.

• The Information Technology Division of the Naval Research Laboratory has a page related to their work in high assurance computing systems.

• SRI International Computer Science Laboratory has a group doing research on Formal Methods and Dependable Systems.

• Kestrel Institute is a non-profit research institute focusing on formal and knowledge-based methods for incremental automation of the software process.

• INRIA has the following projects related to aspects of formal methods: COQ (software specifications and proofs), PROGRAIS (derivation of specifications and programs), and SAFIR (algebraic formal systems for industry and research).

• Oxford University has information on the ESPRIT ProCoS project and Working Group, the ESPRIT REDO project, and the UK IED safemos project.

• Larch is a multi-site project exploring methods, languages, and tools for the practical use of formal specifications.

• The Information Systems Workgroup at the University of Twente has a page describing the TM formal database specification language.

• Carolyn Talcott (clt@sail.stanford.edu) has a Database of Automated Reasoning Systems.