Java Pathfinder
Stc
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.
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.
