Model Checker for Java Programs

TBMG-2380

09/01/2007

Abstract
Content

Java Pathfinder (JPF) is a verification and testing environment for Java that integrates model checking, program analysis, and testing. JPF consists of a custom-made Java Virtual Machine (JVM) that interprets bytecode, combined with a search interface to allow the complete behavior of a Java program to be analyzed, including interleavings of concurrent programs. JPF is implemented in Java, and its architecture is highly modular to support rapid prototyping of new features.

Meta TagsDetails
Citation
"Model Checker for Java Programs," Mobility Engineering, September 1, 2007.
Additional Details
Publisher
Published
Sep 1, 2007
Product Code
TBMG-2380
Content Type
Magazine Article
Language
English