Software Verification

Our Software Verification Tools

A distinguishing feature of our software verification tools is accurate modeling of low-level arte­facts, such as bit-vector semantics, memory models, and interfaces to hardware.

Our tools can check automatically generated properties such as array bounds (buffer over­flows) and pointer safety, but also user-specified assertions. The typical application for our tools is the validation of embedded software. Read our survey paper.

• Bounded Model Checking for C/C++:
  

• SAT-based Predicate Abstraction for C/C++:
  

• Front-end (parser) for C/C++: GOTO-CC
• Model Checkers for Boolean programs: BOPPO and BOOM

Benchmarks

We have a collection of software-verification benchmarks available for download. We also main­tain a repository of sequential and concurrent Boolean Programs.

Relevant Publications

• New: Symbolic Counter Abstraction for Concurrent Software
• Race Analysis for SystemC using Model Checking
• Deciding Bit-Vector Arithmetic with Abstraction
• Counterexamples with Loops for Predicate Abstraction (Journal Version)
• Approximating Predicate Images for Bit-Vector Logic