Computing That Serves

Distributed-Memory Model-Checking


Thursday, April 8, 2004 - 11:00am


Ivana Cerna, Masaryk University

The demand of validation ensuring the correctness of the design is a major challenge in system development process and nowadays the need for effective verification techniques is critical. This need has given rise to what is commonly referred to as ``Formal Verification''. Specifically the model checking method has a number of advantageous over traditional approaches to this problem like simulation, testing, and deductive reasoning. Unfortunately, the model checking method also has a drawback: its performance is dependent on the size of the state space of the system and the number of states to explore can grow exponentially.

Alleviating the state explosion problem is a challenging area of research in model-checking. The use of distributed and/or parallel processing to combat the state explosion problem gained interest in recent years. We survey several approaches to distributing enumerative model-checking for linear temporal logic LTL, compare their advantages, and discuss their drawbacks. Combinations with other state space techniques are considered as well.


Dr. Ivana Cerna graduated (with honors) in 1986 from Comenius University, Bratislava, Slovakia  in Computer Science. In 1992, she received her PhD in Computer Science from Comenius University. In 1994, she became an Associate Professor at Masaryk University, Brno, Czech Republic.

Her research interests are in concurrency theory, especially in verification and validation of concurrent systems. She is especially interested in model checking of both finite and infinite system with respect to their linear time and branching time temporal properties. Her other interests are in the area of computational complexity and algorithm design.