Some Companies that Do or Did Verification-Related Things

Group Cohesion in Modern Verification-Oriented Companies, essay by Ruzica Piskac

NIST Case Study on Testing Infrastructure

Computational Logic, Inc.

Cedilla systems was a company doing proof carrying code.

Not too much info is available, they do not exist any more.

Intrinsa Corporation. Was using a kind of unsound static analysis that samples various program paths and creates summaries. Was bought by MSFT and Pincus remain to lead a very successful team developing tools Prefix and Prefast, widely used internally to detect software flaws.


  author = "William R. Bush and Jonathan D. Pincus and David J. Sielaff",
  title = "A static analyzer for finding dynamic programming errors",
  journal = SPE,
  volume = 30,
  number = 7,
  pages = "775-802",
  year = 2000


Kesterel Institute

Stayed around for a very long time.

Kestrel's funding agencies include DARPA, AFRL, ONR and NASA.

Galois Connection

Praxis High Integrity Systems around for a while, verifying absence of errors in Ada programs


Automatically finding bugs in C++ programs. Young and successful.


WCET analysis for embedded systems.

Polyspace, used abstract interepretation using polyhedra.

Recently acquired by Mathworks that make Matlab.

EADS - European Space Agancy Ongoing RichModelToolkit collaboration with them. They verify C code.

SRI - Rushby, Shankar, Tiwari

MSFT Many verification groups.

IBM specifically the groups including

Jana Kohler (IBM Zurich)

Eran Yahav (IBM Hawthorne)

Tata Consultancy Services (they opened a branch in ETHZ)

Significant and relevant research effort in finding software flaws.

More companies listed here, some of them do verification: