Tools

CIS 301: Logical Foundations of Programming, Spring 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

Windows

Installing

  • Quick Start Video (must authenticate with KSOL to watch video)
  • (alternatively) Read the instructions for Windows in Section 1.1.1.1 of the Logika documentation

Downloading CS 301 Examples Used in Lectures

Mac

Installing

  • Read the instructions for Mac in Section 1.1.1.1 of the Logika documentation

Downloading CS 301 Examples Used in Lectures

  • Follow the concepts in this video related to obtaining the examples. They may be slightly different for Mac Quick Start Video

Linux

Installing

  • Read the instructions for Linux in Section 1.1.1.1 of the Logika documentation

Downloading CS 301 Examples Used in Lectures

  • Follow the concepts in this video related to obtaining the examples. They may be slightly different for Linux Quick Start Video

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

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.

CS Linux Machines

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.

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