Efficient Model Checking of Applications with Input/Output

Most non-trivial applications use some form of 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 software model checking needs to encapsulate such operations in a caching layer that is capable of hiding redundant executions of I/O operations from the environment.

• Type: Conference
• Year: 2007
• Where: EUROCAST
• Authors: Cyrille Artho, Boris Zweimüller, Armin Biere, Etsuya Shibayama, Shinichi Honiden
• Keywords: EUROCAST 2007, Hardware, I/O Operations, Model Checking, Most Non-trivial Applications