• Software distribution and licensing: Public binary distribution
  • Software maturity: Basic usage works, terse documentation.
  • Software Maintenance and Evolution: No maintenance, no future plans
A Compositional Deadlock Detection and Verification Tool for BIP Models


More details about the compositional deadlock detection and verification method implemented in the D-Finder tool can be found here.

 How To Install and Run D-Finder


  • Linux or Mac OS X.
  • Java 1.6.

The installation of D-Finder requires the following steps:

  • First dowload the D-Finder tool-set
  • Extract the package.
  • Follow the instructions in the INSTALL file to install and configure the third party tools Yices, Omega, and JavaBDD
  • Build your BIP model (here is an example of Dining Philosopher in BIP). More information about BIP modeling framework can be found here.
  • Go to the DFinder directory and run the D-Finder tool to verify your model by the following command:
    • For global methods: ./dfinder -c dfinder.config -f [path-to-model.bip] --method=[pm/linear]
    • For incremental methods: ./dfinder -c dfinder.config -f [path-to-model.bip] --incr_file [incr-file] --method=[pm]
    • pm: symbolic method based on positive mapping
    • linear: computes linear invariants that might be stronger but is not efficient for large-scale/complex systems.
    • [incr-file]: file that defines set of increments

News: a GUI for D-Finder has been available (for both Linux and Mac OS X). In DFinder directory, run the following script: ./dfinder-gui

 Running Examples

Dining Philosopher

in Terminal, go to D-Finder folder run the global methods by the following command:

./dfinder -c dfinder.config -f examples/philo20.bip --method=pm/fp/linear

or run the incremental methods by the following command:

./dfinder -c dfinder.config -f examples/philo20.bip -incr_file examples/philo20.incr --method=pm/fp