Embedded software verification: challenges and solutions

ABSTRACT

Embedded software are becoming more and more pervasive in our lives, and many application domains have very high reliability requirements. Ensuring high software quality while still maintaining software productivity is a challenging task. In order to address this challenge, more formal analysis and automated verification techniques are needed in addition to standard software testing.

In this tutorial, we will showcase the important ideas and techniques of software formal verification, including static program analysis, program modeling and (bounded) model checking, and predicate abstraction refinement. We will emphasize some of the key techniques that have been successfully adopted by recent, industrial-strength software verification tools. In this tutorial, we will focus on detecting bugs in sequential programs written in C/C++ for portable devices as well as for general purpose platforms.

The tutorial will be tailored to the ICCAD audience by emphasizing the use of decision procedures such as BDDs, Presburger arithmetic, bit-vector arithmetic, SAT and SMT solvers. Many of these techniques have been used in the context of analyzing, optimizing, and verifying IC designs.

By attending this tutorial, the audience will get a better understanding of the challenges and potential solutions of embedded software verification.