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

NIST Case Study on Testing Infrastructure

Computational Logic, Inc.

http://www.computationallogic.com/

Cedilla systems was a company doing proof carrying code.

http://www.linkedin.com/in/chriscolby http://raw.cs.berkeley.edu/pcc.html

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.

@Article{BushETAL00StaticAnalyzerPincus,

  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.

http://www.kestrel.edu/

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

Galois Connection

http://www.galois.com/ http://www.galois.com/company/people

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

http://www.praxis-his.com/

Coverity

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

http://www.coverity.com/

AbsInt

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:

http://computer.euro-companies.com/