Formal Methods Wiki
 
(5 intermediate revisions by 2 users not shown)
Line 29: Line 29:
 
* [http://www.cis.rl.ac.uk/proj/but.html B User Trials] (BUT) project, using the [[#B| B-Tool]].
 
* [http://www.cis.rl.ac.uk/proj/but.html B User Trials] (BUT) project, using the [[#B| B-Tool]].
 
* [http://lifc.univ-fcomte.fr/RECHERCHE/TFC/Page_BZ-TT.html BZ-Testing-Tools Project] (in French and [http://translate.google.com/translate?hl=en&u=http://lifc.univ-fcomte.fr/RECHERCHE/TFC/Page_BZ-TT.html English]).
 
* [http://lifc.univ-fcomte.fr/RECHERCHE/TFC/Page_BZ-TT.html BZ-Testing-Tools Project] (in French and [http://translate.google.com/translate?hl=en&u=http://lifc.univ-fcomte.fr/RECHERCHE/TFC/Page_BZ-TT.html English]).
  +
* [http://cadp.inria.fr/ CADP] . A comprehensive toolbox for the Construction and Analysis of Distributed Processes (1986-now).
 
* [http://www.brics.dk/Projects/CoFI/ CoFI]<nowiki>: The Common Framework Initiative for Algebraic Specification and Development. See </nowiki>[http://www.brics.dk/Projects/CoFI/Documents/CASL/Summary/ CASL summary] (Common Algebraic Specification Language), [http://www.loria.fr/~hkirchne/COFI-TOOLS/ CoFI tools] and [http://www.dcs.ed.ac.uk/home/dts/CoFI-WG/ CoFI Working Group] information.
 
* [http://www.brics.dk/Projects/CoFI/ CoFI]<nowiki>: The Common Framework Initiative for Algebraic Specification and Development. See </nowiki>[http://www.brics.dk/Projects/CoFI/Documents/CASL/Summary/ CASL summary] (Common Algebraic Specification Language), [http://www.loria.fr/~hkirchne/COFI-TOOLS/ CoFI tools] and [http://www.dcs.ed.ac.uk/home/dts/CoFI-WG/ CoFI Working Group] information.
 
* [http://www.itee.uq.edu.au/~gwat/Cogito_1.html Cogito 1 project], SVRC, Australia.
 
* [http://www.itee.uq.edu.au/~gwat/Cogito_1.html Cogito 1 project], SVRC, Australia.
Line 38: Line 39:
 
* [http://cswww.essex.ac.uk/Research/FSS/projects/c-z.html Constructive Z] project.
 
* [http://cswww.essex.ac.uk/Research/FSS/projects/c-z.html Constructive Z] project.
 
* [http://coq.inria.fr/ Coq project] on ''Software specifications and proofs''. See also [http://www.inria.fr/Equipes/COQ-eng.html here].
 
* [http://coq.inria.fr/ Coq project] on ''Software specifications and proofs''. See also [http://www.inria.fr/Equipes/COQ-eng.html here].
* [http://www.deploy-project.eu/ DEPLOY project] on the Industrial deployment of system engineering methods providing high dependability and productivity. See also the [http://fm4industry.cetic.be FAQ on evidence about the use and the impact of formal engineering methods in Industry]
+
* [http://www.deploy-project.eu/ DEPLOY project] on the Industrial deployment of system engineering methods providing high dependability and productivity. See also the [http://www.fm4industry.org FAQ on evidence about the use and the impact of formal engineering methods in Industry]
 
* [http://www.irisa.fr/ep-atr/welcome.english.html EP-ATR Project], IRISA, France. Design of embedded applications based on a synchronous computation model.
 
* [http://www.irisa.fr/ep-atr/welcome.english.html EP-ATR Project], IRISA, France. Design of embedded applications based on a synchronous computation model.
 
* [http://www.first.gmd.de/org/espres.html ESPRESS project], Engineering of safety-critical embedded systems, Germany. (See also [http://www.first.gmd.de/~espress/ here].)
 
* [http://www.first.gmd.de/org/espres.html ESPRESS project], Engineering of safety-critical embedded systems, Germany. (See also [http://www.first.gmd.de/~espress/ here].)
Line 75: Line 76:
 
* [http://theoretica.Informatik.Uni-Oldenburg.DE/~moby/ MOBY project].
 
* [http://theoretica.Informatik.Uni-Oldenburg.DE/~moby/ MOBY project].
 
* [http://www.brics.dk/mona/ MONA/FIDO Project].
 
* [http://www.brics.dk/mona/ MONA/FIDO Project].
  +
* [http://vasy.inria.fr/multival/rapport2010.html MULTIVAL]: Industrial project on formal methods for high-performance multiprocessor and network-on-chip architectures (2006-2011)
 
* [http://www.cs.man.ac.uk/fmethods/projects/mural.html Mural] project (1984–1988).
 
* [http://www.cs.man.ac.uk/fmethods/projects/mural.html Mural] project (1984–1988).
 
* [http://polaris.dit.upm.es/~cdk/nada.html NADA] ESPRIT Working Group on ''New Hardware Design Methods''.
 
* [http://polaris.dit.upm.es/~cdk/nada.html NADA] ESPRIT Working Group on ''New Hardware Design Methods''.
Line 111: Line 113:
 
* [http://www.cs.ucsd.edu/groups/tatami/ Tatami Project]: [http://www.cs.ucsd.edu/groups/tatami/kumo/ Kumo] web-based proof assistant and [http://www.cs.ucsd.edu/groups/tatami/bobj/ BOBJ] system for behavioural specification. See also [http://www.cs.ucsd.edu/users/goguen/projs/tut.html here].
 
* [http://www.cs.ucsd.edu/groups/tatami/ Tatami Project]: [http://www.cs.ucsd.edu/groups/tatami/kumo/ Kumo] web-based proof assistant and [http://www.cs.ucsd.edu/groups/tatami/bobj/ BOBJ] system for behavioural specification. See also [http://www.cs.ucsd.edu/users/goguen/projs/tut.html here].
 
* [http://ls4-www.informatik.uni-dortmund.de/RVS/P-TLA/ Tools for TLA] project.
 
* [http://ls4-www.informatik.uni-dortmund.de/RVS/P-TLA/ Tools for TLA] project.
  +
* [http://www.topcased.org TOPCASED] project: The Open-Source Toolkit for Critical Systems.
 
* [http://www.fokus.gmd.de/step/topic/entry.html TOPIC], RACE Project R2088, a Toolset for Protocol and Advanced Service Verification in IBC Environments, using formal methods and tools.
 
* [http://www.fokus.gmd.de/step/topic/entry.html TOPIC], RACE Project R2088, a Toolset for Protocol and Advanced Service Verification in IBC Environments, using formal methods and tools.
 
* [http://www.informatik.uni-bremen.de/~uniform/ UniForM project] (Universal Formal Methods workbench), Germany.
 
* [http://www.informatik.uni-bremen.de/~uniform/ UniForM project] (Universal Formal Methods workbench), Germany.
 
* [http://www.cs.utah.edu/projects/formal_verification/ Utah Verifier (UV) Project]: Formal Methods in System Design and Verification, Department of Computer Science, {{wp|University of Utah}}, USA.
 
* [http://www.cs.utah.edu/projects/formal_verification/ Utah Verifier (UV) Project]: Formal Methods in System Design and Verification, Department of Computer Science, {{wp|University of Utah}}, USA.
  +
* [http://vasy.inria.fr VASY Team], INRIA Grenoble, France. Validation of Systems - CADP toolbox.
 
* [http://www.cs.cmu.edu/afs/cs.cmu.edu/project/venari/www/home.html Venari Project], CMU, USA. Specification and language support for transactions.
 
* [http://www.cs.cmu.edu/afs/cs.cmu.edu/project/venari/www/home.html Venari Project], CMU, USA. Specification and language support for transactions.
 
* [http://www.verificard.org/ VerifiCard Project]: Smartcard verification
 
* [http://www.verificard.org/ VerifiCard Project]: Smartcard verification

Latest revision as of 16:33, 18 March 2012

Virtual Library
Computing
Software engineering
Formal methods

Formal Methods Projects

Please feel free to add formal methods projects with hyperlinks to this page. Alternatively, contact Jonathan Bowen if you know of relevant online information not included here or would like to maintain information on a particular topic.


This web page contains some pointers to projects involved with formal methods which provide on-line information on the World Wide Web.


Individual projects

Other lists


Last updated by Jonathan Bowen, 18 March 2009.
Further information for possible inclusion is welcome.

Part of the Virtual Library on the Formal Methods Wiki.