Grunddaten
Titel | Dekomposition von k-Induktion |
Beschreibung | Induktion ist eine oft verwendete Beweistechnik, die k-Induktion eine Generalisierung davon [1]. Auch in der Softwareverifikation verwenden eine Vielzahl von Tools k-Induktion, um Eigenschaften von Programmen zu zeigen, insbesondere um zu zeigen, dass ein Programm sicher ist. Dabei wird eine k-induktive (System)-Invariante gesucht (in der Regel eine boolesche Formel). |
Heimateinrichtung | Department für Informatik |
Art der Arbeit | praktisch / anwendungsbezogen |
Abschlussarbeitstyp | Bachelor |
Autor | Jan Frederik Haltermann, M. Sc. |
Status | verfügbar |
Aufgabenstellung | Since k-induction has been shown to be a successful technique for software verification, it is used in several approaches. In each new approach, both the base-case and step-case are re-implemented, often in sequential form. On the one hand, this leads to a high implementation effort, on the other hand, components can hardly be exchanged or parallelized. [2] Beyer, D., Dangl, M., Wendler, P. (2015). Boosting k-Induction with Continuously-Refined Invariants. In: CAV 2015. LNCS, vol 9206. Springer, Cham. https://doi.org/10.1007/978-3-319-21690-4_4 |
Voraussetzung | |
Erstellt | 06.12.2022 |