📄 http:^^www.cs.utexas.edu^users^boyer^courses^backup-formal-methods.html
字号:
MIME-Version: 1.0
Server: CERN/3.0
Date: Wednesday, 08-Jan-97 16:30:09 GMT
Content-Type: text/html
Content-Length: 25828
Last-Modified: Wednesday, 17-Jan-96 23:03:29 GMT
<HTML><HEAD><TITLE>The World Wide Web Virtual Library:Formal Methods</TITLE><LINK REV=made HREF="mailto:J.P.Bowen@reading.ac.uk"><!-- Maintained by: Jonathan Bowen, Oxford University Computing Laboratory --><!-- Usage: 150 --><!-- Links: 153 --><!-- Cited: W.W. Gibbs, Software's Chronic Crisis. Scientific American, 271(3):86-95, September 1994 --></HEAD><BODY bgcolor="ffffff"><BODY><A NAME=top HREF=http://www.w3.org/hypertext/DataSources/bySubject/Overview2.html><iMG ALT="*" SRC="/archive/gifs/Virtual_Library.gif" HEIGHT=48 WIDTH=48 BORDER=0>Virtual Library</A><A HREF=http://src.doc.ic.ac.uk/bySubject/Computing/Overview.html><iMG ALT="*" SRC="/archive/gifs/Virtual_Library.gif" HEIGHT=48 WIDTH=48 BORDER=0>Computing</A><A HREF=http://ricis.cl.uh.edu/virt-lib/soft-eng.html><iMG ALT="*" SRC="/archive/gifs/Virtual_Library.gif" HEIGHT=48 WIDTH=48 BORDER=0>Software Engineering</A><CENTER><H1><A HREF=http://wombat.doc.ic.ac.uk/?formal+methods>Formal Methods</A></H1></CENTER>Please mail <A HREF=mailto:J.P.Bowen@reading.ac.uk><EM>J.P.Bowen@reading.ac.uk</EM></A>if you know of relevant on-line information not included hereor would like to maintain information on a particular topic.Use the <A HREF=news:comp.specification><EM>comp.specification</EM></A>newsgroup, or the newer<!12 Jul 95><A HREF=news:comp.specification.misc><EM>comp.specification.misc</EM></A>newsgroup, for general formal methods queries.<P><CENTER><iMG SRC="/archive/formal-methods/symbols.gif" ALT="__________" HEIGHT=19 WIDTH=536></CENTER><P><!-- desc -->This document contains some pointers to informationon <A HREF=http://shemesh.larc.nasa.gov/whatfm.html><EM>Formal Methods</EM></A>available around the world on the<A HREF=http://www.w3.org/hypertext/WWW/TheProject.html>World Wide Web</A> (WWW), a global hypermedia system providing<A HREF=http://wings.buffalo.edu/world>worldwide information</A>.<!-- end_desc -->Links for accessing on-lineinformation in the following categories are available:<!-- fields --><UL><LI> <A HREF=/archive/formal-methods/announce.html>Announcement</A><LI> <A HREF=#latest><BLINK>Latest news</BLINK></A><LI> <A HREF=/archive/formal-methods/pubs.html#intro> Introductory articles</A><LI> <A HREF=#notations>Individual notations, methods and tools</A><LI> <A NAME=papers NAME=journals HREF=/archive/formal-methods/pubs.html>Publications</A> (including journals, papers, books, etc.)<LI> <A NAME=repositories HREF=/archive/formal-methods/repositories.html> Electronic repositories</A><LI> <A NAME=meetings HREF=/archive/formal-methods/meetings.html>Meetings</A><LI> <A HREF=/archive/formal-methods/projects.html>Projects</A><LI> <A HREF=/archive/formal-methods/companies.html>Companies</A><LI><!4 Apr 95> <A HREF=/archive/formal-methods/orgs.html>Organizations</A><LI> <A HREF=/archive/formal-methods/whos-who.html> Who's Who on the Web</A> in <A HREF=http://www.cs.man.ac.uk/fmethods/background.html> Formal Methods</A><LI> <A HREF=#news>Relevant newsgroups</A><LI> <A HREF=#other>Related topics</A></UL><!-- end_fields --><P><iMG ALT="!" SRC="http://www.w3.org/hypertext/WWW/Icons/WWW/new.gif" HEIGHT=11 WIDTH=5>indicates new entries.<iMG ALT="*" SRC="http://www.w3.org/hypertext/WWW/Icons/WWW/star11t.gif" HEIGHT=11 WIDTH=11>indicates a (subjectively!) recommended link for especially goodon-line information. If enough people email me, I will add a star toentries recommended by others. <P><A NAME=latest><iMG ALT="*" SRC="http://www.w3.org/hypertext/WWW/Icons/WWW/star11t.gif" HEIGHT=11 WIDTH=11><BLINK><B>Latest news:</B></BLINK><EM>This space will be used to indicate selected new entriesand developments in the formal methods pages. </EM><UL><LI><A HREF=http://www.informatik.uni-kiel.de/~procos/dag9523/dag9523.html>The Steam Boiler Control Specification Problem</A>by J.-R. Abrial, E. B鰎ger and H. Langmaack.A comparative case study for different formal techniques -further submissions are invited.(2 August 1995)<LI><A HREF=news:comp.specification.*><EM>Comp.specification.</EM>*</A> newsgroups.(12 July 1995)<LI><A HREF=http://www.daimi.aau.dk/~petrinet/>Petri Nets</A> graphical notation.(11 April 1995)<LI><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.(6 April 1995)<LI>A new<A HREF=#LOTOS>LOTOS</A> page.(16 February 1995)<LI>Information on<A HREF=#RAISE>RAISE</A> language and tools.(19 January 1995)<LI>A new section on the<A HREF=#B>B-Method</A> has been added.(6 January 1995)</UL><P><HR SIZE=10><H2><A NAME=notations>Individual notations, methods and tools</A></H2><UL><P><LI><A NAME=ACL2 HREF=http://www.cli.com/software/acl2/>Acl2</A> theorem prover, a successor to the<A HREF=#BM> Boyer-Moore theorem prover</A>.In progress - watch this space!<P><LI><!24 Mar 95><A NAME=ACTION HREF=http://www.daimi.aau.dk/~thales/as/AS.html>Action Semantics</A>, a framework for specifying formal semanticsof programming languages.<P><LI><!15 Mar 95><A NAME=ADL HREF=http://www.cse.ogi.edu/~sheard/adl.html>Algebraic Design Language</A>,a higher-order software specification language.<P><LI><A NAME=ASLAN HREF=ftp://ftp.cs.ucsb.edu/pub/aslan.rat.Z>ASLAN</A>, a specificationlanguage processor/proof obligation generator (email Dick Kemmerer on<A HREF=mailto:kemm@cs.ucsb.edu> <EM>kemm@cs.ucsb.edu</EM></A> forfurther details), and <A HREF=ftp://ftp.cs.ucsb.edu/pub/gil>GIL</A>, agraphical interval logic tool (email Laura Dillon on <AHREF=mailto:dillon@cs.ucsb.edu> <EM>dillon@cs.ucsb.edu</EM></A>for further details), areavailable from a formal support tools archive (see the <AHREF=ftp://ftp.cs.ucsb.edu/pub/INDEX> index</A>) at <AHREF=ftp://ftp.cs.ucsb.edu/pub/>UC Santa Barbara</A>.<P><LI><!21 Apr 95><A HREF=http://xenon.stanford.edu/~sankar/adlt-summary.html>Assertion Definition Language Translator</A> (ADLT),a specification based testing toolset.<P><LI><A NAME=BM> Boyer-Moore theorem prover(a forerunner of <A HREF=#NQTHM>Nqthm</A>).Available via <A HREF=/archive/logic-prog#IFS>ICOT Free Software</A> for use under Unix at<A HREF=ftp://ftp.sics.se/ifs/solver-prover/unix/bmtp.tar.Z>ICOT</A> (Japan),<A HREF=ftp://ftp.sics.se/ifs/solver-prover/unix/bmtp.tar.Z>SICS</A> (Sweden),<A HREF=ftp://ftp.gmd.se/ifs/solver-prover/unix/bmtp.tar.Z>GMD</A> (Germany) and<A HREF=ftp://ftp.sics.se/ifs/solver-prover/unix/bmtp.tar.Z>Univ. of Oregon</A> (USA).<P><LI><!5 Jan 95><A NAME=B HREF=/archive/formal-methods/b.html>B-Method</A>, including the B-Tool and B-Toolkit.<P><LI><!10 Jul 95><A NAME=CIRCAL HREF=http://cis0.levels.unisa.edu.au/www/projects/detail/circal.html>Circal</A> (CIRcuit CALculus) System supporting a process algebra whichmay be used to rigorously describe, verify and simulate concurrentsystems.<!ftp://circal-ftp.cs.strath.ac.uk/pub/CircSys.4.1.1.tar.Z><!ftp://lux.levels.unisa.edu.au/pub/circal/CircSys.4.1.1.tar.Z><P><LI><!8 Jun 95><A NAME=COLD HREF=http://www.cs.rug.nl/~rix/cold.html>COLD</A> (Common Object-oriented Language for Design), a wide-spectrum specification language. <!developed at Philips Research, Eindhoven.><!http://www.phil.ruu.nl/home/keesm/NSD.html><P><LI><A NAME=CONCURRENCYHREF=http://www.dcs.ed.ac.uk/packages/cwb/>CWB</A> (Edinburgh Concurrency Workbench), andautomated toolset.<P><LI><!24 Jul 95><A NAME=COQ HREF=http://pauillac.inria.fr/coq/systeme_coq-eng.html>Coq</EM> proof assistant.See also<!5 Jan 95><A NAME=CTCOQ HREF=http://www.inria.fr/croap/ctcoq/ctcoq-eng.html>CtCoq</EM>, a working environment for the<A HREF=http://www.inria.fr/Equipes/COQ-eng.html>Coq project</A> theorem prover.<P><LI><!12 Oct 95><A NAME=COSPAN HREF=ftp://ftp.research.att.com/dist/COSPAN/>COSPAN</A> (COordinated SPecification ANalysis),a general-purpose rapid-prototyping tool,using the S/R (selection/resolution) language.<P><LI><A NAME=CSP HREF=/archive/csp.html>CSP</A> (Communicating Sequential Processes) including the<A NAME=FDR HREF=ftp://ftp.comlab.ox.ac.uk/pub/CSP/FDR> FDR tool</A>.<P><LI><iMG ALT="*" SRC="http://www.w3.org/hypertext/WWW/Icons/WWW/star11t.gif" HEIGHT=11 WIDTH=11><A NAME=DISCOHREF=http://www.cs.tut.fi/laitos/DisCo/DisCo-english.fm.html> DisCo</A>is specification method for reactive systems including a <AHREF=http://www.cs.tut.fi/laitos/DisCo/tool.fm.html> tool</A> developedat the <A HREF=http://www.cs.tut.fi/>Tampere University ofTechnology</A>, Finland.<P><LI><A NAME=ESTELLE HREF=/archive/formal-methods/estelle.html>Estelle</A>:<!27 Feb 95><A HREF=http://alix.int-evry.fr/lor/edt.html><! ftp://157.159.100.27/EDTdemo/>EDT</A> (Estelle Development Toolset)and <A HREF=ftp://louie.udel.edu/pub/grope/estelle-specs/>example specifications</A>.Contact <A HREF=mailto:estelle-request@cs.umb.edu><EM>estelle-request@cs.umb.edu</EM></A> to join the mailing list.<P><LI><!21 Nov 95><iMG ALT="!" SRC="http://www.w3.org/hypertext/WWW/Icons/WWW/new.gif" HEIGHT=11 WIDTH=5><A HREF=http://litwww.epfl.ch/~shawn/Esterel/>Esterel</A>,for verifying safety properties in synchronous distributed systems.<P><LI><A NAME=EVES HREF=http://www.ora.on.ca/eves.html>EVES</A> tool, based on ZF set theory, from <AHREF=http://www.ora.on.ca/>ORA</A>, Canada.<! Email dan@ora.on.ca><!A HREF=http://www.engin.umich.edu/~huggins/ea/><P><LI><!3 Aug 95><A NAME=EA HREF=http://www.eecs.umich.edu/ealgebras/>Evolving Algebras</A>, University of Michigan, USA.<P><LI><A NAME=ML HREF=http://www.dcs.ed.ac.uk/staff/dts/eml>Extended ML</A>framework for the specification and <AHREF=http://www.dcs.ed.ac.uk/staff/dts/alf> formal development</A> ofmodular Standard ML programs.<P><LI><iMG ALT="*" SRC="http://www.w3.org/hypertext/WWW/Icons/WWW/star11t.gif" HEIGHT=11 WIDTH=11><A NAME=HOL HREF=/archive/formal-methods/hol.html>HOL</A> mechanical theorem proving system.<P><LI><!21 Nov 94><A NAME=HYTECH HREF=http://www.cs.cornell.edu/Info/People/tah/hytech.html>HyTech</A> is an automatic tool for the analysis of embedded systems.It computes the condition under which a linear hybrid system satisfiesa temporal-logic requirement. Installation requires a Mathematicalicense.<P><LI><iMG ALT="*" SRC="http://www.w3.org/hypertext/WWW/Icons/WWW/star11t.gif" HEIGHT=11 WIDTH=11><A NAME=IMPS HREF=file://math.harvard.edu/imps/imps_html/imps.html>IMPS</A>, an Interactive Mathematical Proof System intended to providemechanical support for traditional mathematical techniques and stylesof practice.<P><LI><iMG ALT="*" SRC="http://www.w3.org/hypertext/WWW/Icons/WWW/star11t.gif" HEIGHT=11 WIDTH=11><A NAME=ISABELLE HREF=http://www.cl.cam.ac.uk/Research/HVG/isabelle.html>Isabelle</A>.See also the Cambridge <A HREF=http://www.cl.cam.ac.uk/Research/HVG/>Automated Reasoning Group</A> and <A HREF=ftp://ftp.cl.cam.ac.uk/ml>FTPaccess</A> including an <A HREF=ftp://ftp.cl.cam.ac.uk/ml/>index</A>. Email <A HREF=http://www.cl.cam.ac.uk/users/lcp/><EM>Larry.Paulson-request@cl.cam.ac.uk</EM></A>for information, including requests concerning the<EM>isabelle-users@cl.cam.ac.uk</EM> mailing list.<P><LI><A NAME=JAPE HREF=/oucl/users/bernard.sufrin/jape.html>JAPE</A> (Just Another Proof Editor) by<A HREF=/oucl/people/bernard.sufrin.html>Bernard Sufrin</A> and<!17 Oct 95><A HREF=http://www.dcs.qmw.ac.uk/~richard/>Richard Bornat</A> is available via<A HREF=ftp://ftp.comlab.ox.ac.uk/pub/Packages/JAPE> anonymous FTP</A>.See also<!17 Oct 95><A HREF=ftp://ftp.dcs.qmw.ac.uk/programming/jape/index.html>MacOS JAPE</A>.<P><LI><!26 Sep 95><A NAME=KIV HREF=http://i11www.ira.uka.de/~kiv/>KIV</A> (Karlsruhe Interactive Verifier). A tool for the development of correct software using stepwise refinement.<P><LI><!8 Aug 95><!http://www.ahl.co.uk/products.html#lambda><A NAME=LAMBDA HREF=http://www.ahl.co.uk/lambda.html>LAMBDA</A> toolset from<A HREF=http://www.ahl.co.uk/>Abstract Hardware Ltd</A>, UK,supports <A HREF=http://www.ahl.co.uk/fmpt.html>formal verification</A> for hardware/software co-design.Email <A HREF=mailto:lamba@ahl.co.uk><EM>lambda@ahl.co.uk</EM></A>. To join the usergroup mailing list,email <A HREF=mailto:lambda-usergroup-request@dcs.ed.ac.uk><EM>lambda-usergroup-request@dcs.ed.ac.uk</EM></A>.<P><LI><iMG ALT="*" SRC="http://www.w3.org/hypertext/WWW/Icons/WWW/star11t.gif" HEIGHT=11 WIDTH=11><A NAME=LARCH HREF=http://larch-www.lcs.mit.edu:8001/larch/>Larch</A> and LP (<A NAME=LPHREF=http://larch-www.lcs.mit.edu:8001/larch/lp.html>Larch⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -