Tools and Techniques for Model Checking Networked Programs

For software executing several threads in parallel, testing is unreliable, as it cannot cover all thread schedules. Model checking, however, can cover all possible thread interleavings. Software model checkers can directly verify an implementation, but typically cannot handle network input/output operations, which most programs require. This shortcoming can be addressed by a special model checker designed for multiple processes, or by different kinds of extensions and preprocessors for existing model checkers. This paper surveys currently existing approaches and tools.