Åsmund Aqissiaq Arild Kløvstad

• 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