Tools

The KeY System is a formal software development tool that aims to integrate design, implementation, formal specification, and formal verification of object-oriented software as seamlessly as possible. At the core of the system is a novel theorem prover for the first-order Dynamic Logic for Java with a user-friendly graphical interface.

The project was started in November 1998 at the University of Karlsruhe. It is now a joint project of KIT, Chalmers University of Technology, Gothenburg, and TU Darmstadt. The KeY tool is available for download

KeY Project

Rêve is an automatic verification tool for relational properties (2-hyper safety properties) of C programs. Rêve can be used to automatically check whether two C programs behave equally or to verify non-interference properties of C programs.

The recent version (llreve) operates on LLVM bitcode and combines various static analyses. You can try rêve online by following the links below.

Publications ∣ llreve ∣ Reve for Non-interference ∣ IMPROVE project

Voting rules are methods to aggregate the preferences of a group to make decisions. It is however difficult to design voting rules which meet the manifold expectations regarding dependability, proportionality, fairness, etc. demanded by the voters and election commissions. BEAST is a tool to check voting rules for such properties by an easy specification language and a comprehensible counterexample presentation. It relies on the powerful bounded model checking tool CBMC. BEAST furthermore enables the computation of concrete election margins to support risk-limiting audits of election outcomes.

Website (Github) ∣ Paper

The proof script debugger is a prototypical implementation of an interaction concept for program verification systems that are rule based and use a program logic. The prototype is implemented on top of the interactive program verification system KeY. KeY is an interactive program verification system for Java program annotated with the Java Modeling Language (JML).

The protypical implementation includes a proof scripting language that is tailored to the problem domain of program verification. The main features of the language are:

1. integration of domain specific entities like goal, formula, term and rule as first-class citizens into the language;
2. an expressive proof goal selection mechanism
   • to identify and select individual proof branches,
   • to easily switch between proof branches,
   • to select multiple branches for uniform treatment (multi-matching); that is resilient to small changes in the proof
3. a repetition construct which allows repeated application of proof strategies;
4. support for proof exploration within the language.

Website

ivil is a tool for the interactive (better semi-automatic) verification on the level of an intermediate verification language.

This is a proof-of-concept implementation. Current Version: 0.20

The verification language which is used in ivil is embedded into a special dynamic logic. It is closely related - yet not entirely identical - to BoogiePL and is unstructured, indeterministic, and side-effect-free. Its basic statements are:

• assertions (assert phi)
• assumptions (assume phi)
• anonymisations (havoc x)
• assignments (x := t)
• indeterministic branching (goto n1 n2)

ivil can translate proof obligations to SMTLib input. The result of SMT solvers (such as Z3) can be used to close subgoals in ivil.

Website

leanTAP was invented by Bernhard Beckert and Joachim Posegga. It is written in Prolog and implements a complete and sound theorem prover for classical first-order logic based on free-variable semantic tableaux. The unique thing about lean is that it is probably the smallest theorem prover around. The minimal version of the Prolog source code is only 360 bytes. This is of course hardly readable; there is also the standard distribution of lean, which comes with a rudimentary user interface and some test examples. It is distributed as a shell archive (see information on getting the source code).

Website

Generalised test tables extend the concept of test tables, which are already frequently used in quality management of reactive systems. The main idea is to allow more general table entries, thus enabling a table to capture not just a single test case but a family of similar behavioural cases. We show how generalised test tables can be encoded into verification conditions for state-of-the-art model checkers. — from the paper

stvs provides a graphical user interface for the verification of Structured Text source code against generalized test tables. It is a graphical frontend for the geteta backend, providing a useful and beautiful user interface, e.g., a visualization of specification violations. stvs is open source, provided under GNU Public License v3.

Features

• Verification of Structured Text against one or more specified generalized test tables
• Transform a generalized test table into a concrete test table
• Source Code Editor for Structured Text

The Backend geteta ∣ The Frontend stvs

SemSlice is a tool which automatically produces very precise slices for C routines. Slicing is the process of removing statements from a program such that defined aspects of its behavior are retained. For producing precise slices, i.e., slices that are close to the minimal number of statements, the program's semantics must be considered. SemSlice is based on automatic relational regression verification, which SemSlice uses to select valid slices from a set of candidate slices. SemSlice provides several approaches for producing candidates for precise slices. Evaluation shows that precise slices for typical slicing challenges can be found automatically and fast.

Website

Information flow control (IFC) is a category of techniques for enforcing information flow properties. These properties require secret inputs to have a limited influence on the non-secret outputs of a program. Established IFC techniques range from scalable, fully automatic approaches that over-approximate the potential information flow (e.g., approaches based on system dependence graphs — SDGs) to more precise but less scalable approaches (e.g., logic-based approaches using theorem provers). The Combined Approach is a novel IFC technique that combines a scalable SDG-based tool, JOANA, with a precise logic-based technique provided by the theorem prover KeY, increasing the precision while maintaining the scalability of the SDG-based tool. The Combined Approach is described in more depth in this paper.

Website (GitLab)

VerifAPS (Verifiaction for Automated Producton System) is a library for supporting the verification of software for automation manufacturing domain.

Features

• parsing and analyzation of Structured Text and Sequential Function Chart, including
  • PCLOpenXML
  • Object-oriented extension (IEC 61131 2013)
• Symbolic Execution
• Reading and generation of SMV files, including
  • nuXmv control
  • counter example parsing

Website Github

sharpPI is a tool for quantified information flow analysis with support Shannon Entropy based on the SAT-based approach of Vladimir Klebanov.

QIF with sharpPI has following features:

• applicable for the C language
• support Shannon entropy (counts images and pre-images)
• deterministic and non-deterministic programs
• bounds calculation

Website

ApproxMC-p is a (δ, ϵ)-counter for models of propositional formulas with support for projection. In short, ApproxMC-p calculates an model count M for an propositional formula φ with projection on Δ, s.t. the confidence δ and the tolerance ϵ is maintained.

Website

NCubeV is a Nonlinear Neural Network Verifier: It supports the verification of neural networks w.r.t. polynomial arithmetic constraints of arbitrary propositional structure. In the past, it has been used to verify neural networks for control systems, e.g. for Vertical Airborne Collision Avoidance.

GitHub

An interactive applet for proving validity of formulas in first order predicate logic using a tableau calculus. It has been written for teaching purposes and is used in the course Formale Systeme.

Website ∣ Lecture