Tools

CIS 301: Logical Foundations of Programming, Fall 2017

Sireum Logika

Logika is a program verifier and a natural deduction proof checker for propositional, predicate, and programming logics. Logika is part of a much larger analysis and verification framework developed by Robby called Sireum.

It is crucial that you get set up to use Logika during the first week of class. We will use Logika every week in class, and almost all homework assignments will use it.

There are two ways of getting set up to use Logika (actually, these methods also provide the entire Sireum framework, but we will only use and talk about the Logika part):

  • [Personal installation] You can install it own your own computer
  • [CS Lab installation (direct use and remote desk top)] You can use it via the K-State CS Lab machines (see below for different OS options).

Logika can be used in a nice IntelliJ-based Integrated Verification Environment (Sireum/Logika IVE) (this is what we recommend for doing all your classroom exercises and homework). There is also a way to call Logika from the command line using its command line interface (Sireum/Logika CLI).

In summary,

  • choose your method of use for Logika (personal installation, CS lab direct use, CS lab remote desktop)
  • complete the “quick start” guides above for installing/configuring and confirming that you can use Logika as needed for class activities.

If you want to do a custom installation of Logika (e.g., install from sources, install IVE into an existing installation of IntelliJ, use the Logika CLI, etc.), you can find how to do that in the complete Logika Documentation.

Z3

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

We will use Z3 in one lecture early in the course, and then we will refer to it throughout the rest of the course.

Fortunately, you do not have to install Z3.

  • It is already included in the Sireum Logika installation (in both the Personal installation and CS Lab installations). It can be found under SIREUM_HOME/apps/z3 (or SIREUM_HOME\apps\z3 in Windows OS).
  • There is a web-based Online version which is good enough for playing around or doing the Z3-related homework assignment.

Many interesting analysis, verification, and testing tools (including tools developed by Microsoft) use Z3. You can find out more about Z3 using the links below:

Using Logika on your Own Machine

Quick start videos and instructions below.

Windows

Mac

Linux

Using Logika via the K-State CS Laboratories

Sireum Logika is installed in all CS labs (e.g., 1114 and 1117 Engineering Hall). These machines can also be accessed from your personal machine using the Remote Desktop Protocol (RDP) (for this method, you need an RDP client on your personal machine, then you point it to the appropriate CS RDP servers corresponding to lab machines).

CS Windows Machines

Quick Start Videos:

In a CS Windows machine (including Windows RDP server remote.win.cs.ksu.edu), Sireum IVE can be launched by using the start menu item Sireum (or Sireum32 for the 32-bit version) or by issuing the command-line idea64 or idea. Sireum CLI can be launched by issuing the command-line sireum.

The absolute path to SIREUM_HOME is \\files.cs.ksu.edu\santos\sireum\win64\Sireum.

CS Linux Machines

Quick Start Video:

In a CS Linux machine (including using ssh -X or using the faster remote desktop protocal X2Go to cslinux.cs.ksu.edu, Sireum IVE can be launched by issuing the command-line idea.

The absolute path to SIREUM_HOME is /research/santos/sireum/linux64/Sireum.

CS RDP macOS Server

In the CS RDP macOS server remote-mac.cs.ksu.edu, Sireum IVE can be launched by double-clicking the Sireum icon in /Applications or by issuing the command-line: open /Applications/Sireum.app. Sireum CLI can be launched by issuing the command-line sireum.

The absolute path to SIREUM_HOME is /Applications/Sireum.app/Contents/Resources/sireum-v3.

Installing Remote Desktop Clients to Access CS Lab Machines from your Personal Machine

If you plan to use Remote Desktop Protocol (RDP) to access Logika on CS Lab machines from your personal machine, you can download the appropriate free client for your machine OS:

Installing X2Go Clients to Access CS Linux Lab Machines from your Personal Machine

X2Go clients for various OSes can be downloaded from: http://wiki.x2go.org/doku.php/download:start