docs/index.md

   1 ## Welcome to the Java™Pathfinder System ##
   2
   3 This is the main page for Java™ Pathfinder (JPF). JPF is an extensible software model checking framework for Java™ bytecode programs. The system was developed at the [NASA Ames Research Center](http://arc.nasa.gov), open sourced in 2005, and is freely available on this server under the [Apache-2.0 license](http://www.apache.org/licenses/LICENSE-2.0).
   4
   5
   6 This page is our primary source of documentation, and is divided into the following sections.
   7
   8    ---
   9
  10   * [Introduction](intro/index) -- a brief introduction into model checking and JPF
  11     * [What is JPF?](intro/what_is_jpf)
  12     * [Testing vs. Model Checking](intro/testing_vs_model_checking)
  13          - [Random value example](intro/random_example)
  14          - [Data race example](intro/race_example)
  15     * [JPF key features](intro/classification)
  16
  17     ---
  18
  19   * [How to obtain and install JPF](install/index) -- everything to get it running on your machine
  20     - [System requirements](install/requirements)
  21     - Downloading [binary snapshots](install/snapshot) and [sources](install/repositories)
  22     - [Creating a site properties file](install/site-properties)
  23     - [Building, testing, and running](install/build)
  24     - Installing the JPF plugins
  25          - [Eclipse](install/eclipse-plugin)
  26          - [NetBeans](install/netbeans-plugin)
  27
  28     ---
  29
  30   * [How to use JPF](user/index) -- the user manual for JPF
  31     - [Different applications of JPF](user/application_types)
  32     - [JPF's runtime components](user/components)
  33     - [Starting JPF](user/run)
  34     - [Configuring JPF](user/config)
  35     - [Understanding JPF output](user/output)
  36     - [Using JPF's Verify API in the system under test](user/api)
  37
  38     ---
  39
  40   * [Developer guide](devel/index) -- what's under the hood
  41     * [Top-level design](devel/design)
  42     * Key mechanisms, such as
  43         - [ChoiceGenerators](devel/choicegenerator)
  44         - [Partial order reduction](devel/partial_order_reduction)
  45         - [Slot and field attributes](devel/attributes)
  46     * Extension mechanisms, such as
  47         - [Listeners](devel/listener)
  48         - [Search Strategies](devel/design)
  49         - [Model Java Interface (MJI)](devel/mji)
  50         - [Bytecode Factories](devel/bytecode_factory)
  51     * Common utility infrastructures, such as
  52         - [Logging system](devel/logging)
  53         - [Reporting system](devel/report)
  54     * [Running JPF from within your application](devel/embedded)
  55     * [Writing JPF tests](devel/jpf_tests)
  56     * [Coding conventions](devel/coding_conventions)
  57     * [Hosting an Eclipse plugin update site](devel/eclipse_plugin_update)
  58
  59     ---
  60
  61   * [JPF core project](jpf-core/index) -- description and link to jpf-core
  62
  63     ---
  64
  65   * [Related research and publications](papers/index)
  66