# Rekonstruktion von SMT-Lib-Beweisen innerhalb von KeY

# Problem statement

Deductive program verification is the task of formally proving that a
piece of software satisfies its formally specified requirements. This
task is undecidable in theory and quite difficult to make work well
automatically in practice.

The KeY solver is a tool
developed in the research group with which Java programs can be
verified against a formal specification in a specification language
called JML.
In the course of the verification process, a variety of intermediate
formulas are produced which must be proved. Currently, most proofs are
solved with a specially deviced solver within KeY.

At the same time,
SMT solvers
have experienced considerable progress in the last years. In many cases,
they produce proofs faster than the KeY solver. Unfortunately, they
usually only *report* that a proof has been conducted successfully, but not provide
*evidence* for the fact. Hence, proofs are not easily checkable.

Some solvers, e.g. the open source solver Z3,
support proof reporting. The challenge is to incorporate these proofs
into the KeY system.

# Your Task

The goal of the thesis is to extend KeY with mechanims that allow it
to replay proofs found by Z3 (or other solvers).

In course of this thesis, you will analyse the proof reporting format
and will investigate how the steps can be replayed within the KeY
proof system.

You conduct manual experiments for the translation, but eventually
implement also an automatic proof replay engine.

## Your profile

You have a background in *formal systems* (e.g., from the
corresponding course from the KIT curricula).

### Contact

If you are interested, contact Mattias Ulbrich.