Seminar by Prof. Supratik Chakraborty
Model Checking Large Finite State Systems
Prof. Supratik Chakraborty
Computer Science and Engineering Department
Indian Institute of Technology Bombay
Date: Thursday, August 29, 2002
Time: 04:15 PM
Venue: CS-101
Abstract
Model checking is a widely used technique to automatically check if a finite state transition system satisfies a property expressed in a suitable temporal logic. Symbolic techniques using compact encodings have enabled analysis of state spaces with more than 2^100 states, allowing application of model-checking to real-life industrial problems. Nevertheless, there appear to be inherent bottlenecks in scaling these techniques to even larger state spaces. In this talk, I will survey the state of the art in model-checking techniques, and describe our ongoing research efforts in approximate model checking. We have recently come up with an algorithm for additive decomposition of state transition systems encoded as Boolean relations. This decomposition allows us to eliminate a particularly expensive operation, that of existential quantification, in the model checking process. Initial experiments reveal that this results in a reduction of the actual memory requirement for model checking some large benchmarks by more than an order of magnitude.
About the Speaker
Supratik Chakraborty is a faculty member in the Department of Computer Science and Engineering at IIT Bombay. He has received his BTech from IIT Kharagpur in 1993, and Ph.D. from Stanford University in 1998. After he finished his Ph.D., he briefly worked in the Fujitsu Labs, before joining IIT Bombay in 1999. His research interests include: formal methods in analysis and verification of computer systems, algorithm and complexity issues in verification, and asynchronous systems.