Invited Speakers

Byron Cook Microsoft Research, UK Battling Infinity The difficulty with compiling software to hardware is one of finding a priori bounds on the potentially unbounded resources used by programs: memory and time. New approaches now allow us to find bounds on these resources, leading to new high-level hardware synthesis tools. Martin Leucker Institut für Informatik, Technische Universität Münche, Germany Don't Know for Multi-Valued Systems Abstraction is one of the key techniques for model checking especially infinite state systems. In this presentation, we briefly review two-valued as well as three-valued abstraction techniques. We then turn our attention towards multi-valued logics. In multi-valued logics interpreted over multi-valued Kripke structures, the semantics of a formula is no longer just true or false but one of many truth values. To make multi-valued model checking feasible in practice, abstraction and refinement techniques are essential in this setting as well. In this talk, we address abstraction and refinement techniques in the setting of multi-valued model checking for the mu-calculus.