Some Companies that Do or Did Verification-Related Things
Group Cohesion in Modern Verification-Oriented Companies, essay by Ruzica Piskac
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
Stayed around for a very long time.
Kestrel's funding agencies include DARPA, AFRL, ONR and NASA.
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: