Virtual Library Software Engineering Formal Methods

This document contains some pointers to on-line repositories of information concerned with formal methods, including research groups, which provide access on the World Wide Web.

• Information on formal methods and dependable systems at SRI CSL, California, USA.
• NASA Langley formal methods program including general information on formal methods. An overview of the programme with a good selection of references is available. There is an associated electronic mailing list. Email info+fm-request@LaRC.NASA.GOV or click here to join.
• An International Survey of Industrial Applications of Formal Methods by D. Craigen, S. Gerhart and T.J. Ralston, in two parts, Volume 1 on Purpose, Approach, Analysis and Conclusions (also in an alternative shorter version) and Volume 2 on Case Studies. Glimpse searching is available.
• Kestrel Institute, California, USA. A research and development organization, applies knowledge-based formal methods to software engineering problems. Current projects include algorithm synthesis, software testing, reactive systems design and verification, data type refinement, visualization synthesis and high-level specification.
• Laboratory for Applied Logic (research unit), Department of Computer Science, College of Engineering, University of Idaho, USA. Goal: making formal modeling and analysis of computer systems tractable for software and hardware design engineers.
• Pointers to Formal Methods sites and course information on computer systems verification are available from the BYU Laboratory for Applied Logic.
• Formal Methods (Working) Group at the Department of Computer Science, Trinity College Dublin, Ireland.
• At INRIA in France the following projects related to aspects of formal methods are underway: COQ project on Software specifications and proofs, PROGRAIS project on Derivation of specifications and programs and SAFIR project on Algebraic formal systems for industry and research.
• Research Grants in formal methods and provably correct systems at the Oxford University Computing Laboratory, UK. E.g., see the ESPRIT Basic Research ProCoS project and Working Group. See also the ESPRIT II REDO project (1989-1992) which investigated formal methods for reverse engineering in software maintenance, and the IED safemos project (1989-1993).
• EuroFORM Human Capital and Mobility Project, Madrid and elsewhere. Investigating Formal Methods for Correct System Design.
• Object Oriented Data Models (OODM) project. Centered around a formal object-oriented database specification language TM is being undertaken by the Information Systems Workgroup at the University of Twente, the Netherlands.
• Formal Methods Research and pointers to semantics based program analysis and manipulation, School of Computer Science, Carnegie Mellon University, USA.
• Formal Methods Section, Center for High Assurance Computer Systems, Information Technology Division, Naval Research Laboratory, Washington DC, USA, conducts interdisciplinary research and development in techniques for processing and communicating data that preserve critical system properties such as security. Improved formal methods for analyzing and developing software and hardware systems are a primary research focus.
• HOP Calculus, CUI Object Systems Group. Provides a basic framework for modelling object-oriented constructs.
• Formal methods information is available from EINet Galaxy.
• A database of automated reaoning systems (including a README file and individual entries) is held at Stanford University.
• Formal Methods and Analysis Research Group (FDA) at Department of Computing Science, Glasgow University, Scotland.
• Software Engineering Group at the Department for Computation and Information, Rutherford Appleton Laboratory, UK.
• Research projects on the application of formal description techniques (FDTs) including TLA by the Computer Networks and Distributed Systems Group at the University of Dortmund, Germany.
• Systematic Program Development Group at MIT interested in the timely development of high-quality software and hardware through the practical application of formal methods, and Larch in particular. See recent publications.
• IEEE CS Technical Segment Committee on Engineering of Complex Computer Systems announcement and other information including the latest newsletter. To subscribe to the newsletter, email ieee-tsc-eccs-request@cl.cam.ac.uk.
• Formal Methods Group, Department of Computer Science, Manchester University, UK. See projects.
• Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh. Includes research on the formal development of programs and systems.
• Andrew Gordon's Web monitor page including many formal methods links.
• Formal methods for high assurance concurrent software from the Experimental Computation Laboratory at the University of Missouri - Rolla, USA.
• Hardware Verification Group, University of Karlsruhe, Germany. Conducts research in various aspects of formal hardware verification, including transistor-level verification, VHDL-based verification and formal synthesis.
• Formal Design Techniques group, SICS/KTH, Sweden. Research projects include COMIC, CONCUR2, CONFER and LOMAPS.
• A list of "formal" languages from the language list.
• Formal Methods pointers from Yahoo.
• NCITS/J21 (formerly X3J21) Technical Committee on Formal Specification Languages (FSLs) including VDM and Z, from the Software Engineering Institute, Carnegie-Mellon University, Pittsburgh, USA. See also official NCTIS/J21 Technical Committee information directly from the National Committee for Information Technology Standards (NCITS), USA.
• Software Verification & Testing and Software Specification abstracts from Research Access.
• QED proposal (including a manifesto) to cooperatively create a public-domain database of formalised mathematics, with machine-checked proofs. Email majordomo@mcs.anl.gov with a message containing the single line "subscribe qed" to join the mailing list.
• IFAD is an independent non-profit organization which specializes in transferring new technologies such as formal methods to industrial use, for VDM and its extensions in particular.
• Research by the Formal Methods Group, Eindhoven University.
• ESPRIT Basic Research: 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), 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 and ProCoS-WG (Provably Correct Systems), REACT-P (Building Correct Reactive Systems).
• Workbook: New Mathematical Foundations for Computer Science Edition 1: Post-IMACS, On-line Conference.
• Search for formal methods by Web Crawler.
• Software Engineering Research Group (SERG), Michigan State University, USA. Involved in a number of research projects developing techniques and tools to support the use of formal methods for software development.
• Research on the formal foundations of object-orientation by the formal methods group at the Programming Technology Laboratory, Department of Computer Science, Brussels Free University, Belgium.
• Center for High Integrity Software Systems Assurance (CHISSA), NIST, USA. Includes a Call For White Papers.
• Formal Methods at Cornell, USA.
• PSP Group (Programs, Specifications and Proofs) and Automated Theorem Proving Group University of Texas at Austin, USA.
• Theory and Semantics Group, Automated Reasoning Group and Action Calculi at the University of Cambridge Computer Laboratory, UK.
• Generation of Interactive Programming Environments (GIPE), CWI and University of Amsterdam, Netherlands. A meta-environment for generating language-specific environments from algebraic specifications of (programming) languages.
• Design Group, Department of Information Technology, Technical University of Denmark. Research on dedicated hardware/software systems including hardware verification.
• Formal Verification research, Computer Systems Section, Department of Information Technology, Technical University of Denmark.
• Software Systems Section, Department of Information Technology, Technical University of Denmark.
• Software Systems Section, Department of Computer Science, Technical University of Denmark. See Formal Software Specification course.
• Formal Methods for Software Maintenance projects, Centre for Software Maintenance, Department of Computer Science, University of Durham, UK.
• Systems Integrity Research, DRA Malvern, UK.
• Tele-Informatics and Open Systems (TIOS) Formal Methods Group, University of Twente, The Netherlands.
• Automated reasoning at Argonne National Laboratory, Illinois, USA.
• PacSoft: Pacific Software Research Center, Oregon Graduate Institute of Science & Technology, USA. A group researching into the design, implementation and maintenance of software systems, including the use of formal methods.
• Programming Language Semantics Research at Kansas State University, USA.
• Formal Methods Group, Department of Computer Science, Royal Holloway, University of London, UK.
• Formal Program Development in New Zealand.
• Software engineering and formal methods, School of Computer Science, University of Birmingham, UK.
• Formal Methods research, Centre for Systems and Software Engineering (CSSE), South Bank University, London, UK.
• Centre for Concurrent Systems and VLSI, School of Computing, Information Systems and Mathematics, South Bank University, London, UK.
• Asynchronous Logic Home Page, Manchester, UK.
• Formal Methods and Software Engineering Group, including the Formal Methods Group, Department of Computer Science, University of Reading, UK. Research into concurrent, real-time, safety-critical systems, and hardware compilation.
• INFORM: Institute for Formal Methods in Software Engineering, including research information, Department of Computer Science, Universität Bremen, Germany.
• Programming Methodology Group, Department of Computer Science, Technical University of Eindhoven, The Netherlands.
• Formal Methods at Bell Laboratories, Murray Hill, New Jersey, USA. Includes SPIN information.
• Logic and Foundations of Programming (LFP) research group, Department of Computer Science, Queen Mary and Westfield College, University of London, UK.
• Formal Methods Group, Department of Computer Studies, Loughborough University, UK. Includes the BCS-FACS home page.
• Irish Formal Methods Special Interest Group, Ireland.
• Formal Methods Europe: Information Resources (FMEInfRes) including Applications Database and Tools Database.
• Verification Methods and Tools from the VERIMAG research group, France.
• Verification Algorithm Research Group, Software Systems Laboratory, Department of Information Technology, Tampere University of Technology, Finland.
• Modeling of Concurrency, including verification techniques, Department of Computer Science, University of Helsinki, Finland.
• Software Engineering Group, Department of Computer Science, The University of Hong Kong.
• Concurrent and Real-Time Systems Group, Department of Computer Science, University of Adelaide, Australia. Research in formal methods and automated verification of concurrent and real-time systems, communication networks, real-time communication protocols, asynchronous design methodolgies.
• Software Verification Research Centre (SVRC), Department of Computer Science, University of Queensland, Australia. See current R&D information.
• Formal Methods information from Roger Jones' Web Space.
• Concurrency and real-time systems group, CWI and University of Amsterdam, Netherlands.
• Stanford University research: Formal Reasoning Group; Hardware Verification Group; Program Analysis and Verification Group.
• Methods Integration Research Group, Florida Atlantic University, USA. Using formal methods with informal object-oriented and structured methods.
• Semantics of Computation Group, University of California, San Diego, USA. Includes information on OBJ languages.
• Theoretical Computing Group, University of Kent at Canterbury, UK. Functional / logic programming and the application of formal methods to distributed systems development.
• Software Engineering Research Group, Communications Reserach Laboratory McMaster University, Hamilton, Ontario, Canada. Led by Prof. David Parnas.
• Equipe MSF : Génie Logiciel, Méthodes et Spécifications Formelles, University of Nantes, France. (In French.)
• Data Security Group, NPL, UK. Security-related areas, from specification through to testing, including formal specifications.
• Formal Methods Research Group, Department of Computing, University of Bradford, UK.
• High Integrity Systems Engineering Group, Department of Computer Science, University of York, UK.
• Formal Methods Research Group, Institute of Software Engineering, School of Computer Science, Telecommunications and Information Systems, DePaul University, USA.
• Glasgow Interactive Systems Group (GIST), including the Glasgow Accident Analysis Group, University of Glasgow, UK. Developing new means of generating accident reports using formal methods such as Z and temporal logic.
• Correct Systems Research Group, Department of Computer Science, The University of Sheffield, UK.
• VASY (Validation of systems), INRIA Rhone-Alpes, France. A research initiative in the area of formal methods applied to industrial-size problems. See in particular CADP (CAESAR/ALDEBARAN Development Package), a protocol engineering toolbox for LOTOS.
• Software Engineering Group, Department of Computer Science, University of Melbourne, Australia.
• Software Engineering Department, FZI, Germany.
• Formal methods standards from ISO.
• Formal Specification and Verification for digital hardware and safety-critical systems, Advanced Computing Research Centre, School of Computer and Information Science, University of South Australia.
• Real-Time Systems Group, University of Pennsylvania, USA. See Algebra of Communicating Shared Resources (ACSR) and Graphical Communicating Shared Resources (GCSR), a formal language for the specification, refinement, and analysis of real-time systems. See the tools VERSA (Verification Execution and Rewrite System for ACSR) and PARAGON for visual specification and verification of real-time systems.
• MEIJE research team, INRIA and the Ecole des Mines de Paris. Investigates concurrency, synchronisation and reactivity. See Esterel language and verification tools.
• Machine-Assisted Proof and Formal Methods Research Group, Middlesex University, London, UK.
• Software Technology Research Laboratory (STRL), De Montfort University, Leicester, UK. Set up to study, analyse and advance formal approaches to the specification, design and the re-engineering of mixed computing systems, especially (distributed) real-time safety-critical applications.
• The Database Group, Technische Universität Braunschweig, Germany.
• Logic and Formal Methods Group, Department of Computer Science, University of Essex, UK.
• Programming Methodology Group, Department of Computer Science, Åbo Akademi University, Finland. Part of the Turku Centre for Computer Science (TUCS).
• Verification Support Environment (VSE), Formal Methods Group, DFKI German Center for Artificial Intelligence, Germany.
• Formal Methods in India home page.
• SCOP Group LSR Laboratory, France. Software specification and program development.
• Software Engineering research, Department of Computing, University of Surrey, UK. Formal, mathematically based approaches to the modelling, analysis and design of complex systems.
• Theory and Formal Methods Group, Department of Computing, Imperial College, UK. See Logic and Automated Reasoning Section. See also SLURP group (Sound Languages Underpin Reliable Programming), investigating the semantics of Java.
• Automated Software Engineering Group, NASA Ames Research Center.
• Formal methods in HCI, maintained by Alan Dix.
• A Specification Pattern System, property specification for finite-state verification, maintained by Matthew Dwyer.
• Object COMX, a design methodology based on the formal specification technique of communicating X-machines, maintained by Judith Barnard.
• ManTa Abstract Datatype handler - tool and methodology.
• Dependable System Architecture Group, SRI Computer Science Laboratory, California, USA. See Structural Architecture Description Language (SADL) allowing formal analysis.
• Computer-Assisted Reasoning Group, Department of Computer Science, University of Durham, UK. See the AORTA toolset for computer support of formal real-time system code generation and model-checking.
• Formal Specification and Verification of Real-Time Systems, Institute of Information Science, Academia Sinica, Nankang, Taipei, Taiwan. See State Graph Manipulator (SGM), a high-level real-time concurrent system specification and verification tool.
• NASA Formal Methods Page, USA.
• Formal Methods for Aviation Safety, ICASE, USA. (Associated with NASA.)
• TVS (Transformation, Verification and Simulation), a toolset under construction for formal verification and simulation of real-time systems. Under development at Department of Technical Mathematics and Informatics, Delft University of Technology, Tha Netherlands,
• Verification Technologies Group, including a Formal Methods Group, IBM Research Lab, Haifa, Israel.
• Software Technology, Christian-Albrechts-University of Kiel, Germany.
• Minerva Center for Verification of Reactive Systems, Faculty of Mathematics and Computer Science, The Weizmann Institute of Science, Rehovot, Israel.
• Software Engineering Programme, Oxford University. Courses, including formal specification.
• Centre for Applied Formal Methods, School of Computing, Information Systems and Mathematics (SCISM), South Bank University, London, UK.

For comparative case studies, see:

• "Production Cell" Case Study - a number of different formal methods have been applied to a robot-based application.
• Steam Boiler Control Specification Problem by J.-R. Abrial, E. Börger and H. Langmaack. A comparative case study for different formal techniques.

Search for formal methods by Lycos.

Part of the OUCL archive.