Repositories

Virtual Library

---

Software Engineering

---

Formal Methods

Formal Methods Repositories

Please add or correct links to formal methods on this page. Alternatively, please contact Jonathan Bowen if you know of relevant online information not included here or would like to maintain information on a particular topic.

---

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

---

• Formal Methods and Dependable Systems program, SRI CSL, California, USA.
• NASA Langley formal methods program, USA. See general information on formal methods.
• NASA Software Engineering Laboratory, Goddard Space Flight Center, Greenbelt, Maryland, USA.
• 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.
• 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.
• The Foundations & Methods Group, Department of Computer Science, Trinity College Dublin, Ireland.
• At INRIA in France there several research teams on formal methods, among which COQ project on Software specifications and proofs, PROGRAIS project on Derivation of specifications and programs, SAFIR project on Algebraic formal systems for industry and research, and VASY project on ``Validation of Systems .
• 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.
• Formal Methods and Tools (FMT) group, 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 Verification group, School of Computing, University of Utah
• 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 Analysis, Theory and Algorithms Research Group (FATA), Department of Computing Science, Glasgow University, Scotland.
• Research projects on the application of formal description techniques (FDTs) including TLA by the Computer Networks and Distributed Systems Group, 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.
• 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.
• Formal Methods Group, University of Karlsruhe↑, Germany. (Now dispersed!)
• Formal Design Techniques Group, SICS↑/KTH↑, Sweden.
• Formal Methods pointers from Yahoo↑.
• [1]
• 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.
• IFAD, Denmark. An independent non-profit organization specializing in technology transfer, including formal methods, especially VDM and its extensions.
• Formal Methods Group, Eindhoven University, The Netherlands.
• 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.
• Centre for Concurrent Systems and VLSI, Faculty of BCIM, London South Bank University, 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 and Formal Methods in Human Computer Interaction 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.
• Verification and Testing 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. See also Theoretical Computer Science and Formal Methods.
• 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, Moffett Field, California, USA.
• 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.
• Verification Automation Laboratory, Institute of Information Science, Academia Sinica, Nankang, Taipei, Taiwan.
• 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, UK. Courses, including formal specification.
• Centre for Applied Formal Methods, Systems and Software Engineering research group, Faculty of BCIM, London South Bank University, UK. The Virtual Library formal methods pages are now located here.
• Formal Methods Group, Software Research and Development Center (SRDC), Middle East Technical University (METU), Turkey. (Disbanded.)
• ERCIM Working Group on Formal Methods for Industrial Critical Systems (FMICS).
• Foundations of Software Engineering Group, Microsoft Research, Redmond, USA.
• Formal Methods Laboratory University of Waikato, Hamilton, New Zealand.
• Centre for Formal Design & Verification of Software, Indian Institute of Technology, Bombay, Mumbai, India.
• Software Engineering Group and Group of Logic and Computation, King's College London, UK.
• Logic and Formal Methods Group, University of Minho, Portugal.
• Formal Methods Group, University of Verona, Italy.
• Applied Formal Methods Research Group, Stirling University, Scotland, UK.
• Logic and Computation Group, Department of Computer Science, University of Liverpool, UK. See research on Formal Software Development.
• Theory and Practice of Programming (TaPP) research group, Department of Computer Science, The University of Warwick, UK.
• Software Technology and Software Engineering (STSE) research group, The Open University, UK.
• Formal Methods && Tools Group, Istituto di Elaborazione della Informazione, National Research Council (CNR), Pisa, Italy.
• Open Systems Laboratory, Department of Computer Science, University of Illinois at Urbana-Champaign (UIUC), USA.
• Laboratory for Logic, Tel-Aviv University, Israel. Covers the study of applications of mathematical logic to computer science.
• Applied Formal Methods Research Group, Department of Computing, School of Technology, Oxford Brookes University, UK.
• Applied Formal Methods Group, School of Computing, Queen's University, Kingston, Ontario, Canada.
• Formal Methods Group, University of Toronto, Ontario, Canada.
• Mechanized Reasoning Group, Université di Genova, Italy.
• TRain: The Railway Domain. Formal specification and verification techniques.
• QPQ ("QED Pro Quo"). An open source repository for deductive software components. Provides an online journal for publishing peer-reviewed source code.
• Mizar. An attempt to reconstruct mathematical vernacular. See also Mizar Project and Mizar System tool.
• South-East European Network on Formal Methods (SEEFM).
• Logical Systems Lab, Carnegie Mellon University, Pittsburgh, USA.

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.
• Software Specification Methods: An Overview Using a Case Study edited by Marc Frappier and Henri Habrias. A study of the process of producing a formal specification using different notations and a common case study.

Search for formal methods by Google.

---

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