About

Sireum Logika is both a highly-automated program verifier and a manual (natural deduction) proof checker for propositional, predicate, and programming logics, where manual proof steps can be used to help automation. The Logika programming language is a subset of Scala that is designed for verification, i.e., language features are incrementally added along with supporting verification features. As Logika programs are Scala programs, they can be developed, compiled, and tested by using the regular Scala language tooling and IDEs. Additionally, Logika provides an automatic program translation to source-traceable and structurally-close-to-source C code, whose results can be compiled using the CompCert Verified C Compiler, thus providing a high-assurance toolchain for program correctness down to machine code.

The IntelliJ-based Sireum Integrated Verification Environment (IVE) provides an all-in-one coding, testing, and proving environment for Logika, and CLion can be used to integrate, test, and debug Logika generated C code (Logika generates CMake files suitable for CLion projects). For teaching, we are developing a set of course notes, which is an adaptation of the Programming Logics lecture notes written by David A. Schmidt.

Logika is inspired by:

• The Natural Deduction Proof Checker (NDPC) tool (see its manual) for propositional and predicate logics developed by Brian Mulanda, Rodney R. Howell, and James Thompson.

• The Floyd-Hoare Programming Logic Proof Checker developed by Schmidt that accompanies his Programming Logics lecture notes.

Sireum Logika is an open source project released under the Simplified BSD license.