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, floating-point arithmetic, 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.

Relevant Publications