Formal Methods Wiki
(New article)
 
 
(10 intermediate revisions by 5 users not shown)
Line 1: Line 1:
  +
{{VLfm}}
[[Image:VL2.jpg|160x|thumb|
 
<center>
 
<small>
 
[http://www.vlib.org/ Virtual Library]
 
----
 
[[Formal Methods]]
 
</small>
 
</center>
 
]]
 
   
 
<center><big>'''Formal Methods Projects'''</big></center>
<center>
 
  +
__TOC__
 
=Formal Methods Projects=
 
 
</center>
 
   
 
Please feel free to add formal methods projects with hyperlinks to this page. Alternatively, contact [[User:Jpbowen|Jonathan Bowen]] if you know of relevant online information not included here or would like to maintain information on a particular topic.
 
Please feel free to add formal methods projects with hyperlinks to this page. Alternatively, contact [[User:Jpbowen|Jonathan Bowen]] if you know of relevant online information not included here or would like to maintain information on a particular topic.
   
 
----
 
----
<!--
 
<center>[[Image:symbols.gif|100%px|__________]]</center>
 
-->
 
   
 
This web page contains some pointers to projects involved with formal methods which provide on-line information on the [http://www.w3.org/ World Wide Web].
 
This web page contains some pointers to projects involved with formal methods which provide on-line information on the [http://www.w3.org/ World Wide Web].
   
 
<!--
 
----
 
----
   
 
* [[#Individual projects|Individual projects]]
 
* [[#Individual projects|Individual projects]]
 
* [[#Other lists|Other lists]]
 
* [[#Other lists|Other lists]]
 
-->
 
 
----
 
----
   
 
==Individual projects==
 
==Individual projects==
   
* [http://www.cs.cmu.edu/afs/cs/project/able/www/able.html ABLE project] (Architecture Based Languages and Environments), exploring the formal basis for [http://www.sei.cmu.edu/~architecture/definitions.html Software Architecture].
+
* [http://www.cs.cmu.edu/afs/cs/project/able/www/able.html ABLE project] (Architecture Based Languages and Environments), exploring the formal basis for [http://www.sei.cmu.edu/~architecture/definitions.html Software Architecture].
* [http://www.ifi.uio.no/~olaf/ADAPT/ ADAPT-FT] project, Norway. Adaptation of Formal Techniques to Support the Development of Open Distributed Systems.
+
* [http://www.ifi.uio.no/~olaf/ADAPT/ ADAPT-FT] project, Norway. Adaptation of Formal Techniques to Support the Development of Open Distributed Systems.
* [http://www.ifad.dk/projects/afrodite.html Afrodite project], developing methodologies and tools for an object-oriented formal specification language based on [[#VDM|VDM]], VDM++.
+
* [http://www.ifad.dk/projects/afrodite.html Afrodite project], developing methodologies and tools for an object-oriented formal specification language based on [[#VDM|VDM]], VDM++.
* [http://set.gmd.de/EES/Synchronie.html AMICO project] on Analysis Methods in Co-Design, based on synchronous languages such as [[#LUSTRE| Lustre]] and [[#ESTEREL| Esterel]].
+
* [http://set.gmd.de/EES/Synchronie.html AMICO project] on Analysis Methods in Co-Design, based on synchronous languages such as [[#LUSTRE| Lustre]] and [[#ESTEREL| Esterel]].
* [http://ic-www.arc.nasa.gov/ic/projects/amphion/ Amphion project], Automatic Programming for Component Libraries. Knowledge-based software engineering (KBSE) at NASA.
+
* [http://ic-www.arc.nasa.gov/ic/projects/amphion/ Amphion project], Automatic Programming for Component Libraries. Knowledge-based software engineering (KBSE) at NASA.
* [http://www.mrc-apu.cam.ac.uk/amodeus/amodeus.html Amodeus project], ESPRIT BRA 7040, on cognitive modelling, system modelling, integration and evaluation, including [http://www.mrc-apu.cam.ac.uk/amodeus/people.html#YORKCS University of York] and [http://www.mrc-apu.cam.ac.uk/amodeus/people.html#RAL Rutheford Appleton Laboratory], UK.
+
* [http://www.mrc-apu.cam.ac.uk/amodeus/amodeus.html Amodeus project], ESPRIT BRA 7040, on cognitive modelling, system modelling, integration and evaluation, including [http://www.mrc-apu.cam.ac.uk/amodeus/people.html#YORKCS University of York] and [http://www.mrc-apu.cam.ac.uk/amodeus/people.html#RAL Rutheford Appleton Laboratory], UK.
* [http://www.cwi.nl/~gipe/asf+sdf.html ASF+SDF project].
+
* [http://www.cwi.nl/~gipe/asf+sdf.html ASF+SDF project].
* [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.
* [http://www.colognet.org/ CoLogNET] European Network of Excellent on Computational Logic including [[Image:star11t.gif|11px|*]] [http://fm.colognet.org/ formal methods].
+
* [http://www.colognet.org/ CoLogNET] European Network of Excellent on Computational Logic including [[Image:star11t.gif|11px|*]] [http://fm.colognet.org/ formal methods].
* [http://www.sics.se/fdt/comic.html COMIC project].
 
* [http://www.sics.se/fdt/concur2.html CONCUR2 project] on [[concurrency]].
+
* [http://www.sics.se/fdt/comic.html COMIC project].
* [http://www.sics.se/fdt/confer.html CONFER project].
+
* [http://www.sics.se/fdt/concur2.html CONCUR2 project] on [[concurrency]].
* [http://www.cs.man.ac.uk/fmethods/projects/essi-ConForm.html ConForm] project (ESSI).
+
* [http://www.sics.se/fdt/confer.html CONFER project].
* [http://cswww.essex.ac.uk/Research/FSS/projects/c-z.html Constructive Z] project.
+
* [http://www.cs.man.ac.uk/fmethods/projects/essi-ConForm.html ConForm] project (ESSI).
 
* [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.irisa.fr/ep-atr/welcome.english.html EP-ATR Project], IRISA, France. Design of embedded applications based on a synchronous computation model.
 
  +
* [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.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.irisa.fr/espresso/ Espresso Project], Environment for the Specification of Synchronous Reactive Programs, France. (In French.)
+
* [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.dit.upm.es/~cdk/euroform.html EuroFORM] project, investigating ''Formal Methods for Correct System Design'' (Human Capital and Mobility Project).
+
* [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.irisa.fr/espresso/ Espresso Project], Environment for the Specification of Synchronous Reactive Programs, France. (In French.)
* [http://www.ifad.dk/projects/fmeindsem.html FMEIndSem]<nowiki>: Formal Methods Europe Industrial Seminars. </nowiki>
 
  +
* [http://www.dit.upm.es/~cdk/euroform.html EuroFORM] project, investigating ''Formal Methods for Correct System Design'' (Human Capital and Mobility Project).
* [http://www.csr.ncl.ac.uk/projects/FMEInfRes.html FMEInfRes]<nowiki>: Formal Methods Europe Information Resources. See the </nowiki>[http://www.csr.ncl.ac.uk/projects/FME/InfRes/applications/ applications database]. See also [http://www.cs.tcd.ie/FME/PROJECTS/FMEInfRes.html TCD] and [http://www.ifad.dk/projects/fmeinfres.html IFAD] information.
 
* [http://www.ifad.dk/projects/fmguides.html FM-Guides] project - Guide Books and Videos for Managers on Formal Methods.
+
* [http://www.ifad.dk/projects/fmeindsem.html FMEIndSem]<nowiki>: Formal Methods Europe Industrial Seminars. </nowiki>
 
* [http://www.csr.ncl.ac.uk/projects/FMEInfRes.html FMEInfRes]<nowiki>: Formal Methods Europe Information Resources. See the </nowiki>[http://www.csr.ncl.ac.uk/projects/FME/InfRes/applications/ applications database]. See also [http://www.cs.tcd.ie/FME/PROJECTS/FMEInfRes.html TCD] and [http://www.ifad.dk/projects/fmeinfres.html IFAD] information.
* [http://www.fmnet.info/ FMnet] - Formal Methods Network.
 
* [http://www.cs.ukc.ac.uk/research/netdist/fmoods/projects.html FMOODS projects] (Formal Methods for Open Object-Based Distributed Systems)
+
* [http://www.ifad.dk/projects/fmguides.html FM-Guides] project - Guide Books and Videos for Managers on Formal Methods.
 
* [http://www.fmnet.info/ FMnet] - Formal Methods Network.
* [http://www4.informatik.tu-muenchen.de/FORSCHUNG/A6_TitelE.html Focus]<nowiki>: A Design Methodology for Distributed Systems. </nowiki>
 
  +
* [http://www.cs.ukc.ac.uk/research/netdist/fmoods/projects.html FMOODS projects] (Formal Methods for Open Object-Based Distributed Systems)
* [http://www.sfb501.uni-kl.de/c1doc/C1.html Formal Description Techniques] Project C1, University of Kaiserslautern, Germany.
 
 
* [http://www4.informatik.tu-muenchen.de/FORSCHUNG/A6_TitelE.html Focus]<nowiki>: A Design Methodology for Distributed Systems. </nowiki>
* [http://www.cs.tcd.ie/FME/PROJECTS/Master.html Formal Methods Europe projects].
 
* [http://www.cs.man.ac.uk/fmethods/projects/formal-support-ella.html Formal verification support for ELLA] project.
+
* [http://www.sfb501.uni-kl.de/c1doc/C1.html Formal Description Techniques] Project C1, University of Kaiserslautern, Germany.
 
* [http://www.cs.tcd.ie/FME/PROJECTS/Master.html Formal Methods Europe projects].
* [http://www.cs.ubc.ca/formalWARE/ ''formal''WARE] industry/university collaborative research project, Canada. See [http://www.cs.ubc.ca/spider/day/Research/SeparationMinima/SeparationMinima.html Separation Minima for Aircraft in the North Atlantic Region Formalization and Analysis of the Separation Minima for Aircraft in the North Atlantic Region].
 
  +
* [http://www.cs.man.ac.uk/fmethods/projects/formal-support-ella.html Formal verification support for ELLA] project.
 
* [http://www.cs.ubc.ca/formalWARE/ ''formal''WARE] industry/university collaborative research project, Canada. See [http://www.cs.ubc.ca/spider/day/Research/SeparationMinima/SeparationMinima.html Separation Minima for Aircraft in the North Atlantic Region Formalization and Analysis of the Separation Minima for Aircraft in the North Atlantic Region].
 
* [http://www.dit.upm.es/~format/ FORMAT project].
 
* [http://www.dit.upm.es/~format/ FORMAT project].
 
* [http://www.fortest.org.uk/ FORTEST] Network, UK. Formal methods and testing.
 
* [http://www.fortest.org.uk/ FORTEST] Network, UK. Formal methods and testing.
* [http://www.haifa.il.ibm.com/projects/verification/genevieve.html GENeration ENvironment for Effective VErification] (GENEVIEVE), [http://www.haifa.il.ibm.com/ IBM Research Lab], Haifa, Israel.
+
* [http://www.haifa.il.ibm.com/projects/verification/genevieve.html GENeration ENvironment for Effective VErification] (GENEVIEVE), [http://www.haifa.il.ibm.com/ IBM Research Lab], Haifa, Israel.
* [http://www.cse.ogi.edu/PacSoft/projects/Hawk/ Hawk]<nowiki>: Specifying, Verifying, and Simulating Microprocessors. </nowiki>
+
* [http://www.cse.ogi.edu/PacSoft/projects/Hawk/ Hawk]<nowiki>: Specifying, Verifying, and Simulating Microprocessors. </nowiki>
* [http://www-cse.ucsd.edu/users/goguen/projs/halg.html Hidden Algebra] project.
+
* [http://www-cse.ucsd.edu/users/goguen/projs/halg.html Hidden Algebra] project.
* [http://nemo.ncsl.nist.gov/ahis/CHISSA.html HISSA]<nowiki>: High Integrity Software Systems Assurance Project. </nowiki>
+
* [http://nemo.ncsl.nist.gov/ahis/CHISSA.html HISSA]<nowiki>: High Integrity Software Systems Assurance Project. </nowiki>
* [http://www.compapp.dcu.ie/~gclynch/insyde.html INSYDE project] (INtegrated Methods for evolving SYstem DEsign).
+
* [http://www.compapp.dcu.ie/~gclynch/insyde.html INSYDE project] (INtegrated Methods for evolving SYstem DEsign).
* [http://www.ifad.dk/projects/iptes.html IPTES project].
+
* [http://www.ifad.dk/projects/iptes.html IPTES project].
* [http://www.cl.cam.ac.uk/Research/HVG/Isabelle/projects.html Isabelle projects].
+
* [http://www.cl.cam.ac.uk/Research/HVG/Isabelle/projects.html Isabelle projects].
* [http://i12www.ira.uka.de/~key/ KeY project]<nowiki>: Integrated Deductive Software Design. </nowiki>
+
* [http://i12www.ira.uka.de/~key/ KeY project]<nowiki>: Integrated Deductive Software Design. </nowiki>
  +
* [http://symbolaris.com/info/KeYmaera.html KeYmaera project]<nowiki>: Hybrid Systems Design and Verification. </nowiki>
* [http://www.informatik.uni-bremen.de/~inform/forschung/korso/korso.html KORSO project] (1991–1994) on correct software (Germany).
 
* [http://www.research.digital.com/SRC/tla/logic-calculators.html Logic Calculator Project].
+
* [http://www.informatik.uni-bremen.de/~inform/forschung/korso/korso.html KORSO project] (1991–1994) on correct software (Germany).
  +
* [http://www.research.digital.com/SRC/tla/logic-calculators.html Logic Calculator Project].
* [http://www.logosphere.org/ Logosphere] project. A formal digital library, Department of Computer Science, Yale University, USA.
+
* [http://www.logosphere.org/ Logosphere] project. A formal digital library, Department of Computer Science, Yale University, USA.
* [http://www.sics.se/fdt/lomaps.html LOMAPS project].
 
* [http://www.cis.rl.ac.uk/proj/mafmeth.html MaFMeth project], using [[#B| B-Tool]] and [[#VDM|VDM-SL]].
+
* [http://www.sics.se/fdt/lomaps.html LOMAPS project].
* [http://agamenon.uniandes.edu.co/~manta/historia_eng.html ManTa project], Colombia. Abstract Datatype handler - tool and methodology.
+
* [http://www.cis.rl.ac.uk/proj/mafmeth.html MaFMeth project], using [[#B| B-Tool]] and [[#VDM|VDM-SL]].
  +
* [http://agamenon.uniandes.edu.co/~manta/historia_eng.html ManTa project], Colombia. Abstract Datatype handler - tool and methodology.
* [http://www.csci.csusb.edu/dick/maths/home.html MATHS Project]. See [http://www.csci.csusb.edu/dick/monograph/10.manifesto.html manifesto] and [http://www.csci.csusb.edu/dick/samples/ samples of syntax description] including a [http://www.csci.csusb.edu/dick/samples/z.syntax.html Z syntax].
+
* [http://www.csci.csusb.edu/dick/maths/home.html MATHS Project]. See [http://www.csci.csusb.edu/dick/monograph/10.manifesto.html manifesto] and [http://www.csci.csusb.edu/dick/samples/ samples of syntax description] including a [http://www.csci.csusb.edu/dick/samples/z.syntax.html Z syntax].
 
* [http://www.matisse.qinetiq.com/ MATISSE project].
 
* [http://www.matisse.qinetiq.com/ MATISSE project].
 
* [http://www.mizar.org/project/ Mizar Project], started about 1973. An attempt to reconstruct mathematical vernacular.
 
* [http://www.mizar.org/project/ Mizar Project], started about 1973. An attempt to reconstruct mathematical vernacular.
* [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''.
* [http://uebb.cs.tu-berlin.de/~opal/ OPAL Project] concerned a programming environment where advanced language concepts and formal development methods can be used for creating production-quality software using the algebraic programming language, OPAL, which integrates both concepts of algebraic specification and functional programming.
+
* [http://uebb.cs.tu-berlin.de/~opal/ OPAL Project] concerned a programming environment where advanced language concepts and formal development methods can be used for creating production-quality software using the algebraic programming language, OPAL, which integrates both concepts of algebraic specification and functional programming.
* [http://progwww.vub.ac.be/prog/pools/opus/opus.html OPUS project], developing a formal model for expressing the essential object-oriented features.
+
* [http://progwww.vub.ac.be/prog/pools/opus/opus.html OPUS project], developing a formal model for expressing the essential object-oriented features.
* [http://archive.museophile.lsbu.ac.uk/osaf/ OMI Software Architecture Forum] (20858) including [http://archive.museophile.lsbu.ac.uk/osaf/links.html#proof proof approaches]
+
* [http://archive.museophile.lsbu.ac.uk/osaf/ OMI Software Architecture Forum] (20858) including [http://archive.museophile.lsbu.ac.uk/osaf/links.html#proof proof approaches]
* [http://www.cs.man.ac.uk/fmethods/projects/pobl-development-method.html `pobl' project] on a development method for concurrent (object based) programs.
 
  +
* [http://www.cs.man.ac.uk/fmethods/projects/pobl-development-method.html `pobl' project] on a development method for concurrent (object based) programs.
 
* '''[[ProCoS]]''', ''Provably Correct Systems'':
 
* '''[[ProCoS]]''', ''Provably Correct Systems'':
 
** [[ProCoS I|'''ProCoS I''' project]] (1989–1992).
 
** [[ProCoS I|'''ProCoS I''' project]] (1989–1992).
Line 98: Line 89:
 
** [[ProCoS Co-design|''Provably Correct Hardware/Software Co-design'']].
 
** [[ProCoS Co-design|''Provably Correct Hardware/Software Co-design'']].
 
* [http://www.fzi.de/divisions/prost/projects/production_cell/ProductionCell.html "Production Cell" Case Study] — a number of different formal methods have been applied to a robot-based application. (See also [[ProCoS Production Cell| here]].)
 
* [http://www.fzi.de/divisions/prost/projects/production_cell/ProductionCell.html "Production Cell" Case Study] — a number of different formal methods have been applied to a robot-based application. (See also [[ProCoS Production Cell| here]].)
* [http://www.inria.fr/Equipes/PROGRAIS-eng.html PROGRAIS project] on ''Derivation of specifications and programs''.
+
* [http://www.inria.fr/Equipes/PROGRAIS-eng.html PROGRAIS project] on ''Derivation of specifications and programs''.
* [http://www.informatik.uni-bremen.de/~inform/forschung/prospectra/prospectra.html PROSPECTRA project] (1985–1990) on correct software (ESPRIT).
+
* [http://www.informatik.uni-bremen.de/~inform/forschung/prospectra/prospectra.html PROSPECTRA project] (1985–1990) on correct software (ESPRIT).
* [http://www.dcs.gla.ac.uk/prosper/ PROSPER] — Proof and Specification Assisted Design Environments (ESPRIT Framework IV LTR 262).
+
* [http://www.dcs.gla.ac.uk/prosper/ PROSPER] — Proof and Specification Assisted Design Environments (ESPRIT Framework IV LTR 262).
* [http://dream.dai.ed.ac.uk/raise/project.html RAISE projects].
+
* [http://dream.dai.ed.ac.uk/raise/project.html RAISE projects].
* [http://anna.stanford.edu/rapide/rapide.html Rapide Project], Standford University, USA.
+
* [http://anna.stanford.edu/rapide/rapide.html Rapide Project], Standford University, USA.
 
* [http://www.comp.lancs.ac.uk/computing/research/cseg/projects/reaims/ REAIMS] (ESPRIT Project 8649). Requirements Engineering adaptation and improvement for safety and dependability. Including the [[B-Method]].
 
* [http://www.comp.lancs.ac.uk/computing/research/cseg/projects/reaims/ REAIMS] (ESPRIT Project 8649). Requirements Engineering adaptation and improvement for safety and dependability. Including the [[B-Method]].
 
* [[REDO project]] (1989–1992) on formal methods for reverse engineering in the software maintenance process (ESPRIT II).
 
* [[REDO project]] (1989–1992) on formal methods for reverse engineering in the software maintenance process (ESPRIT II).
* [http://wwwseti.cs.utwente.nl/~zwiers/react.html REACT] project.
+
* [http://wwwseti.cs.utwente.nl/~zwiers/react.html REACT] project.
* [http://www.ukc.ac.uk/electronics/research/digital/reasoning.html Reasoning about non-ideal digital circuits] — UK EPSRC project at {{wp|University of Kent}}.
+
* [http://www.ukc.ac.uk/electronics/research/digital/reasoning.html Reasoning about non-ideal digital circuits] — UK EPSRC project at {{wp|University of Kent}}.
 
* [http://www.refinenet.org.uk/ RefineNet] Network, UK. Refinement of formal specifications.
 
* [http://www.refinenet.org.uk/ RefineNet] Network, UK. Refinement of formal specifications.
* [http://www.dur.ac.uk/~dcs0ns/research/csm/rip/ReForm.html ReForm project]<nowiki>: From assembler to </nowiki>[http://vl.zuser.org/ Z] using formal transformations. See also [http://www.dur.ac.uk/~dcs0ns/research/csm/rip/proof.html A Proof Theory for Program Refinement and Equivalence: Extensions].
+
* [http://www.dur.ac.uk/~dcs0ns/research/csm/rip/ReForm.html ReForm project]<nowiki>: From assembler to </nowiki>[http://vl.zuser.org/ Z] using formal transformations. See also [http://www.dur.ac.uk/~dcs0ns/research/csm/rip/proof.html A Proof Theory for Program Refinement and Equivalence: Extensions].
* [http://rodin.cs.ncl.ac.uk/ RODIN Project]<nowiki>: Rigorous Open Development Environment for Complex Systems. </nowiki>
+
* [http://rodin.cs.ncl.ac.uk/ RODIN Project]<nowiki>: Rigorous Open Development Environment for Complex Systems. </nowiki>
* [http://www.cs.kun.nl/ita/research/projects/rths/ RTHS project] (Real-Time and Hybrid Systems).
+
* [http://www.cs.kun.nl/ita/research/projects/rths/ RTHS project] (Real-Time and Hybrid Systems).
* [http://www.haifa.il.ibm.com/projects/verification/RB_Homepage/ RuleBase project], [http://www.haifa.il.ibm.com/ IBM Research Lab], Haifa, Israel. Model-checking tool including on-line [http://www.haifa.il.ibm.com/projects/verification/RB_Homepage/demo.html demonstration].
+
* [http://www.haifa.il.ibm.com/projects/verification/RB_Homepage/ RuleBase project], [http://www.haifa.il.ibm.com/ IBM Research Lab], Haifa, Israel. Model-checking tool including on-line [http://www.haifa.il.ibm.com/projects/verification/RB_Homepage/demo.html demonstration].
* [http://www.cs.rhbnc.ac.uk/fmg/safefm.html SafeFM Project] on the practical application of Formal Methods to Safety-Critical Systems.
+
* [http://www.cs.rhbnc.ac.uk/fmg/safefm.html SafeFM Project] on the practical application of Formal Methods to Safety-Critical Systems.
 
* [[SAFEMOS| '''safemos''' project]] (1989–1993) on ''Totally Verified Systems''.
 
* [[SAFEMOS| '''safemos''' project]] (1989–1993) on ''Totally Verified Systems''.
 
* [http://www.inria.fr/Equipes/SAFIR-eng.html SAFIR project] on '' Algebraic formal systems for industry and research''.
 
* [http://www.inria.fr/Equipes/SAFIR-eng.html SAFIR project] on '' Algebraic formal systems for industry and research''.
* [http://www.cse.ogi.edu/PacSoft/Blackberry.html SDRR Project] on Software Design for Reliability and Reuse.
+
* [http://www.cse.ogi.edu/PacSoft/Blackberry.html SDRR Project] on Software Design for Reliability and Reuse.
 
* [http://lml.ls.fi.upm.es/slam/ SLAM Project] on formal methods in the development process, [http://lml.ls.fi.upm.es/babel/ Babel Group], Madrid, Spain.
 
* [http://lml.ls.fi.upm.es/slam/ SLAM Project] on formal methods in the development process, [http://lml.ls.fi.upm.es/babel/ Babel Group], Madrid, Spain.
* [http://www.csd.hku.hk/~tse/projects.html Software Engineering Projects], [http://www.csd.hku.hk/~tse/seg.html Software Engineering Group], [http://www.csd.hku.hk/ Department of Computer Science], The University of Hong Kong. Object-oriented and formal methods.
+
* [http://www.csd.hku.hk/~tse/projects.html Software Engineering Projects], [http://www.csd.hku.hk/~tse/seg.html Software Engineering Group], [http://www.csd.hku.hk/ Department of Computer Science], The University of Hong Kong. Object-oriented and formal methods.
* [http://spy.sci.univr.it/ SPY Lab] project. Static Program Analysis by Abstract Interpretation.
+
* [http://spy.sci.univr.it/ SPY Lab] project. Static Program Analysis by Abstract Interpretation.
* [http://set.gmd.de/EES/Synchronie.html SYNCHRONIE project] on Synchronous Programming for Embedded Systems.
+
* [http://set.gmd.de/EES/Synchronie.html SYNCHRONIE project] on Synchronous Programming for Embedded Systems.
* [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
* [http://i44s11.info.uni-karlsruhe.de/~verifix/ VERIFIX project]: provably correct compilers, {{wp|University of Karlsruhe}}, Germany.
+
* [http://i44s11.info.uni-karlsruhe.de/~verifix/ VERIFIX project]: provably correct compilers, {{wp|University of Karlsruhe}}, Germany.
 
* [http://isabelle.in.tum.de/verisoft/ Verisoft @ Munich], Technische Universit&auml;t M&uuml;nchen, Germany.
 
* [http://isabelle.in.tum.de/verisoft/ Verisoft @ Munich], Technische Universit&auml;t M&uuml;nchen, Germany.
* [http://www-verimag.imag.fr/VHS/ VHS Project]<nowiki>: Verification of Hybrid Systems (ESPRIT-LTR Project 26270), VERIMAG, France. </nowiki>
+
* [http://www-verimag.imag.fr/VHS/ VHS Project]<nowiki>: Verification of Hybrid Systems (ESPRIT-LTR Project 26270), VERIMAG, France. </nowiki>
* [http://www.dfki.de/pas/f2w.cgi?dmass/vse-e VSE] and [http://www.dfki.de/pas/f2w.cgi?dmasp/vseII-e VSE-II] Verification Support Environment projects, Germany. Provably Correct Software through Formal Program Development.
+
* [http://www.dfki.de/pas/f2w.cgi?dmass/vse-e VSE] and [http://www.dfki.de/pas/f2w.cgi?dmasp/vseII-e VSE-II] Verification Support Environment projects, Germany. Provably Correct Software through Formal Program Development.
 
* [[VSR-net]] Network, UK. Verified Software Repository.
 
* [[VSR-net]] Network, UK. Verified Software Repository.
   
 
==Other lists==
 
==Other lists==
   
* [http://www.ifad.dk/projects/projects.html IFAD projects], [http://www.ifad.dk/ IFAD], Denmark.
+
* [http://www.ifad.dk/projects/projects.html IFAD projects], [http://www.ifad.dk/ IFAD], Denmark.
* [http://ls4-www.informatik.uni-dortmund.de/RVS/agrvse.html#Forschungsarbeiten Research projects] on the application of formal description techniques (FDTs) including [[#TLA| TLA]].
+
* [http://ls4-www.informatik.uni-dortmund.de/RVS/agrvse.html#Forschungsarbeiten Research projects] on the application of formal description techniques (FDTs) including [[#TLA| TLA]].
* [http://www.sics.se/fdt/projects.html Research projects], [http://www.sics.se/ SICS/KTH], Sweden.
+
* [http://www.sics.se/fdt/projects.html Research projects], [http://www.sics.se/ SICS/KTH], Sweden.
* [http://www.brics.dk/Projects/ BRICS projects], [http://www.brics.dk/ Centre for Basic Research in Computer Science], Denmark.
+
* [http://www.brics.dk/Projects/ BRICS projects], [http://www.brics.dk/ Centre for Basic Research in Computer Science], Denmark.
* [http://www.cs.man.ac.uk/fmethods/projects/ Manchester University Formal Methods Group projects], UK.
+
* [http://www.cs.man.ac.uk/fmethods/projects/ Manchester University Formal Methods Group projects], UK.
   
 
----
 
----
   
Last updated by [[Jonathan Bowen]], 12 March 2009. <br />
+
Last updated by [[Jonathan Bowen]], 18 March 2009.<br />
 
Further information for possible inclusion is welcome.
 
Further information for possible inclusion is welcome.
   
 
Part of the [[Virtual Library]] on the [[Formal Methods Wiki]].
 
Part of the [[Virtual Library]] on the [[Formal Methods Wiki]].
 
 
[[Category:Formal methods|*Projects]]
 
[[Category:Formal methods|*Projects]]
  +
[[Category:Projects| ]]
 
[[Category:Virtual Library]]
 
[[Category:Virtual Library]]

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.