Rekonstruktion von SMT-Lib-Beweisen innerhalb von KeY

Typ:	MA
Datum:
Betreuer:	Mattias Ulbrich Jonas Schiffl
Aushang:

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.