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.

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