Date: 2007-12-20 Time: 11:45 Room: BBL room 471 ----+++ Speaker: Jinfeng Zhu ----+++ Title: Java Pathfinder ----+++ Abstract Many groups from either academia or industry have paid increasingly attention on model checking software written in real program languages. The most challenging issue of model checking programs is the state explosion problem. [[http://javapathfinder.sourceforge.net/][Java !PathFinder]], which is developed by NASA Ames Research Center, is one of the most successful model checkers on real programs. It provides several mechanisms to combat the state explosion problem. These mechanism are classified into two categories: (1) reducing the storage cost of each state space; (2) reducing the number of all the generated states. In this presentation, we will first describe how Java !PathFinder solves the state explosion problem, and then give some examples of using Java !PathFinder to model check some simple programs.