Virtual Library Software Engineering Formal Methods

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

• Individual projects
• ESPRIT synopses
• Other lists

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.
• 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.
• COMIC project.
• CONCUR2 project on concurrency.
• CONFER project.
• ConForm project (ESSI).
• Constructive Z project.
• Coq project on Software specifications and proofs. See also here.
• 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.)
• 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.
• 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.
• 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.
• KORSO project (1991-1994) on correct software (Germany).
• Logic Calculator Project.
• 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.
• MOBY project.
• MONA/FIDO Project.
• Mural project (1984-1988).
• ESPRIT Working Group on New Hardware Design Methods.
• OODM project (Object Oriented Data Models) centered around a formal object-oriented database specification language TM.
• 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.
• OSAF OMI Software Architecture Forum (20858) including proof approaches
• `pobl' project on a development method for concurrent (object based) programs.
• ProCoS, Provably Correct Systems (also here - ESPRIT Basic Research):
  • 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 Kent.
• ReForm project: From assembler to Z using formal transformations. See also A Proof Theory for Program Refinement and Equivalence: Extensions.
• 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.
• Software Engineering Projects, Software Engineering Group, Department of Computer Science, The University of Hong King. Object-oriented and formal methods.
• SYNCHRONIE project on Synchronous Programming for Embedded Systems.
• Tools for TLA project.
• 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.
• VERIFIX project: provably correct compilers, University of Karlsruhe, 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.

ESPRIT Basic Research synopses

• CHARME (Correct Hardware and System-Level Design Methodologies)
• CHARME-2 (Formal Design and Correctness Verification of Synchronous and Asynchronous Digital VLSI Systems)
• COMPASS (A Comprehensive Algebraic Approach to System Specification and Development) see also Working Group information
• CONCUR 2 (Calculi and Algebras of Concurrency: Extensions, Tools and Applications)
• IS-CORE (Information Systems: Correctness and Reusability)
• NADA (New Hardware Design Methods)
• ProCoS II (Provably Correct Systems - project)
• ProCoS-WG (Provably Correct Systems - Working Group)
• Quest project
• REACT-P (Building Correct Reactive Systems)
• Venari Project, CMU. Specification and language support for transactions.

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.

Part of the OUCL archive.