Java Pathfinder

Java Pathfinder (JPF) is a system to verify executable Java bytecode programs. JPF was developed at the NASA Ames Research Center and open sourced in 2005. The acronym JPF is not to be confused with the unrelated Java Plugin Framework project. The core of JPF is a Java Virtual Machine. JPF executes normal Java bytecode programs and can store, match and restore program states. Its primary application has been Model checking of concurrent programs, to find defects such as data races and deadlocks. With its respective extensions, JPF can also be used for a variety of other purposes, including

Comment
enJava Pathfinder (JPF) is a system to verify executable Java bytecode programs. JPF was developed at the NASA Ames Research Center and open sourced in 2005. The acronym JPF is not to be confused with the unrelated Java Plugin Framework project. The core of JPF is a Java Virtual Machine. JPF executes normal Java bytecode programs and can store, match and restore program states. Its primary application has been Model checking of concurrent programs, to find defects such as data races and deadlocks. With its respective extensions, JPF can also be used for a variety of other purposes, including
Developer
NASA
Developer
NASA
Genre
enSoftware verification tool, Virtual machine
Genre
Software verification
Virtual machine
Has abstract
enJava Pathfinder (JPF) is a system to verify executable Java bytecode programs. JPF was developed at the NASA Ames Research Center and open sourced in 2005. The acronym JPF is not to be confused with the unrelated Java Plugin Framework project. The core of JPF is a Java Virtual Machine. JPF executes normal Java bytecode programs and can store, match and restore program states. Its primary application has been Model checking of concurrent programs, to find defects such as data races and deadlocks. With its respective extensions, JPF can also be used for a variety of other purposes, including * model checking of distributed applications * model checking of user interfaces * test case generation by means of symbolic execution * low level program inspection * program instrumentation and runtime monitoring JPF has no fixed notion of state space branches and can handle both data and scheduling choices.
Homepage
github.com/javapathfinder/
Hypernym
System
Is primary topic of
Java Pathfinder
Label
enJava Pathfinder
LatestReleaseDate
30 November 2010
Latest release date
30 November 2010
LatestReleaseVersion
6
Latest release version
6.0
License
Apache License
License
Apache License
Link from a Wikipage to an external page
www.nasa.gov/centers/ames/news/releases/2005/05_28AR.html
fmt.cs.utwente.nl/tools/moonwalker/
github.com/javapathfinder/
www.nasa.gov/centers/ames/multimedia/images/2005/javapathfinder.html
users.ece.utexas.edu/~khurshid/papers/JPF-issta04.pdf
Link from a Wikipage to another Wikipage
Ames Research Center
Apache License
Category:Free software testing tools
Combinatorial explosion
Concurrent computing
Cross-platform
Deadlock
Exception handling
Java (programming language)
Java bytecode
Java Native Interface
Java Virtual Machine
Model checking
NASA
Partial order reduction
Race condition
Software verification
Thread (computer science)
Virtual machine
Name
enJava Pathfinder
Name
enJava Pathfinder
OperatingSystem
Cross-platform
Operating system
Cross-platform
ProgrammingLanguage
Java (programming language)
Programming language
Java (programming language)
SameAs
3jtDQ
Java PathFinder
m.070y0p
Q4041803
Size
en1.6 MB
Size (B)
1600000.00
Size (MB)
1.6
Subject
Category:Free software testing tools
WasDerivedFrom
Java Pathfinder?oldid=1077801242&ns=0
Website
https://github.com/javapathfinder/
WikiPageLength
6693
Wikipage page ID
2285583
Wikipage revision ID
1077801242
WikiPageUsesTemplate
Template:Infobox Software
Template:ISBN
Template:Release date
Wordnet_type
synset-software-noun-1