About me
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 Crowbar, a deductive verification system for Active Objects.
I am contributing to the ABS language and am maintaining its variability layer and its hybrid extension HABS.
You can find a list of my publications at dbpl or Google Scholar. Preprints are published here. A short version of my CV can be found here.
Recent and Upcoming Events
Workshop an Asynchronous Program Models
The 6th Workshop on Asynchronous Program Models, successor of the ABS workshop series, will be held 02. - 04.10.24 in Turin, and will be organized by Ferruccio Damiani, Luca Paolini, Gianluca Torta, and me.
Workshop on Knowledge Graph Software Lifecycle Management
Our proposal to hold the 1st Workshop on Knowledge Graph Software Lifecycle Management as part of ISWC’24 was accepted, more details to follow!
SemIIM Workshop
Our proposal to hold the 3rd International Workshop on Semantic Industrial Information Modelling (SemIIM) as part of ISWC’24 was accepted, more details to follow!
Lorentz Seminar
I am glad to have participated in the Lorentz Workshop on Contract Languages. The slides of my presentation are available here.
Dagstuhl Seminar
I am glad to have participated in the Dagstuhl Seminar 24061 on Are Knowledge Graphs Ready for the Real World?.
WAKERS’24
The 4th WAKERS workshop on Digital Engineering and Knowledge Representation was held in Stellenbosch, the slides from my tutorial on Semantically lifted digital twins and programs are available here
LNCS 14360
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
Recent and Recorded Presentations
A Hoare Logic for Domain Specification
Talk at Lorentz Workshop 2024, Leiden, Netherlands
Semantical Lifting: Programs, Digital Twins, Correctness
Talk at WAKERS Workshop 2024, Stellenbosch, South Africa
Semantical Reflection for Computational Structures
Talk at SIRIUS Lunch 2023, Oslo, Norway
Deltas for Functional Programs with Algebraic Data Types
Talk at SPLC 2023, Tokyo, Japan
Context-aware Trace Contracts
Talk at KeY Workshop 2023, Bergen, Norway
Digital Twins for Ecosystems
Talk at Green Data Lab Conference, Ås, Norway
The Semantically Reflected Digital Twin
Talk at CAMPaM, Cargese, France
Twinning-by-Construction: Ensuring Correctness for Self-adaptive Digital Twins
Talk at ISoLA, Rhodos, Greece
Digital Twin Reconfiguration Using Asset Models
Talk at ISoLA, Rhodos, Greece
Semantically Lifted Programming
Talk at TCS Seminar, KTH, Stockholm, Sweden
Knowledge Structures over Simulation Units
Conference proceedings talk at ANNSIM, online
Never Mind the Semantic Gap: Modular, Lazy and Safe Loading of RDF Data
Conference proceedings talk at ESWC, Heraklion, Greece
On the Notion of Naturalness in Formal Modeling
Talk at The Logic of Software, Darmstadt, Germany
Variability modules for Java-like languages
Conference proceedings talk at SPLC, Online
From post-conditions to post-region invariants: deductive verification of hybrid objects
Conference proceedings talk at HSCC, Online
Teaching
An instance of the KalkulierbaR tool for demonstrating different proof calculi is available at kbar.app, the source code to run an own instance is available on github.
Software
I develop, maintain or contribute to the following software. For details, please click on the respective tool.
Crowbar
Crowbar is a deductive verification tool for ABS, based on heavyweight symbolical execution and behavioral contracts.
SMOL
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
KalkulierbaR is a webtool for teaching different proof calculi for predicate and first-order logic.
Abstract Behavioral Specification (ABS)
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 and Chisel
Hybrid ABS is an extension of ABS with encapsulated continuous behavior.
KeY
KeY is a theorem prover for Java Dynamic Logic based on a sequent calculus.