Model Checking Network Applications

Speaker: Cyrille Artho

Abstract:

This tutorial addresses a new model checking technique for networked applications. Such applications could not be model checked by traditional techniques, as multiple processes cannot be checked in normal (single-process) software model checkers. Our approach is to convert processes into threads and to model network communication using a special library and model checker extensions. Other approaches include the usage of stubs or a special cache that can serialize the state space exploration tree.