The Laboratory for Applied Logic at Brigham Young University.
TheLaboratory for Applied Logic at University of Idahohas 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.
TheBibliographies 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 fromWWW 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
Rubyis 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 Paulsonhas written a page describing the Isabelle Theorem Prover
SDCR Formal Methods Working Group
Andrew Butterfieldhas 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 toinformation about VDM
NASA Langley Research Lab has a Virtual Library 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 onHOLmaintained 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 inhigh assurance computing systems
SRI International has a group doing research onFormal Methods and Dependable Systems
Kestrel Instituteis 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), andSAFIR(algebraic formal systems for industry and research).
Oxford University has information on the ESPRIT ProCoSproject and Working Group, the ESPRIT REDOproject, and the UK IED safemos project.
Larch is a multi-site project exploring methods, languages, and tools for the practical use of formal specifications.
Carolyn Talcott (clt@sail.stanford.edu) has a Database of Automated Reasoning Systems.