PRLChecker Release 2.1 (Nov 14 2008)

PRLChecker is a structural and static checker for PRL. The static checker includes a type checker for PRL. The code can be used as a standalone application or as a Java library.

• A short abstract describing the PRLChecker capabilites

• Standalone application PRLChecker.jar (all included)
  To run the graphical interface: java -jar PRLChecker.jar
  To see the command line options: java -jar PRLChecker.jar -help

• Example of XML messages

generated for test.prl

• CheckMessages Relax NG Compact Syntax

• API Java Libraries (Requires 1.5 or higher)

  • PRLChecker API (orgnianet.jar)
  • JGraphT (jgrapht-jdk1.5.jar)
  • Java documentation
  • Use the templace Test.java to see how to include the static checker libray in your Java code

• In Linux, the PRLChecker uses Yices, SRI's SMT solver, to check that some Boolean conditions in PRL are satisfiable. To use this functionality copy the files libYicesLite.so and libyices.so to a directory that is available through the environment variable "LD_LIBRARY_PATH".

• Plenty of examples!

• Source code is available through svn://squirt.nianet.org/orgnianet/Prejudice2.1