NC State University

Department of Computer Science Colloquia 2003-2004

Date:   Thursday, February 12, 2004
Time:   3:30 PM (Talk)
Place:   Room 136, EGRC, Centennial Campus (click for courtesy parking request)

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

Colloquia Home Page.