Formal Methods Companies

Please contact Jonathan Bowen if you know of relevant on-line information not included here, would like to maintain information for a particular company, or have any corrections.

This document contains some pointers to companies with some interest in formal methods, most of which provide on-line access to information on the World Wide Web.

Abstract Hardware Limited, Uxbridge, Middlesex, UK.: Products including the LAMBDA system synthesis tool set and PolyML, a commercially supported version of Standard ML. Services include training courses and consultancy.; Now ceased operation.
Adelard, London, UK.: Consultancy in the areas of: development, verification and assessment; safety cases; standards and guidelines; training and technology transfer.
ATX Software, Portugal.: Coordination Development Environment (CDE) tool.
B-Core (UK) Limited, Oxford, UK.: B-Toolkit, based on the B-Tool.
Bell Labs, New Jersey, USA.: Part of Lucent Technologies.; Bell Labs Design Automation have produced the FormalCheck tool for verifying the functionality of ASIC and digital IC designs in Verilog or VHDL, based on the COSPAN model checker.
BT Laboratories, Martlesham, Ipswich, UK.: Formal Methods Group. Contact Elspeth Cusack on elc@fmg.bt.co.uk for further information.
Cap Gemini, Utrecht, The Netherlands. (Was Cap Volmac.): VDM++ language and tools. Afrodite project. Contact Nico Plat on Nico.Plat@ACM.org.
Chrysalis Symbolic Design, Inc., North Billerica, MA, USA.: Produces software for creating and verifying electronic circuits and systems. Products include Symbolic Logic (tm) technology to help with formal verification.
ClearSy System Engineering, Aix-en-Provence & Paris, France.: Maintainer of Atelier B tool and consulting based on B-Method. Special consultant: J.-R. Abrial. (In French.)
Computational Logic Inc., Austin, Texas, USA.: Nqthm and Pc-Nqthm theorem proving tools. Hardware verification including the FM9001 microprocessor.; Ceased 1997.
Daimler-Benz Research, Berlin, Germany.: Local organizers and sponsors of ZUM'98, Berlin, September 1998.
Danish State Railways (DSB), Denmark.: Members of the ProCoS-WG Working Group. Contact Kirsten Mark Hansen on kmh@id.dth.dk.
Digilog, France.: Atelier B tool supporting the B-Method. Contact Francois Bustany on digilog@dialup.francenet.fr.
DST (Deutsche System-Technik GmbH), Kiel, Germany.: Members of the ProCoS-WG Working Group.; Ceased trading in November 1996. All former employees now work for VST.
Escher Technologies, UK.: Perfect Developer tool.
Esterel Technologies, France.: Esterel Studio tool for verification and validation, based on the Esterel language.
Formal Systems (Europe) Ltd., Oxford, UK.: CSP software including FDR2 model checker.; Email enquiries@fsel.com.; See also earlier FDR tool for CSP model checking. Contact fdr-request@comlab.ox.ac.uk.
GEC Alsthom, Paris, France.: Users of the B-Tool.; Members of the ProCoS-WG Working Group.; Contact Babak Dehbonei or Fernando Mejia on fax: +33 (1) 40 10 65 00 (no email!).
Harlequin, Australia / UK / USA.: Consultancy including formal software engineering and reasoning systems.
Headway Software, Calgary, Canada.: Consultancy. Formal modelling using Z, VDM, UML, etc. Rose Formaliser Link (Z and UML).
IBM United Kingdom Laboratories, Hursley Park, UK.: See 1992 Queen's Award for work on CICS. See also IBM's Cleanroom Software Technology Center, Clear Lake, Texas USA.
ICL, UK.: Original developer of ProofPower, a tool based on HOL for proofs about Z specifications.
IFAD, Odense, Denmark.: Products include VDMTools supporting VDM-SL and VDM++.; Consultancy, training and technology transfer of VDM.; VDM repository.; Members of the ProCoS-WG Working Group.
Industrilogik L4i AB, Stockholm, Sweden.: Safety and quality using formal methods. Consultancy, R&D.
Inmos, Bristol, UK.: Now SGS-Thomson Microelectronics.; See 1990 Queen's Award for work on the T800 transputer.; See also PACT (Partnership in Advanced Computing Technologies), occam programming language and safemos project.
IST (Imperial Software Technology Ltd), Reading, UK. (Also Cambridge, London, and Palo Alto, USA.): Software engineering company, including an Advanced Technology Group specializing in the application of formal methods for high-integrity and secure systems.; Products include Zola, an integrated editor, type-checker and prover for the Z notation.
Kestrel Institute, California, USA.: Undertakes research in applying formal methods and automated reasoning systems to software engineering.
K&M Technologies Limited, Dublin, Ireland.: Industrial exploitation of the Irish School of the VDM, etc.
Lemma 1 Ltd., Reading, UK.: Founded 1997.; Consultancy company run by Rob Arthan, previously at ICL.; Co-located with InterGlossa Ltd.; Experience of the ProofPower tool for Z proofs.
Lloyds Register, Croydon, UK.: Members of the B User Trials project.; Members of the ProCoS-WG Working Group.; Members of the REDO project.
Logica UK Limited.: Formal methods tools and services, including the Formaliser Z type-checker. Contact Susan Stepney on stepneys@logica.com for further information.
Logikkonsult NP AB, Sweden.: See Prover Technology.
Mentor Graphics Corporation, Wilsonville, Oregon, USA.: Hardware system design and verification.; formal verification equivalency checker for multi-million gate ASIC and SoC (system-on-a-chip) verification.; Seamless hardware/software co-verification.
National Physical Laboratory (NPL), UK.: Market Prover from Prover Technology.; Members of the ProCoS-WG Working Group.
ORA, Ottawa, Canada.: EVES tool.
Philips GmbH Forschungslaboratorien, Aachen, Germany.: Members of the ProCoS-WG Working Group.
Praxis Critical Systems, Bath, UK.: Separated from Praxis in April 1997. Skills in formal specification, static analysis, safety engineering.; Products include SPARK language and tool support for program verification.; Contact Anthony Hall on jah@praxis-cs.co.uk for formal methods course information.; Contact Amanda Kingscote on ark@praxis-cs.co.uk to join the Z postal mailing list.; Members of the ProCoS-WG Working Group. Contact Trevor King on trevor@praxis-cs.co.uk.
Program Validation Limited, UK.: Now Praxis Critical Systems.; Members of the B User Trials project.
Prover Technology, Sweden.: See proof engine products. Previously known as Logikkonsult NP.
Reactive Systems, Inc., USA.: Model checking.
Research Access Inc., USA.: Specification and verification documents.
Rolls Royce & Associates, Derby, UK.: Use VDM.
RWTÜV Anlagentechnik, Germany.: Members of the ProCoS-WG Working Group.
Safet, Buenos Aires, Argentina.: Safe software technologies, including verification.
SoftwareIntegrity, Inc., USA.: SoftwareExcelaration methodology.
SRI, Menlo Park, California, USA. Also, Cambridge, UK.: Formal methods information and PVS tool.
Telelogic AB, Malm, Sweden.: Products include SDT, a software engineering toolset based on SDL, and the ITEX test suite tool.
Terma A/S, denmark.: Provider and user of RAISE (Rigorous Approach to Industrial Software Engineering).
Time-Rover.: Temporal-Rover tool based on temporal logic.
Transitive Technologies, Manchester, UK & San Diego, USA.: Uses formal methods "light" for optizing dynamic binary translation technology.
Contact John Fitzgerald on johnf@transitives.com for formal methods aspects.
Verified System International GmbH, Bremen, Germany.: FDR model-checker and RT-Tester tools. (Information in German.)
Verilog, USA.: See also France. Products include the ObjectGEODE toolset, based on the OMT, SDL and MSC standards notations, dedicated to analysis, design, verification and validation through simulation, code generation and testing of real-time and distributed applications.
Verplex Systems, Inc., USA.: Formal verification and logical equivalence checking products for ASIC and IC applications, including the Tuxedo-LEC^TM tool.; See Verify99 seminar information.
Vossloh System-Technik GmbH (VST), Germany: Daughter company of the Vossloh AG.; Active in traffic sector (mainly railway).; Former employees or DST now work for VST.; Contact Hans-Martin Hörcher, Vossloh System-Technik GmbH Edisonstr. 3, 24147 Kiel (tel: +49-431-7109-539, fax: -502, email: hoercher@vst.vossloh.de).
WetStone Technologies, Inc., USA.: Information security.; See formal methods questionnaire.
York Software Engineering Ltd (YSE), UK: See products, including CADiZ Z type-checker;
Subsidiary of CSE.