Formal Methods Companies

Please mail J.P.Bowen@reading.ac.uk 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.
B-Core (UK) Limited, Oxford, UK.: B-Toolkit, based on the B-Tool. Contact Ib Sørensen on Ib.Sorensen@comlab.ox.ac.uk for further information.
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.
Computational Logic Inc., Austin, Texas, USA.: Nqthm and Pc-Nqthm theorem proving tools. Hardware verification including the FM9001 microprocessor.; Ceased 1997.
CRI, Denmark.: RAISE language and tools. Contact raise@csd.cri.dk for information.
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.: Contact Hans-Martin Hörcher on hmh@informatik.uni-kiel.d400.de.; Members of the ProCoS-WG Working Group.; Ceased trading in November 1996. All former employees now work for VST.
Escher Technologies, UK.: ESEL language and Escher Tool.
Formal Systems (Europe) Ltd., Oxford, UK.: Email mailto:postmaster@fsel.com. FDR tool for CSP model checking. Contact fdr-request@comlab.ox.ac.uk for further FDR information.
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.; See also other related organizations.
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.
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.: Products include Prover (a theorem prover for propositional logic extended with finite integer arithmetic) and NP-Tools (a framework for mathematically proving safety properties). Also known as Logikkonsult NP.
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.
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.
Time-Rover.: Temporal-Rover tool based on temporal logic.
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.