Research

Formal Verification of Hardware Systems

SymC - A symbolic bounded property checker from University of Tübingen, Germany
RAVEN - Real-Time Analysis and Verification Environment from University of Tübingen, Germany
VIS - A system for verification and synthesis from University of Colorado at Boulder, USA
NuSMV - A Symbolic model checker from ITC-irst, Italy
Verus - A Compiler/Verifier for real-time systems from Carnegie Mellon University, USA
KRONOS - A verifier for real time systems from Verimag research center, France
ABC - A system for sequential synthesis and verification, Berkley logic synthesis and verification group, USA

Spin (Simple Promela (Process Meta Language) Interpreter) - An explicit state on-the-fly, LTL model checker from Bell Labs, USA

Inspect - A Runtime Model Checker for Multithreaded C Programs from University of Utah, USA

Collection of software bugs at Gesellschaft für Schwerionenforschung mbH, Darmstadt, Germany
Collection of software bugs at University of Munich, Germany
For latest software bugs and risks at Forum on Risks to the Public in Computers and Related Systems from ACM Committee on Computers and Public Policy, UK
History's Worst Software Bugs published at www.wired.com
Software Engineering Disasters published at Wikipedia.org

F-Soft - A software verification tool from NEC Labs, USA

BLAST - Berkeley Lazy Abstraction Software Verification Tool from EPFL, Lausanne, Switzerland

C32SAT - C boolean expression checker from Johannes Kepler University, Linz, Austria

PICOSAT - A solver for boolean formula in the DIMACS (Example) format from Johannes Kepler University, Linz, Austria.

CBMC - Bounded Model Checking for ANSI-C from Carnegie Mellon University, USA

SATABS - A verification tool for ANSI-C and C++ programs from ETH Zürich, Switzerland

Quantor - A solver for quantified boolean formula (QBF) in the QDIMACS (Example) format from Johannes Kepler University, Linz, Austria.

CCured - A source-to-source translator for C from Berkeley Labs, USA

MOPED - A model checker for push down systems from University of Stuttgart, Germany

Modex and FeaVer - A high level verification model extractor from concurrent C programs from Bell Labs, USA

SLAM - A Static driver verifier from Microsoft, USA

mygcc - An extensible version of the GNU C compiler that has static analysis capabilities
Polyspace - A commercial tool from The Mathworks
Splint - A tool for statically checking C programs from University of Virginia
FlexLint/PC-Lint Tools from Gimpel
coverity Prevent - A commercial tool from Coverity
Other static analysis tools