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.

• Bounded Model Checking for C/C++:
  

• Bounded Model Checking for Java:
  

• SAT-based Predicate Abstraction for C:
  

Relevant Publications

• 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