http:^^www.cs.utexas.edu^users^boyer^courses^backup-formal-methods.html

This data set contains WWW-pages collected from computer science departments of various universities

Prover</A>).  See also DEC SRC's <A
HREF=http://www.research.digital.com/SRC/larch/larch-home.html> Larch
Home Page</A> and the <A
HREF=http://www.cs.cmu.edu/afs/cs.cmu.edu/project/larch/www/home.html>
Larch Project</A> at <A
HREF=http://www.cs.cmu.edu/Web/FrontDoor.html> CMU</A>.  The <A
HREF=ftp://larch.lcs.mit.edu/pub/Larch> Larch tool set</A> (look at the
<A HREF=ftp://larch.lcs.mit.edu/pub/Larch/README> <TT>README</TT></A>
file first) is available.

<P><LI>
<A NAME=LEANTAP
 HREF=http://emmy.ira.uka.de/~posegga/leantap/leantap.html>
LeanTaP</A>, a tableau-based deduction theorem prover for classical
first-order logic.

<P><LI>
<A NAME=LEGO HREF=http://www.dcs.ed.ac.uk/packages/lego/>
LEGO</A> proof-checker.

<P><LI><!16 Feb 95>
<iMG ALT="*" SRC="http://www.w3.org/hypertext/WWW/Icons/WWW/star11t.gif" HEIGHT=11 WIDTH=11>
<A NAME=LOTOS HREF=http://wwwtios.cs.utwente.nl/lotos/>
LOTOS</A> (Language of Temporal Ordering Specifications).
See also
<!12 Sep 95>
<A HREF=http://www.dit.upm.es/~lotos/>
here</A>.

<P><LI><!30 Jan 95>
<A NAME=MA HREF=http://www.dur.ac.uk/~dcs1tmb/MA/home-page.html>
Maintainer's Assistant</A>,
a tool for reverse engineering and re-engineering code using
formal methods.

<P><LI><!1 Feb 95>
<A NAME=MEIJE HREF=http://www.inria.fr/meije/meijetools.html>
Meije</A> tools for the verification of concurrent programs.
Includes ATG</A>, a graphical editor/visualizer.

<P><LI>
<A NAME=MIZAR HREF=http://web.cs.ualberta.ca/~piotr/Mizar/>
Mizar</A> tool, a long-term effort aimed at developing
software to support a working mathematician in preparing
papers.

<P><LI><!5 Dec 95>
<iMG ALT="!" SRC="http://www.w3.org/hypertext/WWW/Icons/WWW/new.gif" HEIGHT=11 WIDTH=5>
<iMG ALT="*" SRC="http://www.w3.org/hypertext/WWW/Icons/WWW/star11t.gif" HEIGHT=11 WIDTH=11>
<A HREF=http://www.cs.cmu.edu/~modelcheck/>
Model Checking</A> at CMU, a method for formally verifying
finite-state concurrent systems. 

<P><LI>
<A NAME=MURAL HREF=http://www.cs.man.ac.uk/fmethods/projects/mural.html>
Mural</A> tool to aid formal reasoning about
specifications including a proof assistant and <A
HREF=#VDM>VDM</A> support.
See also the <A
HREF=http://web.inf.rl.ac.uk/proj/mural.html>
Mural Project</A>.

<P><LI><!12 Oct 95>
<A NAME=MURPHI HREF=ftp://snooze.stanford.edu/pub/murphi/>
Murphi</A>, a finite-state verification tool for concurrent systems.
See also
<A HREF=ftp://snooze.stanford.edu/pub/papers/verification/>
on-line papers</A>.

<P><LI>
<iMG ALT="*" SRC="http://www.w3.org/hypertext/WWW/Icons/WWW/star11t.gif" HEIGHT=11 WIDTH=11>
<A NAME=NQTHM HREF=http://www.cli.com/software/nqthm/>
Nqthm</A> theorem prover and the <A
HREF=http://www.cli.com/software/pc-nqthm/>
Pc-Nqthm</A> interactive ``Proof-checker'' enhancement
of the <A HREF=#BM> Boyer-Moore Theorem Prover</A>
from <A HREF=http://www.cli.com/>Computational Logic Inc.</A>
See also
<!A HREF=gopher://sun12.tfh-berlin.de/11/Labore/ST-Lab/nqthm>
<A HREF=gopher://gopher.tfh-berlin.de/11/Labore/ST-Lab/nqthm>
Nqthm users Gopher information</A>.

<P><LI>
<iMG ALT="*" SRC="http://www.w3.org/hypertext/WWW/Icons/WWW/star11t.gif" HEIGHT=11 WIDTH=11>
<A NAME=NUPRL
HREF=http://www.cs.cornell.edu/Info/Projects/NuPrl/nuprl.html>
Nuprl</A> tool based on intuitionistic type theory.

<P><LI>
<A NAME=OBJ HREF=/archive/obj.html>
OBJ</A> - OBJ3 and 2OBJ.

<P><LI><!18 Feb 95>
<A HREF=http://www.mcs.anl.gov/home/mccune/ar/otter/>
Otter</A>, an automated deduction system.

<P><LI><!11 Apr 95>
<iMG ALT="*" SRC="http://www.w3.org/hypertext/WWW/Icons/WWW/star11t.gif" HEIGHT=11 WIDTH=11>
<A NAME=PETRI-NETS HREF=http://www.daimi.aau.dk/~petrinet/>
Petri Nets</A>, a formal graphical notation
for modelling systems with concurrency.
See also
<!19 Oct 95>
<A HREF=http://www.iao.fhg.de/Library/conferences/index/Petri_Nets.html>
conferences</A>.

<P><LI>
<A NAME=PI-CALCULUS>
Pi-calculus. (Also <A NAME=CCS>
CCS - Calculus of Communicating Systems.)
See
<!A HREF=http://www.dcs.ed.ac.uk/staff/rm>
<A HREF=ftp://ftp.cl.cam.ac.uk/users/rm135/>
papers by Robin Milner <EM>et al.</EM></A>
<!6 Jan 95>
the <A HREF=ftp://ftp.docs.uu.se/pub/mwb/>
Mobility Workbench</A>
(see <A HREF=ftp://ftp.docs.uu.se/pub/mwb/README>
<TT>README</TT></A> file)
and a <A HREF=ftp://ftp.docs.uu.se/pub/mwb/pi.bib>
BibTeX bibliography</A>.

<P><LI>
<iMG ALT="*" SRC="http://www.w3.org/hypertext/WWW/Icons/WWW/star11t.gif" HEIGHT=11 WIDTH=11>
<A NAME=PROOFPOWER
HREF=http://www.to.icl.fi/ICLE/ProofPower/>
ProofPower</A> is a commercial tool, developed and marketed by ICL,
supporting development and checking of specifications and formal proofs
in <A HREF=#HOL> Higher Order Logic</A> and/or <A HREF=#Z> Z</A>.
Support for Z uses a deep(ish) embedding of Z into HOL, but includes
syntax and type checking customized for Z.

<P><LI>
<iMG ALT="*" SRC="http://www.w3.org/hypertext/WWW/Icons/WWW/star11t.gif" HEIGHT=11 WIDTH=11>
<A NAME=PVS HREF=http://www.csl.sri.com/sri-csl-pvs.html>
PVS</A> (Prototype Verification System) tool based on classical typed
higher-order logic developed at the <A HREF=http://www.ai.sri.com/>
SRI</A> International <A HREF=http://www.csl.sri.com/> Computer Science
Laboratory</A>.

<P><LI><!19 Jan 95>
<iMG ALT="*" SRC="http://www.w3.org/hypertext/WWW/Icons/WWW/star11t.gif" HEIGHT=11 WIDTH=11>
<A NAME=RAISE HREF=http://dream.dai.ed.ac.uk/raise/>
RAISE</A> language and tools from CRI, Denmark.
Email <A HREF=mailto:[e-mail]>.
<EM>[e-mail]</EM></A>.

<P><LI>
<A NAME=REFINEMENT HREF=http://www.abo.fi/~mbutler/pmg/theory-backg.html>
Refinement Calculus</A> by Ralph Back <EM>et al.</EM>.

<P><LI>
<iMG ALT="*" SRC="http://www.w3.org/hypertext/WWW/Icons/WWW/star11t.gif" HEIGHT=11 WIDTH=11>
<A NAME=SDL HREF=http://www.tdr.dk/public/SDL/>
SDL</A> Specification and Description Language.

<P><LI><!12 Oct 95>
<A NAME=SMV HREF=ftp://emc.cs.cmu.edu/pub/>
SMV</A> (Symbolic Model Verifier) model checker for finite-state
systems, using the specification language CTL (Computation Tree Logic),
a propositional branching-time temporal logic.
See also <A HREF=ftp://emc.cs.cmu.edu/pub/csml.tar.Z>
CSML and MCB</A>, a language for compositional
description of
finite state machines and a (non-symbolic) model checker for CTL,
a <A HREF=ftp://emc.cs.cmu.edu/pub/bdd/>
BDD library with extensions for sequential verification, and
<A HREF=ftp://emc.cs.cmu.edu/pub/bdd/>
papers</A> on various related topics.

<P><LI> <A NAME=SPIN
HREF=ftp://netlib.att.com/netlib/att/cs/home/holzmann-spin.html>
SPIN</A> is an automated verification tool (model checker), using a
language based on <A HREF=#CSP>CSP</A>, for finite state systems, such
as protocols or validation models of distributed systems, developed at
AT&amp;T Bell Labs.

<P><LI>
<A NAME=STEP HREF=http://theory.stanford.edu/people/zm/step.html>
STeP</A>, the  Stanford Temporal Prover.

<P><LI> <A NAME=TAM
HREF=http://dcpu1.cs.york.ac.uk:6666/real-time/tam.html>
TAM</A>. The <EM>Temporal Agent Model</EM> from
the <A HREF=http://dcpu1.cs.york.ac.uk:6666/real-time/>
Real-Time Systems Research Group</A> at York University.

<P><LI>
<iMG ALT="*" SRC="http://www.w3.org/hypertext/WWW/Icons/WWW/star11t.gif" HEIGHT=11 WIDTH=11>
<A NAME=TLA
HREF=http://www.research.digital.com/SRC/personal/Leslie_Lamport/tla/tla.html>
TLA</A> (Temporal Logic of Actions) has <A
HREF=http://ls4-www.informatik.uni-dortmund.de/RVS/P-TLA/welcome.html>
tool</A> support.

<P><LI><!19 Jan 95>
<A NAME=TPS
HREF=http://www.cs.cmu.edu/afs/cs.cmu.edu/user/andrews/www/tps.html>
<!http://www.cs.cmu.edu/afs/cs.cmu.edu/user/andrews/www/tps.html>
TPS and ETPS</A>, the Theorem Proving System and the Educational
Theorem Proving System.

<P><LI>
<A NAME=TTM/RTTL HREF=http://www.cs.yorku.ca/People/Jonathan.Ostroff/ttm.rttl.html>
TTM/RTTL</A> framework for real-time reactive systems.

<P><LI><!22 Nov 94>
<A NAME=UNITY HREF=http://www.cs.utexas.edu/users/psp/welcome.html#unitysec>
UNITY</A>, a programming notation and a logic to reason about
parallel and distributed programs.

<P><LI>
<iMG ALT="*" SRC="http://www.w3.org/hypertext/WWW/Icons/WWW/star11t.gif" HEIGHT=11 WIDTH=11>
<A NAME=VDM HREF=http://www.ifad.dk/vdm/vdm.html> VDM</A>
(Vienna Development Method).  See also
the <A HREF=#MURAL>Mural</A> tool, and VDM <A
HREF=http://www.cs.man.ac.uk/fmethods/refs/vdm-text-books.html> text
books</A>.

<P><LI>
<iMG ALT="*" SRC="http://www.w3.org/hypertext/WWW/Icons/WWW/star11t.gif" HEIGHT=11 WIDTH=11>
<A NAME=Z HREF=/archive/z.html>
Z notation</A> for formal specification.

</UL>

See also:

<UL>

<LI>
<A HREF=ftp://chopwell.ncl.ac.uk/pub/fm_tools/fm_tools_db>
Formal Methods Tools Database</A>
(<A HREF=ftp://ecs.soton.ac.uk/pub/misc/fm_tools_db>second sourced</A>)
maintained by Tim Denvir.
<P>

Request for information for a
<A HREF=gopher://nisp.ncl.ac.uk/11/lists-u-z/vdm-forum/files/fm-appl-db-form.txt>
Formal Methods Applications Database</A> by Nico Plat (November 1994).
<P>

<LI><!6 Apr 95>
<A HREF=/archive/formal-methods/wift95.html>
Tools demonstration information</A>
for <A NAME=WIFT HREF=http://www.cse.fau.edu/WIFT/>
WIFT95</A> workshop.
<P>

</UL>


<H2><A NAME=news>Newsgroups</A></H2>

<UL>

<P><LI>
<A HREF=news:comp.specification><EM>
Comp.specification</EM></A> including discussion of formal
specification and methods.
See also the newer
<!12 Jul 95>
<A HREF=news:comp.specification.misc><EM>comp.specification.misc</EM></A>
newsgroup and other
<A HREF=news:comp.specification.*>
related newsgroups</A>:

<UL>

<P><LI>
<!12 Jul 95>
<A HREF=news:comp.specification.larch><EM>
Comp.specification.larch</EM></A> - more specific discussion on the
<A HREF=#LARCH> Larch</A>.

<P><LI>
<A HREF=news:comp.specification.z><EM>
Comp.specification.z</EM></A> - more specific discussion on the
<A HREF=/archive/z.html> Z and related notations</A>.
Messages are <A HREF=ftp://ftp.comlab.ox.ac.uk/pub/Zforum> archived</A>
(e.g., see <A HREF=ftp://ftp.comlab.ox.ac.uk/pub/Zforum/zforum>
most recent messages</A>).
See also <A
HREF=http://www.cis.ohio-state.edu/hypertext/faq/usenet/z-faq/faq.html>
FAQ message</A> (Frequently Asked Questions).

</UL>

<P><LI>
<A HREF=news:comp.software-eng><EM> Comp.software-eng</EM></A> -
more general discussion on software engineering, including formal
aspects.  Messages relating to <A
HREF=http://dxsting.cern.ch/sting/comp.software-eng/safety.txt> formal
methods and software safety</A> in this newsgroup have been <A
HREF=http://dxsting.cern.ch/sting/comp.software-eng/Index.html>
archived</A>. See also the
<!A HREF=ftp://ftp.qucis.queensu.ca/pub/software-eng>
<A HREF=http://www.qucis.queensu.ca:1999/Software-Engineering/>
<EM>comp.software-eng</EM> archive</A> and
<A HREF=http://www.cis.ohio-state.edu/hypertext/faq/usenet/software-eng/top.html>
FAQ message information</A> especially <A
HREF=http://www.cis.ohio-state.edu/hypertext/faq/usenet/software-eng/part3/faq-doc-5.html>
formal specification</A>.

<P><LI>
<A HREF=news:news.announce.conferences><EM>
News.announce.conferences</EM></A> - announcements of conferences
including many specifically on formal methods
or with a formal methods content (e.g., see 
<A HREF=/archive/formal-methods/meetings.html>separated page on
meetings</A>).

</UL>
<P>

<!30 Nov 94>
<!18 Jan 95>
An electronic mailing list mostly concerned with educational issues
relating to formal methods in computer science is available.  Email <A
HREF=mailto:[e-mail]>
<EM>[e-mail]</EM></A> to join/leave the
list and <A HREF=mailto:[e-mail]>
<EM>[e-mail]</EM></A> to post to the list.  <P>


<H2><A NAME=other>Of related interest</A></H2>

See also information on:

<UL>

<LI><!5 Dec 95>
<iMG ALT="!" SRC="http://www.w3.org/hypertext/WWW/Icons/WWW/new.gif" HEIGHT=11 WIDTH=5>
<iMG ALT="*" SRC="http://www.w3.org/hypertext/WWW/Icons/WWW/star11t.gif" HEIGHT=11 WIDTH=11>
<A HREF=http://www-formal.stanford.edu/clt/ARS/ars-db.html>
Automated reasoning systems</A>
(see also systems
<A HREF=http://js-sfbsun.cs.uni-sb.de/pub/www/deduktion/systems-germany.html>
developed in Germany</A>)

<LI>
<A HREF=/archive/concurrent.html> Concurrent systems</A>

<LI>
<A HREF=/archive/logic-prog.html> Logic programming</A>

<LI><!9 Nov 94>
<A NAME=LF HREF=http://www.cs.cmu.edu/afs/cs/user/fp/www/lfs.html>
Logical frameworks</A>

<LI>
<A HREF=/archive/safety.html> Safety-critical systems</A>

<LI><!19 Oct 95>
<A HREF=http://cuiwww.unige.ch/db-research/Enseignement/analyseinfo/BNFweb.html>
BNF</A> (Backus-Naur Form notation) 

</UL>

<P>

<HR SIZE=10>

Last updated by
<A HREF=/oucl/people/jonathan.bowen.html>Jonathan Bowen</A>,
<!22 Nov 95>
<iMG ALT="!" SRC="http://www.w3.org/hypertext/WWW/Icons/WWW/new.gif" HEIGHT=11 WIDTH=5>
<A HREF=http://www.cs.reading.ac.uk/cs/research/fmg/>
Formal Methods Group</A>,
<A HREF=http://www.cs.reading.ac.uk/cs/>
Dept. of Computer Science</A>,
<A HREF=http://www.reading.ac.uk/>
University of Reading</A>,
5 December 1995.<BR>
Further information for possible inclusion is welcome.<P>

Part of the <A HREF=/oucl.html> OUCL</A>
<A HREF=/archive/index.html> archive</A>.

</BODY>
</HTML>