An Improved Interface for Interactive Proofs in Separation Logic

Seit Software entwickelt wird, stellt sich die Frage, ob diese korrekt ist, d.h. ob sie
das tut, was sie tun soll. Gegeben eine formale Spezifikation der Anforderungen, ist
eine Aufgabe der Softwareverifikation also zu beweisen, ob eine Implementierung diese
Spezifikation erfüllt. Diese Aufgabe kann schwierig zu lösen sein, wenn die verwendete
Programmiersprache Befehle mit globalem Effekt erlaubt, sodass diese andere Befehle
in unabhängigen Teilen des Programms beeinflussen können, zum Beispiel durch einen
gemeinsam genutzten Heap-Speicher. Separation-Logic löst dieses Problem, indem es
... mehr
Aussagen um einen separierenden Operator erweitert, wodurch es möglich ist, Teile
eines Programms als unabhängig vom Rest des Programms anzusehen. Ein Werkzeug,
das Beweise zur Softwareverifikation unterstützt, sind interaktive Theorembeweiser.
Allerdings benötigen Separation-Logic-Beweise in interaktiven Theorembeweisern,
besonders mit nicht-linearem Typsystem, viel manuellen Aufwand zur Verwaltung
der benötigten Datenstrukturen. Dies kann vermieden werden, indem dem Nutzer
eine Schnittstelle zur Verfügung gestellt wird, die Beweise auf der typischen, höheren
Abstraktionsebene ermöglicht. Diese Arbeit beschreibt eine neue Schnittstelle für
Separation-Logic-Beweise in dem interaktiven Theorembeweiser Lean 4, basierend
auf dem Iris-Projekt, und die Verbesserungen an dieser Schnittstelle.

For as long as software has been developed, a major concern has been to know
whether it is correct in the sense that is does what it is supposed to do. Given a
formal specification of the requirements, one task of software verification is to prove
that an implementation fulfills the specification. This task can be difficult if the used
programming language allows commands to have global effect, such that they can
influence commands in unrelated parts of the program, for example through a shared
heap. Separation logic aims to solve this problem by adding a separating operator to
... mehr
propositions, which makes it possible to treat parts of a program as independent of
the rest. One tool that supports software verification proofs are interactive theorem
provers. However, performing separation logic proofs in interactive theorem provers,
especially with non-linear type systems, requires a lot of boilerplate code and manual
bookkeeping. This can be avoided by providing the user with an interface that
allows proofs on the common, higher abstraction level. This work describes a new
separation logic interface for the interactive theorem prover Lean 4 based on the Iris
project and the improvements made to this interface.