I am a senior researcher at the University of Oslo, associated with the Reliable Systems group and the SIRIUS centre, where I work on formal methods for digital twins, software engineering for and with knowledge graphs, and deductive verification. Before I came to Oslo, I got my PhD from the Technical University of Darmstadt under the supervision of Reiner Hähnle.
My research focuses on the integration of technologies and theories from the Semantic Web with formal methods to specify, analyse and simulate data-heavy computational systems, in particular Digital Twins. I am developing and maintaining the SMOL language which enables programs to use knowledge graphs for reflection and data access. Furthermore, I research novel approaches to modularity in deductive program verification, in particular notions of contracts for distributed and hybrid systems. I am developing and maintaining the Crowbar, a deductive verification system for Active Objects.
Recent and Upcoming Events
Our state-of-the-art volume on current research trends in Active Object languages is now published by Springer: https://link.springer.com/book/10.1007/978-3-031-51060-1
The 5th ABS Workshop was held in Lyon, and presented recent results on using trace logics in method contracts and combining type systems with deductive verification of distributed hybrid systems.
Presentation KeY Workshop’23
Presentation on Digital Twins for Ecological Systems
Workshop on Applications of Formal Methods and Digital Twins
The Workshop on Applications of Formal Methods and Digital Twins, was successfully held at FM’23 with 6 exciting presentations and an invited talk by Ana Cavalcanti.
Tutorial on Semantically Reflected Digital Twins
Together with Einar Broch Johnsen, Silvia Lizeth Tapia Tarifa and Rudolf Schlatte, I gave a tutorial at ICTAC 2022 about our work on the combination of Semantic Web technologies with programming languages to enable self-adaptive Digital Twins that react to changes in the asset model.
Recent and Recorded Presentations
Talk at SIRIUS Lunch 2023, Oslo, Norway
Talk at KeY Workshop 2023, Bergen, Norway
Talk at Green Data Lab Conference, Ås, Norway
Talk at CAMPaM, Cargese, France
Talk at WAKERS Workshop 2024, Stellenbosch, South Africa
Talk at ISoLA, Rhodos, Greece
Talk at ISoLA, Rhodos, Greece
Talk at TCS Seminar, KTH, Stockholm, Sweden
Conference proceedings talk at ANNSIM, online
Conference proceedings talk at ESWC, Heraklion, Greece
Talk at The Logic of Software, Darmstadt, Germany
Conference proceedings talk at SPLC, Online
Conference proceedings talk at HSCC, Online
I develop, maintain or contribute to the following software. For details, please click on the respective tool.
Crowbar is a deductive verification tool for ABS, based on heavyweight symbolical execution and behavioral contracts.
The Semantic Micro Object Language is an object oriented-language that implements semantic lifting: at runtime programs states are interpreted as knowledge graphs and enriched with ontological knowledge.
KalkulierbaR is a webtool for teaching different proof calculi for predicate and first-order logic.
ABS is a language for Abstract Behavioral Specification, which combines implementation-level specifications with verifiability, high-level design with executablity, and formal semantics with practical usability. ABS is a concurrent, object-oriented, modeling language that features functional data-types.
Hybrid ABS is an extension of ABS with encapsulated continuous behavior.
KeY is a theorem prover for Java Dynamic Logic based on a sequent calculus.