PReMo -- Probabilistic Recursive Models analyzer

This is the homepage of a tool called PReMo (read as primo). PReMo is capable of analyzing:

RMC is a natural model for recursive imperative programs with probabilistic transitions. Probability comes either from an explicit randomization like in the Quicksort algorithm or by abstracting some aspects of a program.

What's new

Current version of PReMo is 1.3.1 For the changes see the changelog.


Click here and download one of the distributions

If that does not work, one can always run is from the command-line like this:
	java -jar PReMo-<version>-<your OS name><arch>.jar
If you encounter any problems when running PReMo first see the troubleshooting notes and then write an email to the address given at the bottom of this web page.


To run any of the examples:
  1. Unzip them somewhere.
  2. Run PReMo as described above.
  3. Choose from the File menu Open -> RMC, RSSG, SCFG, QBD, Equation depending on what type of an example you would like to run.
  4. Then from the Run menu Parse
  5. after parsing successfully choose Generate equations -> termination probability
  6. and finally choose the solver you would like to use from the Find solution submenu


The documentation is available here:
        PDF format   and   HTML format (unfortunately some of the pictures are missing)

Performance tests


Coming up in PReMo

Problems or comments

Send me an e-mail:
 d.wojtczak -- at --