Our Software Verification Tools
A distinguishing feature of our software verification tools is accurate modeling of low-level artefacts, 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 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.
- JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode
- Model Checking Boot Code from AWS Data Centers
- Verification of Tree-Based Hierarchical Read-Copy Update in the Linux Kernel
- Program Synthesis for Program Analysis
- Effective Verification for Low-Level Software with Competing Interrupts
- Bit-Precise Procedure-Modular Termination Analysis
- Modular Demand-Driven Analysis of Semantic Difference for Program Versions
- Abstract Interpretation with Unfoldings