MSV Incognito Knowledge Base

Have you ever written a program with a bug in it? Then this course is for you! Software verification tools can check whether your program works by showing that it correctly satisfies its specification, or finds a case in which it can go wrong. Unlike unit testing and other software validation methods, verification tools use formal methods to rigorously prove correctness. Similar techniques can be used to show that (mathematical models of) cyber-physical systems work as designed.
In the course, we will start by looking at formal models of software and systems as labelled transition systems (automata) and at formal temporal logics for specification, and consider the fundamental algorithms for verification. We shall then apply these algorithms to simple discrete verification problems, such as vending machines and communications systems, and use tools for the verification of Java programs. Finally, we will look at simple continuous systems, such as robots and electronic systems, and show how to verify these using rigorous numerical methods based on interval arithmetic.