Tools
This course will use the following tools, which students should have installed on laptops that can be brought to class for in-class exercises.
Sireum is a programming language, software engineering, and formal methods framework developed at Kansas State University. This class will use Slang (the Sireum programming Language) and Logika (an automated SMT-based verification environment for Slang)
- Download and installation instructions – installation based on git sources is needed for this class
Resources
While the above Sireum/HAMR installation steps will install all of the tools needed for the class, here are some links to other documentation that you might find useful.
Rust
- Online Rust Book
- Udemy Course on Rust – Ultimate Rust Crash Course – Nathan Stocks
- I also recommend the follow-on course Ultimate Rust Crash Course
- Rustlings - free Rust exercises
- PropTest Rust property-based testing framework
- Verus - Rust verification tool
seL4
HAMR Installation (part of Sireum) with VSCode Extension
Windows Setup Instructions
1. Build\Install Sireum
Open a Command Prompt and run:
git clone --recursive https://github.com/sireum/kekinian Sireum
Sireum\bin\build.cmd
(Recommended) Add the following environment variables so Sireum tools are available from any shell:
set SIREUM_HOME=<path-to-Sireum>\Sireum
set PATH=%SIREUM_HOME%\bin;%PATH%
2. Install IVE
(Interactive Verification Environment based on IntelliJ)
From a command prompt:
%SIREUM_HOME%\bin\sireum setup ive
Launch IVE
start /B %SIREUM_HOME%\bin\win\idea\bin\IVE.exe
3. Install CodeIVE
(Interactive Verification Environment based on VS Codium, for Rust and SysMLv2 IDE support)
From a command prompt:
%SIREUM_HOME%\bin\sireum setup vscode
Launch CodeIVE
start /B %SIREUM_HOME%\bin\win\vscodium\CodeIVE.exe
Linux Setup Instructions
1. Build\Install Sireum
Open a terminal and run:
git clone --recursive https://github.com/sireum/kekinian Sireum
Sireum/bin/build.cmd
(Recommended) Add the following environment variables so Sireum tools are available from any shell:
export SIREUM_HOME=<path-to-Sireum>/Sireum
export PATH=$SIREUM_HOME/bin:$PATH
2. Install IVE
(Interactive Verification Environment based on IntelliJ)
From a terminal
$SIREUM_HOME/bin/sireum setup ive
Launch IVE
$SIREUM_HOME/bin/linux/idea/bin/IVE.sh > /dev/null 2>&1 &
3. Install CodeIVE
Interactive Verification Environment based on VS Codium, for Rust and SysMLv2 IDE support
From a terminal:
$SIREUM_HOME/bin/sireum setup vscode
Launch CodeIVE
$SIREUM_HOME/bin/linux/vscodium/bin/codeive > /dev/null 2>&1 &
macOS Setup Instructions
1. Build\Install Sireum
Open a terminal and run:
git clone --recursive https://github.com/sireum/kekinian Sireum
Sireum/bin/build.cmd
(Recommended) Add the following environment variables so Sireum tools are available from any shell:
export SIREUM_HOME=<path-to-Sireum>/Sireum
export PATH=$SIREUM_HOME/bin:$PATH
2. Install IVE
(Interactive Verification Environment based on IntelliJ)
From a terminal
$SIREUM_HOME/bin/sireum setup ive
Launch IVE
open %SIREUM_HOME/bin/mac/idea/IVE.app
3. Install CodeIVE
Interactive Verification Environment based on VS Codium, for Rust and SysMLv2 IDE support
From a terminal:
$SIREUM_HOME/bin/sireum setup vscode
Launch CodeIVE
open $SIREUM_HOME/bin/mac/vscodium/CodeIVE.app
Rust
Install Rust via rustup according to the official Rust installation instructions. You might want to take a look at the discussion of “Rust tool chains” (essentially, having different versions of Rust installed). In the future, when we start working with Verus, we will need to rely on older version(s) of Rust.
Install the Rustlings exercise framework following the instructions here