SMT-based Verification of Timed Systems and Software

Roland Kindermann, M.Sc. (Tech.), will defend the dissertation "SMT-based Verification of Timed Systems and Software” on 9 December 2014 at 12 noon in lecture hall TU1, Otaniementie 17, Espoo. This dissertation studies novel methods for finding faults in hardware and software systems when timing aspects are of particular importance. The work focuses on the use of techniques from the area of computational logic, especially modern SMT solvers, in this setting.

In many areas, the failure of hardware or software can have grave consequences. Examples of such areas include medical systems, airplanes, spacecraft, and control systems of nuclear power plants. In such areas, mere testing does not give sufficient confidence in the correctness of a system, as has been shown by devastating failures of well tested systems, such as the Ariane V malfunction, leading to the rocket's detonation, the Pentium floating point division bug, leading to significant economic loss for the manufacturer, or an error in the Therac-25 radiation therapy machine leading to three casualties. Verification tries to address this issue by, unlike testing, not only checking the correctness of a system in a finite number of scenarios, but instead proving the correctness of the system in all possible scenarios, often in a fully automated process.

This thesis studies the verification of timed systems, i.e. verification in a setting where timing aspects of the verified system are accurately modeled. As a common theme, the verification techniques discussed in this dissertation use a symbolic, logic-based approach to verification and modern SMT solvers capable of supporting this approach.