Verifying networked programs using a model checker extension

Model checking finds failures in software by exploring every possible execution schedule. Until recently it has been mainly applied to stand-alone applications. This paper presents the I/O-cache, an extension for a Java model checker to support networked programs. It contains a cache module, which captures data streams between a target process and its peer processes. This demonstration also shows how we found a defect in a WebDAV client with a model checker and our extension.

• Type: Conference
• Year: 2009
• Where: ICSE
• Authors: Watcharin Leungwattanakit, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
• Keywords: ICSE 2009, Java Model Checker, Model Checker, Possible Execution Schedule, Software Engineering