Textdokument
Holistische Verifikation von Hybriden Quantenprogrammen durch Software Bounded Model Checking
Vorschaubild nicht verfügbar
Volltext URI
Dokumententyp
Dateien
Zusatzinformation
Datum
2021
Autor:innen
Zeitschriftentitel
ISSN der Zeitschrift
Bandtitel
Quelle
Verlag
Gesellschaft für Informatik, Bonn
Zusammenfassung
Quantencomputer erschließen uns durch ihren überpolynomiellem Speedup neue Anwendungsfelder für schwer-berechenbare Probleme. Der Entwurf von Quantenalgorithmen ist bisher allerdings komplex und fehleranfällig. Daher ist zu erwarten, dass vorerst nur einzelne Subroutinen eines Programms auf Quantencomputern umgesetzt werden. Um die Korrektheit solcher Programme garantieren zu können, sind neue Ansätze erforderlich. In dieser Arbeit stellen wir einen Ansatz zum vollautomatischen Nachweis der Korrektheit von Programmen mit eingebetteten Quantenalgorithmen vor. Dazu bauen wir auf Bounded-Model-Checking-Verfahren auf, welche die Fehlerfreiheit hinsichtlich einer gegebenen Spezifikation beweisen können. Als Spezifikationssprache verwenden wir JML. Dabei werden die Quantenalgorithmen als Quantenschaltkreis beschrieben und in Java eingebettet. Wir zeigen die Umsetzbarkeit unseres Ansatzes an zwei etablierten Quantenalgorithmen.