PRLChecker Release 2.1 (Jan 28 2009)

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.

• Static Verification of Spacecraft Procedures, E. Connors, C. Munoz, C. Schnur, and R. Siminiceanu, AIAA Infotech@Aerospace Conference and Exhibit, 2009

• Standalone application PRLChecker.jar (all libraries included)

  • Graphical interface: java -jar PRLChecker.jar
  • Command line options: java -jar PRLChecker.jar -help

• 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!

• A4O Checker Demo (Procedure 1_252).

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