Bounds for quantum weakest preconditions

Deutsch, Jonas; Gehnen, Christina; Unruh, Dominique; Katoen, Joost-Pieter

doi:10.18154/RWTH-2026-06831

Bounds for quantum weakest preconditions

Deutsch, Jonas

2026

VerantwortlichkeitsangabeJonas Deutsch

ImpressumAachen : RWTH Aachen University 2026

Umfang1 Online-Ressource : Illustrationen

Masterarbeit, RWTH Aachen University, 2025

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2026

Genehmigende Fakultät
Fak09

Hauptberichter/Gutachter
Katoen, Joost-Pieter (Thesis advisor)^RWTH* ; Unruh, Dominique (Thesis advisor)^RWTH* ; Gehnen, Christina (Consultant)^RWTH*

Tag der mündlichen Prüfung/Habilitation
2025-09-08

Online
DOI: 10.18154/RWTH-2026-06831
URL: https://publications.rwth-aachen.de/record/1038899/files/1038899.pdf

Einrichtungen

Lehrstuhl für Softwaremodellierung und Verifikation (Informatik 2) (121310)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
This thesis presents multiple proof rules for bounds on weakest (liberal) preconditions of quantum loops. It adapts Park induction as a basic mechanism for establishing upper bounds of weakest preconditions and lower bounds of weakest liberal preconditions. Building on Park induction, it discusses k-induction and derives the related approach chain comparison as further techniques for reasoning about upper bounds. Finally, it introduces guard strengthening as a mechanism to prove the correctness of lower bounds on weakest preconditions.

OpenAccess:
PDF