Correctness

The main focus of the verification group is on specification and verification of concurrent, distributed, and real-time systems. In particular, we develop theories, algorithms, and tools for analysis of programs with large state spaces and model checking of infinite-state systems. In the context of UPMARC, we concentrate on the verification of concurrent systems.

The multicore revolution forces software to exploit concurrency for performance. It is well known that concurrent programs are particularly hard to verify and test, because of the vast number of possible interactions between concurrently executing activities, making it difficult to detect and reproduce defects. Techniques for ensuring correctness must adapt, along several directions.

• Application programming will use concurrency in a disciplined way, using monitors, message-passing, transactions, or other structured concurrency primitives. Efficient tools and techniques must be developed to ensure that programs use primitives appropriately. Static program analysis techniques are currently in rapid development to meet these challenges.
• Performance-critical software in libraries for concurrent programming, in run-time systems, network protocols, operating systems, etc., will use fine-grained concurrency to exploit the potential parallelism of the underlying architecture, Such highly-concurrent algorithms will often avoid locks. In the project on Verification of highly concurrent algorithms, we combine program analysis and model checking techniques to develop powerful techniques for such algorithms and programs.
• Concurrent algorithms are often exposed to weak (relaxed) memory consistency models. Reasoning about the behavior of programs on relaxed memory models is much more difficult than for sequentially consistent memory, and it is not clear how to apply standard reasoning techniques or finite-state abstractions. Furthermore bugs introduced by weak memory model instruction reordering are frequently very hard to find by testing, since their manifestations may be rare and unpredictable.

The last decades have seen dramatic advances in software model checking, static program analysis, and testing, which can be exploited to develop methods for verification of multicore programs, which should be further developed and combined in order to address the above problems.

Research Projects

Automated Verification of Highly Concurrent Algorithms
Automated Verification of Algorithms under Weak Memory Models
Automated Verification of Concurrent Recursive Programs
Caches, Coherence and Accelerations of Transactional Memory