You can access CIS Windows machine remotely via remote desktop to
remote.win.cis.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.cis.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 is a high-performance Satisfiability Modulo Theories (SMT) solver being developed at the Research in Software Engineering (RiSE) group in Microsoft Research.
sireum-v3/apps/z3 once Logika is installed.Logika is a natural deduction proof checker for propositional, predicate, and programming logics developed by Robby. We will use Logika for most of the part of the course.
Logika
and its
IntelliJ-based Integrated Verification Environment (LIVE)
are installed in remote.win.ksu.edu.
Sireum v3 is installed in C:\sireum-v3 and
IntelliJ IDEA Community Edition 15.0.3 (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.
Sireum v3 is installed in /research/santos/sireum-v3 and
IntelliJ is installed in /research/santos/idea-IC-15.0.3.
To run IntelliJ in CIS Linux labs: /research/santos/idea-IC-15.0.3/bin/idea.sh.
CIS administrators are in the process of installing Logika in the CIS labs.
Alloy is a language for modeling class/object-oriented structures and relations between those structures (in some sense, it is analogous to UML class diagrams, but it is semantically cleaner). One can use Alloy to abstractly model a variety of systems. Alloy includes a constraint language based on predicate logic that can be used to specify properties/constraints on Alloy structures. Alloy’s Constraint Analyzer can automatically analyze constraints to, e.g., find example structures that satisfy the constraints or determine if the constraints hold for all possible structures that match the given class declarations.
We will use Alloy to help learn the meaning of propositional and predicate logic. In particular, we will focus on gaining a strong intuitive understanding of the meaning of propositional connectives (and, or, not, implies) and universal and existential quantifiers from predicate logic.