Tools¶

Remote Desktop¶

You can access CIS Windows machine remotely via remote desktop to remote.win.cs.ksu.edu. You need to use a remote desktop software specific to your OS (e.g., win, linux, mac).

Note that if you are accessing remote.win.cs.ksu.edu from off-campus, you will need to use K-State VPN software (http://www.k-state.edu/its/security/vpn/) before connecting to it.

Z3 SMT Prover¶

Z3 is a high-performance Satisfiability Modulo Theories (SMT) solver being developed at the Research in Software Engineering (RiSE) group in Microsoft Research.

• Website
• Introductory video
• Online version
• Offline (64-bit) version is included in Sireum Logika (see below); it can be found under sireum-v3/apps/z3 once Logika is installed.

Sireum Logika¶

Logika is a natural deduction proof checker for propositional, predicate, and programming logics developed by Robby.

• Website: http://logika.sireum.org

Logika and its IntelliJ-based Integrated Verification Environment (LIVE) are installed in remote.win.cs.ksu.edu. Sireum v3 is installed in C:\Sireum-v3 and IntelliJ IDEA Community Edition (with Scala plugin and Sireum v3 plugin) is accessible through the Windows Start menu’s JetBrains folder.

They are also available in CIS Linux labs (1114 and 1117 Engineering Hall). Sireum v3 is installed in /research/santos/sireum-v3 and IntelliJ is installed in /research/santos/idea. To run IntelliJ in CIS Linux labs: /research/santos/idea/bin/idea.sh.