RISC JKU
RISCAL Software and Models

The RISC Algorithm Language (RISCAL)

July 7, 2023: RISCAL 4.2.7 (performance improvements and bug fixes in system invariant/LTL checking)

JKU Linz Student Projects and Theses
See here how to join the further development of RISCAL.

The RISC Algorithm Language (RISCAL) is a specification language and associated software system for describing mathematical algorithms, formally specifying their behavior based on mathematical theories, and validating the correctness of algorithms, specifications, and theories by execution/evaluation. RISCAL also includes an interface to various SMT solvers and provides (via an embedding of the RISCTP theorem proving interface) theorem proving capabilities. The software has been implemented in Java; it is freely available under the terms of the GNU GPL. Take a look at this video presentation and this paper.

 
Click to enlarge screenshots.

Virtual Machine: You can download a pre-configured virtual Linux machine (for the free VirtualBox virtualization software) with RISCAL for execution under MS Windows, Mac OS, or Linux:
Virtual Machine with RISCAL
To start the software, login as user "guest" with password "guest", double-click the "Terminal" icon, then execute "RISCAL &". The installation of the software with sample specifications is available in "/software/RISCAL".
RISC Users: RISCAL is installed in the RISC environment. To start the softwarem execute
module load RISCAL
RISCAL &
Download RISCAL
This includes all the files for running the software on 64-bit GNU/Linux x86 computers; for others, the appropriate version of the Standard Widget Toolkit (SWT) has to be downloaded and installed.
See the files README, CHANGES, and COPYING.
Tutorial and Manual [HTML | PDF]
This is the user documentation of the software.
Subversion Repository
This is a web interface to the Subversion repository that holds the source code of the program. The repository can be read anonymously by any Subversion client from the URL
svn://svn.risc.jku.at/schreine/RISCAL
RISCAL WebEx
A software to produce web exercises for RISCAL.
Video Presentation
A slide-based video presentation on RISCAL.
Papers
Publications and reports on RISCAL.
Talks
Further slide presentations on RISCAL.

Wolfgang Schreiner
Last modified: August 29, 2019