Our Software Verification Tools
A distinguishing feature of our software verification tools is accurate modeling of low-level artefacts, such as bit-vector semantics, memory models, and interfaces to hardware.
Our tools can check automatically generated properties such as array bounds (buffer overflows) and pointer safety, but also user-specified assertions. The typical application for our tools is the validation of embedded software. Read our survey paper.
- Front-end (parser) for C/C++: GOTO-CC
- Model Checkers for Boolean programs: BOPPO and BOOM
- 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