"Logical Methods in Automated Hardware and Software Verification";
TU Wien/Fakultät für Informatik,
Computer systems control the world - we have come to rely on the correctness of software and integrated circuits in safety-critical domains such as aviation and automotive engineering, as well as in communication, consumer electronics, and domestic appliances. Yet establishing the correctness of these systems is an ever more tedious and challenging task, which more often than not involves a significant manual effort.
Formal verification techniques such as model checking promise remedy in the form of fully automated tools that answer a range of questions about the system: does it behave as it is supposed to, or does it contain bugs buried deeply in the code? If the result is not as expected, exactly when and where did the system start to misbehave?
In practice, the scale of industrial software and hardware designs and the complexity of bugs severely limits the applicability of automated tools. Software components comprise thousands of lines of code; bugs (such as buffer overflows) may require hundreds of loop iterations to surface; and failing executions of integrated circuits can span millions of cycles.
The constituent publications of this habilitation thesis present novel techniques - centered around mathematical induction and Craig´s interpolation theorem - that push the scalability of automated verification to real-world problems. We combine the most competitive hardware model checking algorithms (which are based on inductive generalization and interpolation) with novel abstraction-refinement techniques to verify industrial-size software. We show how to uncover deep software bugs by collapsing millions of execution steps into a single step by solving recurrences. Using interpolation, we isolate faults in lengthy executions in post-silicon validation. Our novel adaptations of induction and interpolation methods are key to the development of scalable tools for automated verification, bug detection, and fault localization.
verification, logic, interpolation, model checking
Electronic version of the publication:
Created from the Publication Database of the Vienna University of Technology.