Holistische Verifikation von Hybriden Quantenprogrammen durch Software Bounded Model Checking
| dc.contributor.author | Klamroth,Jonas | |
| dc.contributor.author | Scheerer, Max | |
| dc.contributor.author | Denninger, Oliver | |
| dc.date.accessioned | 2021-12-14T10:57:12Z | |
| dc.date.available | 2021-12-14T10:57:12Z | |
| dc.date.issued | 2021 | |
| dc.description.abstract | 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. | de |
| dc.identifier.doi | 10.18420/informatik2021-161 | |
| dc.identifier.isbn | 978-3-88579-708-1 | |
| dc.identifier.pissn | 1617-5468 | |
| dc.identifier.uri | https://dl.gi.de/handle/20.500.12116/37671 | |
| dc.language.iso | de | |
| dc.publisher | Gesellschaft für Informatik, Bonn | |
| dc.relation.ispartof | INFORMATIK 2021 | |
| dc.relation.ispartofseries | Lecture Notes in Informatics (LNI) - Proceedings, Volume P-314 | |
| dc.subject | Bounded Model Checking | |
| dc.subject | Quantencomputing | |
| dc.subject | Verifikation | |
| dc.subject | hybride Quantenprogramme | |
| dc.title | Holistische Verifikation von Hybriden Quantenprogrammen durch Software Bounded Model Checking | de |
| gi.citation.endPage | 1830 | |
| gi.citation.startPage | 1825 | |
| gi.conference.date | 27. September - 1. Oktober 2021 | |
| gi.conference.location | Berlin | |
| gi.conference.sessiontitle | Workshop; Herausforderungen beim Testen moderner Softwaresysteme (TAV-2021) |
Dateien
Originalbündel
1 - 1 von 1
Vorschaubild nicht verfügbar
- Name:
- X1-4.pdf
- Größe:
- 227.42 KB
- Format:
- Adobe Portable Document Format