SAT-Solving and Software Bounded Model Checking: Trends and Applications

The area of software verification has seen renewed interest over the last years. New techniques like Satisfiability Modulo Theory or Software Bounded Model Checking (SBMC) have emerged and turned out to to be suitable to (semi-)automatically check a wide class of properties of real-world software of moderate to large size. Many of these tools rely on advances that have been made in SAT solving. In our talk we will, in a first part, summarize recent trends in SAT solving technology with a focus on parallel implementations. We will also report on the results of SAT-Race 2008, a SAT solver competition that for the first time also included parallel SAT solvers.

In the second part of the talk we present extensions we have implemented in the SBMC tool as well as case studies including Linux device driver verification, equivalence checking of cryptographic software, and functional property checking for automotive control software. We will also comment on strengths and remaining shortcomings of existing verification tools.