![]() ![]() bytecode factories - to provide alternative execution semantics of bytecode instructions (e.g.peer classes - to execute code at the host JVM level (instead of JPF), which is mostly used to implement native methods.listeners - to implement complex properties (e.g.JPF is an open system that can be extended in a variety of ways. Racer.java:16 : int c = 420 / racer.d Extensibility ![]() The following system under test contains a simple race condition between two threads accessing the same variable d in statements (1) and (2), which can lead to a division by zero exception if (1) is executed before (2) JPF has no fixed notion of state space branches and can handle both data and scheduling choices. program instrumentation and runtime monitoring.test case generation by means of symbolic execution.model checking of distributed applications.With its respective extensions, JPF can also be used for a variety of other purposes, including Its primary application has been Model checking of concurrent programs, to find defects such as data races and deadlocks. JPF executes normal Java bytecode programs and can store, match and restore program states. The core of JPF is a Java Virtual Machine. The acronym JPF is not to be confused with the unrelated Java Plugin Framework project. JPF was developed at the NASA Ames Research Center and open sourced in 2005. Java Pathfinder (JPF) is a system to verify executable Java bytecode programs. Software verification tool, Virtual machine ![]()
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |