Software

The following software is used in this course (how to use the software):

• RISC Algorithm Language (RISCAL)
  • Manual
• RISC Theorem Proving Interface (RISCTP)
  • Manual
• Java Modeling Language (JML) (original tools not any more available)
  
  • Local copy of original tools (works with Java 5)
• OpenJML (latest release for Java 21, old stable release V0.8.59 for Java 8)
  
  • Documentation
• Extended Static Checking for Java (ESC/Java 2)
  
  • Local copy (works with Java 5)
• KeY Verification Environment
  • Tutorial (local copy), More Tutorials and Examples
• Spin Model Checker
  • Spin Online References (Basic Spin Manual, Concise Promela Reference, Promela Language Reference)