Software

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

• RISC Algorithm Language
• Manual (PDF)
• RISC ProofNavigator
• Manual (PDF)
• RISC ProgramExplorer
• Manual (PDF)
• Java Modeling Language (JML) tools
• Use the stable release 5.5 from the archive (not the newer release candidates); also note that the JML tools need an installation of Java 1.4.2.
• Documentation
• OpenJML
• Documentation
• Extended Static Checking for Java (ESC/Java 2)
• Documentation
• 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