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).
Das meistgenutzte Verfahren (die sogenannte „Split-Case k-Induction“) besteht aus zwei Schritten (für ein festes k): Zuerst wird gezeigt, dass das System nach k Schritten (bzw. k Schleifenabrollungen) sicher ist (der „base-case“). Im Anschluss wird der Induktionsschritt geprüft (der „step-case“). In der Praxis setzten viele Tools noch eine Komponente zum Generieren von potenziellen Invarianten ein.

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.
In this work the k-Induktions-Schema is to be decomposed first into independent components. Each component is to have thereby a clearly defined task and interfaces (- formats).
Subsequently, the decomposition shall be realized and evaluated exemplarily. For this an existing tool (e.g. the CPAchecker [2]), which uses k-induction, is to be modularized. Finally, the performance of the decomposition will be compared with the original version.

[1] The k-Induction Principle, Thomas Wahl, 2013, https://www.ccs.neu.edu/home/wahl/Publications/k-induction.pdf

[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