CS Colloquium - Jaco van de Pol: Automated Verification: can Brute Force be Smart?
The digital society, including our personal life, depends increasingly on software. Software errors are annoying, hinder productivity, screw up our security, and even lead to loss of lives in the case of safety-critical systems. Why is not all software formally verified?
Info about event
Time
Location
Building 5335, room 016 (Peter Bøgh Auditorium)
Abstract
The digital society, including our personal life, depends increasingly on software. Software errors are annoying, hinder productivity, screw up our security, and even lead to loss of lives in the case of safety-critical systems. Why is not all software formally verified?
We will review the current status of automated verification techniques, in particular model checking. This is an exhaustive procedure to automatically check temporal requirements on finite (abstractions of) systems. The main bottleneck is the complexity and state space explosion of the systems under investigation. This is typically addressed with clever algorithms and logical reasoning. My own line of research in the last 10 years has been to design parallel algorithms to speed up model checking. This brute force approach can only be successful if it includes the clever techniques mitigating the state space explosion. I will demonstrate some of the fundamental difficulties, and show a number of breakthroughs in LTL model checking and symbolic model checking.
Finally, I will mention some challenges ahead: it would be great to complement parallel analysis algorithms with high-performance synthesis. This requires parallel algorithms for solving games and computing strategies, as well as dealing with numerical parameters for time and probability. Another direction to increase impact is to generalize model checking from finite systems to real software, including reasoning about data structures.
Inaugural lecture
1 November 2018 Jaco started as a Professor in the Logic and Semantics group at the department. His research interests include modeling and analysis of safety, dependability and security aspects of software-intensive embedded systems by means of model checking, theorem proving and testing. More specifically, he has worked on the development of new model checking techniques based on symbolic techniques and high-performance computing (e.g. distributed model checking, multi-core and out-of-core algorithms). Application domains include embedded systems, distributed systems, security protocols, and biological systems.
The lecture will be followed by an informal reception