Speaker: Richard Mayr , Computer Science, Albert-Ludwigs-University, Freiburg, Germany
Semantic Equivalences and the Verification of Infinite-State Systems
Abstract: We give an overview over various techniques used for the automatic verification of systems with infinitely many different reachable states. Infinite state-spaces are due to features like unbounded recursion, parallel process creation, counters, clocks, buffers for asynchronous communication, and unbounded data types. In particular, we focus on the field of semantic equivalence checking and present an abstract result that explains why simulation checking is computationally harder than bisimulation checking. Furthermore, we report on some work on applied verification and the IBOC-tool. This tool implements a scalable method for automatically checking buffer-overflow conditions in UML RT and Promela models. Finally, we describe the results of some case studies with IBOC.
Short Bio: Richard Mayr holds a PhD degree in Computer Science from TU-Muenchen, Germany in 1998. His main research interest is methods for the design and formal verification of concurrent and distributed systems. Further research interest are logic, A-calculus, term rewriting, functional programming, automata theory and complexity theory.
Host: Purush Iyer, Computer Science, NCSU