Model Checking Network Programs

Go Back to Talks and Events

Talk by Cyrille Artho ,National Institute of Advanced Industrial Science and Technology (AIST), Research Center for Information Security, Japan.
Time: July 13, 2pm Place: Rm.2311 (CS Wireless Seminar Room), Computer Science Building

Modular model checking of networked programs: Most applications today communicate with other processes over a network. Such applications are often multi-threaded. The non-determinism in the thread and communication schedules makes it desirable to model check such applications. When model checking such a networked application, a simple state space exploration scheme is not applicable, as the process being model checked would repeat communication operations when revisiting a given state after backtracking. One solution to this problem is to manage the combined state space of all processes involved, but this comes at the cost of a very large state space. We propose a solution that encapsulates I/O operations in a caching layer that is capable of hiding redundant communication operations from the environment. This approach is both more portable and more scalable than other approaches, as only a single process executes inside the model checker.