Lars Tveito

• Kristensen, Joachim Tilsted; Perhac, Jan; Tveito, Lars; Vadgaard, Lars-Bo; Thomsen, Michael Kirkedal & Shturmov, Oleks [Show all 8 contributors for this article] (2024). OnlineProver: First Experience with Teaching Formal Proofs. NIKT: Norsk IKT-konferanse for forskning og utdanning. ISSN 1892-0713. doi: 10.5324/nikt.6205. Full text in Research Archive
• Boer, Frank de; Bonsangue, Marcello; Johnsen, Einar Broch; Pun, Ka I; Tarifa, Silvia Lizeth Tapia & Tveito, Lars (2020). SymPaths: Symbolic Execution Meets Partial Order Reduction. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 12345, p. 313–338. doi: 10.1007/978-3-030-64354-6_13. Full text in Research Archive Show summary

  Symbolic execution is an important technique for software analysis, which enables systematic model exploration by following all possible execution paths for a given program. For multithreaded shared variable programs, this technique leads to a state space explosion. Partial order reduction is a technique which allows equivalent execution paths to be recognized, reducing the state space explosion problem. This paper provides formal justifications for these techniques in a multithreaded setting by proving the correctness and completeness of symbolic execution for multithreaded shared variable programs, with and without the use of partial order reduction. We then show how these formal justifications carry over to prove the soundness and relative completeness of a proof system for such multithreaded shared variable programs in dynamic logic, such that partial order reduction can be used to simplify the proof construction by mitigating the state space explosion.

• Tveito, Lars; Johnsen, Einar Broch & Schlatte, Rudolf (2020). Global Reproducibility Through Local Control for Distributed Active Objects. In Wehrheim, Heike & Cabot, Jordi (Ed.), Fundamental Approaches to Software Engineering 23rd International Conference, FASE 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings. Springer. ISSN 9783030452339. p. 140–160. doi: 10.1007/978-3-030-45234-6_7. Full text in Research Archive Show summary

  Non-determinism in a concurrent or distributed setting may lead to many different runs or executions of a program. This paper presents a method to reproduce a specific run for non-deterministic actor or active object systems. The method is based on recording traces of events reflecting local transitions at so-called stable states during execution; i.e., states in which local execution depends on interaction with the environment. The paper formalizes trace recording and replay for a basic active object language, to show that such local traces suffice to obtain global reproducibility of runs; during replay different objects may operate fairly independently of each other and in parallel, yet a program under replay has guaranteed deterministic outcome. We then show that the method extends to the other forms of non-determinism as found in richer active object languages. Following the proposed method, we have implemented a tool to record and replay runs, and to visualize the communication and scheduling decisions of a recorded run, for Real-Time ABS, a formally defined, rich active object language for modeling timed, resource-aware behavior in distributed systems.

• Boer, Frank de; Johnsen, Einar Broch; Schlatte, Rudolf; Tarifa, Silvia Lizeth Tapia & Tveito, Lars (2020). Inseguendo Fagiani Selvatici: Partial Order Reduction for Guarded Command Languages. OpenAccess Series in Informatics. 86, p. 10:1–10:18. doi: 10.4230/OASIcs.Gabbrielli.10. Full text in Research Archive Show summary

  This paper presents a method for testing whether objects in actor languages and active object languages exhibit locally deterministic behavior. We investigate such a method for a class of guarded command programs, abstracting from object-oriented features like method calls but focusing on cooperative scheduling of dynamically spawned processes executing in parallel. The proposed method can answer questions such as whether all permutations of an execution trace are equivalent, by generating candidate traces for testing which may lead to different final states. To prune the set of candidate traces, we employ partial order reduction. To further reduce the set, we introduce an analysis technique to decide whether a generated trace is schedulable. Schedulability cannot be decided for guarded commands using standard dependence and interference relations because guard enabledness is non-monotonic. To solve this problem, we use concolic execution to produce linearized symbolic traces of the executed program, which allows a weakest precondition computation to decide on the satisfiability of guards.

• Johnsen, Einar Broch; Steffen, Martin; Stumpf, Johanna Beate & Tveito, Lars (2018). An Analysis Tool for Models of Virtualized Systems. NIKT: Norsk IKT-konferanse for forskning og utdanning. ISSN 1892-0713. Full text in Research Archive Show summary

  This paper gives an example-driven introduction to modelling and analyzing virtualized systems in, e.g., cloud computing, using virtually timed ambients, a process algebra developed to study timing aspects of resource management for (nested) virtual machines. The calculus supports nested virtualization and virtual machines compete with other processes for the resources of their host environment. Resource provisioning in virtually timed ambients extends the capabilities of mobile ambients to model the dynamic creation, migration, and destruction of virtual machines. Quality of service properties for virtually timed ambients can be formally expressed using modal contracts describing aspects of resource provisioning and verified using a model checker for virtually timed ambients, implemented in the rewriting system Maude.

• Johnsen, Einar Broch; Steffen, Martin; Stumpf, Johanna Beate & Tveito, Lars (2018). Checking Modal Contracts for Virtually Timed Ambients. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 11187 LNCS, p. 252–272. doi: 10.1007/978-3-030-02508-3_14. Full text in Research Archive
• Johnsen, Einar Broch; Steffen, Martin; Stumpf, Johanna Beate & Tveito, Lars (2018). Resource-Aware Virtually Timed Ambients. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 11023, p. 194–213. doi: 10.1007/978-3-319-98938-9_12. Full text in Research Archive

View all works in NVA

• Giese, Martin; Johnsen, Einar Broch; Tveito, Lars & Waaler, Arild Torolv Søetorp (2024). Roger Antonsen (1976 - 2024). Full text in Research Archive
• Giese, Martin; Johnsen, Einar Broch; Tveito, Lars & Waaler, Arild Torolv Søetorp (2024). Nekrolog: Roger Antonsen fanget publikum med sitt smittende engasjement. Full text in Research Archive

View all works in NVA