Projects

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

• ABLE project (Architecture Based Languages and Environments), exploring the formal basis for Software Architecture.
• ADAPT-FT project, Norway. Adaptation of Formal Techniques to Support the Development of Open Distributed Systems.
• Afrodite project, developing methodologies and tools for an object-oriented formal specification language based on VDM, VDM++.
• AMICO project on Analysis Methods in Co-Design, based on synchronous languages such as Lustre and Esterel.
• Amphion project, Automatic Programming for Component Libraries. Knowledge-based software engineering (KBSE) at NASA.
• Amodeus project, ESPRIT BRA 7040, on cognitive modelling, system modelling, integration and evaluation, including University of York and Rutheford Appleton Laboratory, UK.
• ASF+SDF project.
• B User Trials (BUT) project, using the B-Tool.
• BZ-Testing-Tools Project (in French and English).
• CADP . A comprehensive toolbox for the Construction and Analysis of Distributed Processes (1986-now).
• CoFI: The Common Framework Initiative for Algebraic Specification and Development. See CASL summary (Common Algebraic Specification Language), CoFI tools and CoFI Working Group information.
• Cogito 1 project, SVRC, Australia.
• CoLogNET European Network of Excellent on Computational Logic including formal methods.
• COMIC project.
• CONCUR2 project on concurrency.
• CONFER project.
• ConForm project (ESSI).
• Constructive Z project.
• Coq project on Software specifications and proofs. See also here.
• DEPLOY project on the Industrial deployment of system engineering methods providing high dependability and productivity. See also the FAQ on evidence about the use and the impact of formal engineering methods in Industry
• EP-ATR Project, IRISA, France. Design of embedded applications based on a synchronous computation model.
• ESPRESS project, Engineering of safety-critical embedded systems, Germany. (See also here.)
• Espresso Project, Environment for the Specification of Synchronous Reactive Programs, France. (In French.)
• EuroFORM project, investigating Formal Methods for Correct System Design (Human Capital and Mobility Project).
• FMEIndSem: Formal Methods Europe Industrial Seminars.
• FMEInfRes: Formal Methods Europe Information Resources. See the applications database. See also TCD and IFAD information.
• FM-Guides project - Guide Books and Videos for Managers on Formal Methods.
• FMnet - Formal Methods Network.
• FMOODS projects (Formal Methods for Open Object-Based Distributed Systems)
• Focus: A Design Methodology for Distributed Systems.
• Formal Description Techniques Project C1, University of Kaiserslautern, Germany.
• Formal Methods Europe projects.
• Formal verification support for ELLA project.
• formalWARE industry/university collaborative research project, Canada. See Separation Minima for Aircraft in the North Atlantic Region Formalization and Analysis of the Separation Minima for Aircraft in the North Atlantic Region.
• FORMAT project.
• FORTEST Network, UK. Formal methods and testing.
• GENeration ENvironment for Effective VErification (GENEVIEVE), IBM Research Lab, Haifa, Israel.
• Hawk: Specifying, Verifying, and Simulating Microprocessors.
• Hidden Algebra project.
• HISSA: High Integrity Software Systems Assurance Project.
• INSYDE project (INtegrated Methods for evolving SYstem DEsign).
• IPTES project.
• Isabelle projects.
• KeY project: Integrated Deductive Software Design.
• KeYmaera project: Hybrid Systems Design and Verification.
• KORSO project (1991–1994) on correct software (Germany).
• Logic Calculator Project.
• Logosphere project. A formal digital library, Department of Computer Science, Yale University, USA.
• LOMAPS project.
• MaFMeth project, using B-Tool and VDM-SL.
• ManTa project, Colombia. Abstract Datatype handler - tool and methodology.
• MATHS Project. See manifesto and samples of syntax description including a Z syntax.
• MATISSE project.
• Mizar Project, started about 1973. An attempt to reconstruct mathematical vernacular.
• MOBY project.
• MONA/FIDO Project.
• MULTIVAL: Industrial project on formal methods for high-performance multiprocessor and network-on-chip architectures (2006-2011)
• Mural project (1984–1988).
• NADA ESPRIT Working Group on New Hardware Design Methods.
• 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.
• OPUS project, developing a formal model for expressing the essential object-oriented features.
• OMI Software Architecture Forum (20858) including proof approaches
• `pobl' project on a development method for concurrent (object based) programs.
• ProCoS, Provably Correct Systems:
  • ProCoS I project (1989–1992).
  • ProCoS II project (1993–1995).
  • ProCoS-WG Working Group.
  • Provably Correct Hardware/Software Co-design.
• "Production Cell" Case Study — a number of different formal methods have been applied to a robot-based application. (See also here.)
• PROGRAIS project on Derivation of specifications and programs.
• PROSPECTRA project (1985–1990) on correct software (ESPRIT).
• PROSPER — Proof and Specification Assisted Design Environments (ESPRIT Framework IV LTR 262).
• RAISE projects.
• Rapide Project, Standford University, USA.
• 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).
• REACT project.
• Reasoning about non-ideal digital circuits — UK EPSRC project at University of Kent↑.
• RefineNet Network, UK. Refinement of formal specifications.
• ReForm project: From assembler to Z using formal transformations. See also A Proof Theory for Program Refinement and Equivalence: Extensions.
• RODIN Project: Rigorous Open Development Environment for Complex Systems.
• RTHS project (Real-Time and Hybrid Systems).
• RuleBase project, IBM Research Lab, Haifa, Israel. Model-checking tool including on-line demonstration.
• SafeFM Project on the practical application of Formal Methods to Safety-Critical Systems.
• safemos project (1989–1993) on Totally Verified Systems.
• SAFIR project on Algebraic formal systems for industry and research.
• SDRR Project on Software Design for Reliability and Reuse.
• SLAM Project on formal methods in the development process, Babel Group, Madrid, Spain.
• Software Engineering Projects, Software Engineering Group, Department of Computer Science, The University of Hong Kong. Object-oriented and formal methods.
• SPY Lab project. Static Program Analysis by Abstract Interpretation.
• SYNCHRONIE project on Synchronous Programming for Embedded Systems.
• Tatami Project: Kumo web-based proof assistant and BOBJ system for behavioural specification. See also here.
• Tools for TLA project.
• TOPCASED project: The Open-Source Toolkit for Critical Systems.
• TOPIC, RACE Project R2088, a Toolset for Protocol and Advanced Service Verification in IBC Environments, using formal methods and tools.
• UniForM project (Universal Formal Methods workbench), Germany.
• Utah Verifier (UV) Project: Formal Methods in System Design and Verification, Department of Computer Science, University of Utah↑, USA.
• VASY Team, INRIA Grenoble, France. Validation of Systems - CADP toolbox.
• Venari Project, CMU, USA. Specification and language support for transactions.
• VerifiCard Project: Smartcard verification
• VERIFIX project: provably correct compilers, University of Karlsruhe↑, Germany.
• Verisoft @ Munich, Technische Universität München, Germany.
• VHS Project: Verification of Hybrid Systems (ESPRIT-LTR Project 26270), VERIMAG, France.
• VSE and VSE-II Verification Support Environment projects, Germany. Provably Correct Software through Formal Program Development.
• VSR-net Network, UK. Verified Software Repository.

Other lists

• IFAD projects, IFAD, Denmark.
• Research projects on the application of formal description techniques (FDTs) including TLA.
• Research projects, SICS/KTH, Sweden.
• BRICS projects, Centre for Basic Research in Computer Science, Denmark.
• Manchester University Formal Methods Group projects, UK.

---

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.