Since the invention of the bug, computer scientists have dreamt of techniques that could help in verifying the correctness of computerized programs and systems. While testing has once been considered a satisfying method for detecting bugs, today's rapid development of complex systems requires more reliable methods: it is very likely that a complex system will contain bugs and it is also likely that tests of a complex system would not detect all its bugs.

Such a more reliable method is formal verification. In formal verification, we verify that a system meets a desired behavior by checking that a mathematical model of the system satisfies a formal specification that describes the behavior. I will describe briefly a variety of methods in formal verification, ranging from methods that require significant user guidance, to highly automated algorithms and tools. I will focus on model checking, which is successfully used for the verification of real-life industrial designs.

Monday, Sept. 10 at 4pm in DH 3076