Åsmund Aqissiaq Arild Kløvstad

• Henrio, Ludovic; Johnsen, Einar Broch; Kløvstad, Åsmund Aqissiaq Arild; Pun, Violet Ka I & Zakowski, Yannick (2026). Layers of Confluence for Actors. In Stark, Kathrin; Zakowski, Yannick; Swamy, Nikhil & Tabareau, Nicolas (Ed.), Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs. Association for Computing Machinery (ACM). ISSN 9798400723414. p. 309–324. doi: 10.1145/3779031.3779104. Full text in Research Archive Show summary

  This paper introduces a novel proof technique to show that parallel or distributed programs exhibit confluent behaviour, even when the execution of these programs is inherently non-deterministic. The proposed method allows us to prove the confluence of programs for which standard properties such as strong confluence or commutativity of operations do not hold. Our technique builds on a method to prove the confluence of rewrite systems by de Bruijn, which we first adapt and formalise in Rocq. This method can be seen as a specialised induction principle for proving confluence. The paper further considers how this induction principle can be used in the context of programming languages. We show how the proof method can be instantiated to establish confluence conditions for programs in a small Actor-like programming language and demonstrate the application of the method to prove the confluence of a class of programs that cannot be proven to have deterministic behaviour by standard techniques.

• Kløvstad, Åsmund Aqissiaq Arild; Kobialka, Paul; Sieve, Riccardo; Pferscher, Andrea; Slaughter, Laura Ann & Tarifa, Silvia Lizeth Tapia [Show all 7 contributors for this article] (2025). What-If Scenarios for the BedreFlyt Digital Twin. In Bertrand, Nathalie; Dubslaff, Clemens & Klüppelholz, Sascha (Ed.), Principles of Formal Quantitative Analysis: Essays Dedicated to Christel Baier on the Occasion of Her 60th Birthday. Springer Nature. ISSN 9783031974397. p. 360–381. doi: 10.1007/978-3-031-97439-7_18. Full text in Research Archive Show summary

  Digital twin technology is emerging as a valuable tool for both short-term decision-making and long-term strategic planning across domains such as process industry, energy, space, transport, and healthcare. This paper reports on ongoing work in designing a digital twin to enhance resource planning in hospitals, e.g., for in-patient needs. Our focus here is on a novel technique to express what-if scenarios in digital twins to improve strategic planning processes, spanning, e.g., average-case and worst-case resource needs, expected patient treatments, and ranging over variations in available resources such as bed bays in the hospital ward. Due to the modularity of our digital twin architecture, different what-if scenarios can be explored simply by configuring the digital twin’s orchestrator, which triggers a formal methods analysis pipeline that combines executable formal models for simulation, optimization over constraints and a knowledge base that formalizes domain knowledge. We illustrate what-if scenario analysis in our digital twin architecture by considering the problem of bed bay allocation in a hospital ward.

• Voogd, Eisse Hendrik; Kløvstad, Åsmund Aqissiaq Arild; Johnsen, Einar Broch & Wąsowski, Andrzej (2025). Compositional symbolic execution semantics. Theoretical Computer Science. ISSN 0304-3975. 1044. doi: 10.1016/j.tcs.2025.115263. Full text in Research Archive Show summary

  Symbolic execution is a program analysis technique to systematically explore all possible paths through a program. The technique can be formally explained by means of small-step transition systems that update symbolic states and compute a precondition corresponding to the taken execution path. In stateful transition systems behavior may depend on previous transitions, which complicates compositional reasoning about programs. To enable compositonal reasoning this paper defines a denotational semantics for symbolic execution. The proposed semantics views a program as a set of traces, each of which has a corresponding substitution — the composition of all its assignments — and a corresponding path condition — the conjunction of all its Boolean tests under appropriate substitution. We prove correspondence between the symbolic denotational semantics and a concrete semantics. We argue that the symbolic denotational semantics is a very natural framework to reason about symbolic execution, and use it to prove that symbolic execution computes (weakest) preconditions. We provide mechanizations in Coq for the main results.

• Voogd, Eisse Hendrik; Johnsen, Einar Broch; Kløvstad, Åsmund Aqissiaq Arild; Rot, Jurriaan & Silva, Alexandra (2024). Correct and Complete Symbolic Execution for Free. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 15234, p. 237–255. doi: 10.1007/978-3-031-76554-4_13. Full text in Research Archive Show summary

  Symbolic execution is a powerful technique for program analysis. However, the formal semantics underlying symbolic execution is often developed on an ad-hoc basis and decoupled from the concrete semantics of the programming language. To overcome this issue, we introduce symbolic SOS: a rule format that allows us to simultaneously specify concrete and symbolic operational semantics. We prove that symbolic semantics, when generated from symbolic SOS, is both correct and complete with respect to the corresponding concrete semantics. The approach relies only on an algebraic signature of the source language, and is thus language-independent.

• Voogd, Eisse Hendrik; Johnsen, Einar Broch; Kløvstad, Åsmund Aqissiaq Arild; Rot, Jurriaan & Silva, Alexandra (2024). Correct and Complete Symbolic Execution for Free. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 15234, p. 237–255. doi: 10.1007/978-3-031-76554-4_13. Full text in Research Archive
• Voogd, Eisse Hendrik; Kløvstad, Åsmund Aqissiaq Arild & Johnsen, Einar Broch (2023). Denotational Semantics for Symbolic Execution. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 14446, p. 370–387. doi: 10.1007/978-3-031-47963-2_22. Full text in Research Archive
• Kløvstad, Åsmund Aqissiaq Arild; Kamburjan, Eduard & Johnsen, Einar Broch (2023). Compositional Correctness and Completeness for Symbolic Partial Order Reduction. Leibniz International Proceedings in Informatics. 279, p. 9:1–9:16. doi: 10.4230/LIPIcs.CONCUR.2023.9. Full text in Research Archive Show summary

  Partial Order Reduction (POR) and Symbolic Execution (SE) are two fundamental abstraction techniques in program analysis. SE is particularly useful as a state abstraction technique for sequential programs, while POR addresses equivalent interleavings in the execution of concurrent programs. Recently, several promising connections between these two approaches have been investigated, which result in symbolic partial order reduction: partial order reduction of symbolically executed programs. In this work, we provide compositional notions of completeness and correctness for symbolic partial order reduction. We formalize completeness and correctness for (1) abstraction over program states and (2) trace equivalence, such that the abstraction gives rise to a complete and correct SE, the trace equivalence gives rise to a complete and correct POR, and their combination results in complete and correct symbolic partial order reduction. We develop our results for a core parallel imperative programming language and mechanize the proofs in Coq.

View all works in NVA