DROPS

Document

DOI: 10.4230/LIPIcs.LICS.2026.17

The Algebra of Iterative Constructions

Authors: Kevin Batz, Benjamin Lucien Kaminski, Lucas Kehrer, Gerwin Klein, Todd Schmid, and Henning Urbat

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract

Fixed points are a recurring theme in computer science and are often constructed as limits of suitably seeded fixed point iterations. We present the algebra of iterative constructions (AIC) - a purely algebraic approach to reasoning about fixed point iterations of continuous endomaps on complete lattices. AIC allows derivations of constructive fixed point theorems via equational logic and avoids explicit computations with indices. For example, F ◇ F^* ⊥ = ◇ F^* ⊥ states in AIC that sup_n Fⁿ (⊥) - a construction known from the Kleene fixed point theorem - is a fixed point of F. We demonstrate the applicability of AIC by providing algebraic proofs of several well- and less-well-known fixed point theorems: Among others, we prove the Tarski-Kantorovich principle - a generalization of the Kleene fixed point theorem - as well as a fixed point-theoretic generalization of k-induction - a technique used in software verification. We moreover present a novel fixed point theorem. It improves a recent generalization of the Tarski-Kantorovich principle due to Olszewski for obtaining pre- and postfixed points from lattice-theoretic limit inferiors and limit superiors through iterating an endomap on an arbitrary seed element: We identify sufficient continuity conditions on the endomaps so that these limits become proper fixed points. We have mechanized our algebra in Isabelle/HOL. Isabelle’s sledgehammer tool is able to find proofs of the above fixed point theorems fully automatically. Finally, we investigate the completeness of our axiomatization of AIC. We prove that our finite set of finitary axioms is (a) sound but incomplete for standard models of AIC (sequences of elements from a complete lattice) and that (b) a different finite set of infinitary axioms is complete. We also prove that infinitary axioms are unavoidable: there exists no complete axiomatization of standard models given by finitely many finitary axioms.

Cite as

Kevin Batz, Benjamin Lucien Kaminski, Lucas Kehrer, Gerwin Klein, Todd Schmid, and Henning Urbat. The Algebra of Iterative Constructions. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 17:1-17:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{batz_et_al:LIPIcs.LICS.2026.17,
  author =	{Batz, Kevin and Kaminski, Benjamin Lucien and Kehrer, Lucas and Klein, Gerwin and Schmid, Todd and Urbat, Henning},
  title =	{{The Algebra of Iterative Constructions}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{17:1--17:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.17},
  URN =		{urn:nbn:de:0030-drops-268040},
  doi =		{10.4230/LIPIcs.LICS.2026.17},
  annote =	{Keywords: fixed point theorems, fixed point iteration, algebra, equational logic}
}

Document

DOI: 10.4230/DagRep.5.4.142

Qualification of Formal Methods Tools (Dagstuhl Seminar 15182)

Authors: Darren Cofer, Gerwin Klein, Konrad Slind, and Virginie Wiels

Published in: Dagstuhl Reports, Volume 5, Issue 4 (2015)

Abstract

Formal methods tools have been shown to be effective at finding defects in and verifying the correctness of safety-critical systems, many of which require some form of certification. However, there are still many issues that must be addressed before formal verification tools can be used as part of the certification of safety-critical systems. For example, most developers of avionics systems are unfamiliar with which formal methods tools are most appropriate for different problem domains. Different levels of expertise are necessary to use these tools effectively and correctly. In most certification processes, a tool used to meet process objectives must be qualified. The qualification of formal verification tools will likely pose unique challenges.

Cite as

Darren Cofer, Gerwin Klein, Konrad Slind, and Virginie Wiels. Qualification of Formal Methods Tools (Dagstuhl Seminar 15182). In Dagstuhl Reports, Volume 5, Issue 4, pp. 142-159, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{cofer_et_al:DagRep.5.4.142,
  author =	{Cofer, Darren and Klein, Gerwin and Slind, Konrad and Wiels, Virginie},
  title =	{{Qualification of Formal Methods Tools (Dagstuhl Seminar 15182)}},
  pages =	{142--159},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{5},
  number =	{4},
  editor =	{Cofer, Darren and Klein, Gerwin and Slind, Konrad and Wiels, Virginie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.5.4.142},
  URN =		{urn:nbn:de:0030-drops-53543},
  doi =		{10.4230/DagRep.5.4.142},
  annote =	{Keywords: Dependable systems, Certification, Qualification, Formal methods, Verification tools}
}

Search Results

Documents authored by Klein, Gerwin

The Algebra of Iterative Constructions

Abstract

Cite as

Qualification of Formal Methods Tools (Dagstuhl Seminar 15182)

Abstract

Cite as

Thanks for your feedback!

Could not send message