System Verification Lab (SVL)

The correctness of computational systems is of great importance to our society, since it becomes ever more reliant on the benefits of computing.

We study a range of approaches to formally model and verify computational systems to detect costly bugs and realize correct implementations. With symbolic reasoning techniques from Artificial Intelligence, we enable the fully automatic verification of larger systems through a method called model checking. In collaboration with the Concurrent Systems Lab, we develop reduction techniques to the same end. And in collaboration with the Quantum and Algorithms Labs, we develop new quantum and parallel algorithms to exploit the power of next-generation computing systems for verification. The added computational power is also necessary to analyze the behaviour of stochastic processes, such as those underlying the risk analysis of power grid infrastructure. In collaboration with industry, this forms another application area for our research.