Efficient Model Checking of Applications with I/O

Most non-trivial applications use input/output (I/O), such as network communication. When model checking such an application, a simple state space exploration scheme is not applicable, as the process being model checked would replay I/O operations when revisiting a given state. Thus a softwaremodel checker requires a faithful model, or it has to encapsulate such operations in a cache layer that is capable of hiding redundant operations from external processes.