Home
Schedule
Abstract Template
Masters Attendance
Center
Home
Courses
People
Projects
Page
Edit Page
Rename Page
Attach File
Printable
Wiki Source
More ...
Web
Recent Changes
Notify Service
News
Page Index
Search
More ...
Wiki
About TWiki
Text Formatting
Registration
Change Password
Reset Password
Users
Groups
Log In
or
Register
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. [[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.
