Crowbar
Published:
Crowbar is a deductive verification tool for ABS, based on heavyweight symbolical execution and behavioral contracts.
Posts by Collection
portfolio
SMOL
Published:
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
Published:
KalkulierbaR is a webtool for teaching different proof calculi for predicate and first-order logic.
Abstract Behavioral Specification (ABS)
Published:
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
Published:
Hybrid ABS is an extension of ABS with encapsulated continuous behavior.
KeY
Published:
KeY is a theorem prover for Java Dynamic Logic based on a sequent calculus.
publications
Towards Fully Automatic Logic-Based Information Flow Analysis: An Electronic-Voting Case Study
Published in POST, 2016
Recommended citation: Quoc Huy Do, Eduard Kamburjan, Nathan Wasser. (2016). POST. LNCS 9635
Uniform Modeling of Railway Operations
Published in FTSCS, 2016
Recommended citation: Eduard Kamburjan, Reiner Hähnle. (2016). FTSCS. CCIS 694
Session-Based Compositional Analysis for Actor-Based Languages Using Futures
Published in ICFEM, 2016
Recommended citation: Eduard Kamburjan, Crystal Chang Din, Tzu-Chun Chen. (2016). ICFEM. LNCS 10009
A Unified and Formal Programming Model for Deltas and Traits
Published in FASE, 2017
Recommended citation: Ferruccio Damiani, Reiner Hähnle, Eduard Kamburjan, Michael Lienhardt. (2017). FASE. LNCS 10202
Detecting Deadlocks in Formal System Models with Condition Synchronization
Published in AVoCS, 2017
Recommended citation: Eduard Kamburjan, Michael Lienhardt. (2018). AVoCS. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. (76)
Deductive Verification of Railway Operations
Published in RSSRail, 2017
Recommended citation: Eduard Kamburjan, Reiner Hähnle. (2017). RSSRail. LNCS 10598
Same Same But Different: Interoperability of Software Product Line Variants
Published in Festschrift Arnd Poetzsch-Heffter, 2018
Recommended citation: Ferruccio Damiani, Reiner Hähnle, Eduard Kamburjan, Michael Lienhardt. (2018). Festschrift Arnd Poetzsch-Heffter. Springer
Prototyping Formal System Models with Active Objects
Published in ICE, 2018
Recommended citation: Eduard Kamburjan, Reiner Hähnle. (2018). ICE. EPTCS 279
Formal modeling and analysis of railway operations with active objects
Published in SCP, 2018
Recommended citation: Eduard Kamburjan, Reiner Hähnle, Sebastian Schön. (2018). Sci. Comput. Program.. Vol 166, Elsevier.
Stateful Behavioral Types for Active Objects
Published in ifm, 2018
Recommended citation: Eduard Kamburjan, Tzu-Chun Chen. (2018). iFM. LNCS 11023
Interoperability of software product line variants
Published in SPLC, 2018
Recommended citation: Ferruccio Damiani, Reiner Hähnle, Eduard Kamburjan, Michael Lienhardt. (2018). SPLC. ACM
Asynchronous Cooperative Contracts for Cooperative Scheduling
Published in SEFM, 2019
Recommended citation: Eduard Kamburjan, Crystal Chang Din, Reiner Hähnle, Einar Broch Johnsen. (2019). SEFM. LNCS 11724
Behavioral Program Logic
Published in TABLEAUX, 2019
Recommended citation: Eduard Kamburjan. (2019). TABLEAUX. LNCS 11714
Tool Support for Validation of Formal System Models: Interactive Visualization and Requirements Traceability
Published in F-IDE, 2019
Recommended citation: Eduard Kamburjan, Jonas Stromberg. (2019). F-IDE. EPTCS 310
Locally Static, Globally Dynamic Session Types for Active Objects
Published in Festschrift Maurizio Gabbrielli, 2020
Recommended citation: Reiner Hähnle, Anton W. Haubner, Eduard Kamburjan. (2020). Festschrift Maurizio Gabbrielli. OASIcs 86
Crowbar: Behavioral Symbolic Execution for Deductive Verification of Active Objects
Published in Arxiv, 2020
Recommended citation: Eduard Kamburjan, Marco Scaletta, Nils Rollshausen. (2021). Arxiv Preprint
Modular Verification of a Modular Specification: Behavioral Types as Program Logics
Published in PhD Thesis, 2020
Recommended citation: Eduard Kamburjan. (2020). PhD Thesis
Behavioral Contracts for Cooperative Scheduling
Published in Deductive Software Verification, 2020
Recommended citation: Eduard Kamburjan, Crystal Chang Din, Reiner Hähnle, Einar Broch Johnsen. (2020). Deductive Software Verification. LNCS 12345
Who Carries the Burden of Modularity? - Introduction to ISoLA 2020 Track on Modularity and (De-)composition in Verification
Published in ISoLA, 2020
Recommended citation: Reiner Hähnle, Eduard Kamburjan, Dilian Gurov. (2020). ISoLA. LNCS 12476
Designing Distributed Control with Hybrid Active Objects
Published in ISoLA, 2020
Recommended citation: Eduard Kamburjan, Rudolf Schlatte, Einar Broch Johnsen, Silvia Lizeth Tapia Tarifa. (2020). ISoLA. LNCS 12479
Programming and Debugging with Semantically Lifted States
Published in ESWC, 2021
Recommended citation: Eduard Kamburjan, Vidar Norstein Klungre, Rudolf Schlatte, Einar Broch Johnsen, Martin Giese. (2021). ESWC. LNCS 12731
From post-conditions to post-region invariants: deductive verification of hybrid objects
Published in HSCC, 2021
Recommended citation: Eduard Kamburjan. (2021). HSCC. ACM
Modeling and Analyzing Resource-Sensitive Actors: {A} Tutorial Introduction
Published in COORDINATION, 2021
Recommended citation: Rudolf Schlatte, Einar Broch Johnsen, Eduard Kamburjan, Silvia Lizeth Tapia Tarifa. (2021). COORDINATION. LNCS 12717
Variability modules for Java-like languages
Published in SPLC, 2021
Recommended citation: Ferruccio Damiani, Reiner Hähnle, Eduard Kamburjan, Michael Lienhardt, Luca Paolini. (2021). SPLC. ACM
Type Checking Semantically Lifted Programs via Query Containment under Entailment Regimes
Published in DL Workshop, 2021
Recommended citation: Eduard Kamburjan, Egor V. Kostylev. (2021). DL Workshop. CEUR 2954
Optimizing Semantically Lifted Programs through Ontology Modularity
Published in NWPT, 2021
Recommended citation: Eduard Kamburjan, Jieying Chen. (2021). NWPT http://icetcs.ru.is/nwpt21/abstracts/paper1.pdf
Increasing Engagement with Interactive Visualization: Formal Methods as Serious Games
Published in Formal Methods Teaching, 2021
Recommended citation: Eduard Kamburjan, Lukas Grätz. (2021). FMTea. LNCS 13122
Never Mind the Semantic Gap: Modular, Lazy and Safe Loading of RDF Data
Published in ESWC, 2022
Recommended citation: Eduard Kamburjan, Vidar Norstein Klungre, Martin Giese. (2022). ESWC. LNCS 13261
On the Notion of Naturalness in Formal Modeling
Published in Festschrift Reiner Hähnle, 2022
Recommended citation: Eduard Kamburjan, Sandro Rama Fiorini. (2022). Festschrift Reiner Hähnle. Springer
The Right Kind of Non-Determinism: Using Concurrency to Verify C Programs with Underspecified Semantics
Published in ICE, 2022
Recommended citation: Eduard Kamburjan, Nathan Wasser. (2022). ICE. EPTCS 365
The ABS Simulator Toolchain
Published in SCP, 2022
Recommended citation: Rudolf Schlatte, Einar Broch Johnsen, Eduard Kamburjan, Silvia Lizeth Tapia Tarifa. (2022). Sci. Comput. Program.. Vol 223, Elsevier.
Knowledge Structures over Simulation Units
Published in ANNSIM, 2022
Recommended citation: Eduard Kamburjan, Einar Broch Johnsen. (2022). ANNSIM. IEEE
Digital Twin Reconguration Using Asset Models
Published in ISoLA, 2022
Recommended citation: Eduard Kamburjan, Vidar Norstein Klungre, Rudolf Schlatte, Silvia Lizeth Tarifa Tapia, David Cameron, Einar Broch Johnsen. (2022). ISoLA.
Twinning-by-Construction: Ensuring Correctness for Self-Adaptive Digital Twin
Published in ISoLA, 2022
Recommended citation: Eduard Kamburjan, Crystal Chang Din, Rudolf Schlatte, Silvia Lizeth Tarifa Tapia, Einar Broch Johnsen. (2022). ISoLA.
A Notion of Equivalence for Refactorings with Abstract Execution
Published in ISoLA, 2022
Recommended citation: Ole Jørgen Abusdal, Eduard Kamburjan, Violat Ka I Pun, Volker Stolz. (2022). ISoLA.
A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems
Published in Leibniz Transactions on Embedded Systems, 2022
Recommended citation: Eduard Kamburjan, Stefan Mitsch, Reiner Hähnle. (2022). Leibniz Trans. Embed. Syst.
Deductive Verification of Active Objects with Crowbar
Published in SCP, 2023
Recommended citation: Eduard Kamburjan, Marco Scaletta, Nils Rollshausen. (2023). Sci. Comput. Program.. Elsevier.
Variability Modules
Published in Journal of Systes and Software, 2023
Recommended citation: Ferruccio Damiani, Reiner Hähnle, Eduard Kamburjan, Michael Lienhardt, Luca Paolini. (2023). J. Syst. Softw.. Elsevier.
Emerging Challenges in Compositionality and Correctness for Digital Twins
Published in fmdt, 2023
Recommended citation: Eduard Kamburjan, Vidar Norstein Klungre, S. Lizeth Tapia Tarifa, Rudolf Schlatte, Martin Giese, David Cameron, and Einar Broch Johnsen. (2023). FMDT.
Digital Twin as a Service (DTaaS): A Platform for Digital Twin Developers and Users
Published in IEEE Digital Twins, 2023
Recommended citation: Prasad Talasila, Claudio Gomes, Peter Høgh Mikkelsen, Santiago Gil Arboleda, Eduard Kamburjan, and Peter Gorm Larsen. (2023). IEEE Digital Twins. IEEE.
Runtime Enforcement Using Knowledge Bases
Published in FASE, 2023
Recommended citation: Eduard Kamburjan, Crystal Chang Din. (2023). FASE. Springer.
A Geological Case Study on Semantically Triggered Processes
Published in ESWC, 2023
Recommended citation: Yuanwei Qu, Eduard Kamburjan, and Marting Giese. (2023). ESWC. Springer.
Deltas for Functional Programs with Algebraic Data Types
Published in SPLC, 2023
Recommended citation: Ferruccio Damiani, Reiner Hähnle, Eduard Kamburjan, Michael Lienhardt, Luca Paolini. (2023). SPLC. ACM.
Compositional Correctness and Completeness for Symbolic Partial Order Reduction
Published in CONCUR, 2023
Recommended citation: Åsmund Aqissiaq Arild Kløvstad, Eduard Kamburjan, and Einar Broch Johnsen. (2023). CONCUR. Schloss Dagstuhl.
Symbolic Reasoning for Early Decision-Making in Model-Based Systems Engineering
Published in MBSE@Models, 2023
Recommended citation: Johan Cederbladh, Loek Cleophas, Eduard Kamburjan, Lucas Lima, Hans Vangheluwe. (2023). MBSE@Models. IEEE.
Context-aware Trace Contracts
Published in AOL, 2023
Recommended citation: Reiner Hähnle, Eduard Kamburjan, Marco Scaletta. (2023). Active Object Languages: Current Research Trends. LNCS 14360, Springer.
Types and Verification for Delegated Control of Hybrid Objects
Published in AOL, 2023
Recommended citation: Eduard Kamburjan, Michael Lienhardt. (2023). Active Object Languages: Current Research Trends. LNCS 14360, Springer.
Mutation-Based Integration Testing of Knowledge Graph Applications
Published in ISSRE, 2024
Recommended citation: Tobias John, Einar Broch Johnsen, Eduard Kamburjan. (2024). ISSRE. Accepted for Publication, ACM.
Composable Digital Twins on Digital Twin as a Service Platform
Published in Simulation Journal, 2024
Recommended citation: Prasad Talasila, Claudio Gomes, Lars B. Vosteen, Hannes Iven, Martin Leucker, Santiago Gil, Peter Høgh Mikkelsen, Eduard Kamburjan and Peter Gorm Larsen. (2024). Simulation, Schloss Dagstuhl.
Towards Representing Processes and Reasoning with Process Descriptions on the Web
Published in Transactions on Graph Data and Knowledge, 2024
Recommended citation: Andreas Harth, Tobias Käfer, Anisa Rula, Jean-Paul Calbimonte, Eduard Kamburjan, Martin Giese. (2024). Transactions on Graph Data and Knowledge, Schloss Dagstuhl.
Semantically triggered qualitative simulation of a geological process
Published in Applied Computing and Geosciences, 2024
Recommended citation: Yuanwei Qu, Eduard Kamburjan, Anita Torabi, Martin Giese. (2024). Appl. Comp. and Geosc. 21. Elsevier.
GreenhouseDT: An Exemplar for Digital Twins
Published in SEAMS, 2024
Recommended citation: Eduard Kamburjan, Riccardo Sieve, Chinmayi Prabhu Baramashetru, Marco Amato, Gianluca Barmina, Eduard Occhipinti, Einar Broch Johnsen. (2023). SEAMS. ACM.
Declarative Lifecycle Management in Digital Twins
Published in EDTConf, 2024
Recommended citation: Eduard Kamburjan, Nelly Bencomo, Silvia Lizeth Tapia Tarifa, Einar Broch Johnsen. (2024). EDTConf. Best Paper Award, ACM.
Towards Ontological Service-Driven Engineering of Digital Twins
Published in EDTConf, 2024
Recommended citation: Bentley Oakes, Claudio Gomes, Eduard Kamburjan, Giuseppe Abbiati, Elif Ecem Bas, Sebastian Engelsgaard. (2024). EDTConf. Best Short Paper Award, ACM.
Semantic Reflection and Digital Twins: A Comprehensive Overview
Published in Festschrift Tiziana Margaria, 2024
Recommended citation: Eduard Kamburjan, Andrea Pferscher, Rudolf Schlatte, Riccardo Sieve, Silvia Lizeth Tapia Tarifa, Einar Broch Johnsen. (2024). The Combined Power of Research, Education, and Dissemination.. LNCS 15240. Springer.
Monitoring Reconfigurable Simulation Scenarios in Co-simulated Digital Twins
Published in ISoLA, 2024
Recommended citation: Simon Tharne Hansen, Eduard Kamburjan, Zahra Kazemi. (2024). ISoLA. Springer LNCS.
Generating Transparent and Query-Based RDF Layers
Published in SofLiM, 2024
Recommended citation: Nils Rollshausen, Eduard Kamburjan, Martin Giese. (2024). SofLiM4KG. Accepted for Publication, CEUR-WS.
An Architecture for Coupled Digital Twins with Semantic Lifting
Published in SoSyM, 2024
Recommended citation: Santiago Gil, Eduard Kamburjan, Prasad Talasila, Peter Gorm Larsen. (2024). Soft. Sys. Model.. Accepted for Publication, Springer.
talks
From post-conditions to post-region invariants: deductive verification of hybrid objects
Published:
This talk about method contracts for distributed hybrid systems is available at Youtube.
Variability modules for Java-like languages
Published:
This talk about interoperable product lines is available at Youtube.
On the Notion of Naturalness in Formal Modeling
Published:
The slides for this talk about a semiotic view on naturalness in formal methods are available here.
Never Mind the Semantic Gap: Modular, Lazy and Safe Loading of RDF Data
Published:
This talk about bridging between the class models of RDF and object-oriented programming is available at Videolectures.net.
Knowledge Structures over Simulation Units
Published:
The slides for this talk about the use of semantic lifting to reason about the connections between simulation units are available here.
Semantically Lifted Programming
Published:
The slides for this talk about a semiotic view on naturalness in formal methods are available here.
Digital Twin Reconfiguration Using Asset Models
Published:
The slides for this talk about this paper are available here.
Twinning-by-Construction: Ensuring Correctness for Self-adaptive Digital Twins
Published:
The slides for this talk about this paper are available here.
The Semantically Reflected Digital Twin
Published:
The slides for this tutorial on digital twins are available here.
Digital Twins for Ecosystems
Published:
The slides for this talk presenting current activities around digital twins at IFI are available here.
Context-aware Trace Contracts
Published:
The slides for this talk presenting current activities around digital twins at IFI are available here.
Deltas for Functional Programs with Algebraic Data Types
Published:
The slides for this talk are available here.
Semantical Reflection for Computational Structures
Published:
The slides for this talk presenting current activities around semantic reflection at IFI are available here.
Semantical Lifting: Programs, Digital Twins, Correctness
Published:
The slides for this tutorial on semantic lifting are available here.
A Hoare Logic for Domain Specification
Published:
The slides for this talk are available here.
A Hoare Logic for Domain Specification
Published:
The slides for this talk are available here.
The Semantically Reflected Digital Twin
Published:
The slides for this tutorial on semantic lifting are available here.
Declarative Lifecycle Management in Digital Twins
Published:
The slides for this talk are available here.
teaching
Analysis of Hybrid Systems
Course, Technical University of Darmstadt, 2020
In the summer term of 2020 I designed and taught a course on the anaylsis of hybrid systems at the Technical University of Darmstadt, which focused on Hybrid Automata and Differential Dynamic Logic. The course material is available here if you are enrolled at TU Darmstadt. If you want to access the material otherwise, please contact me.
Models of Concurrency IN5170
Course, University of Oslo, 2022
In the autumn term of 2022 I am part of the lecturing team of IN5170, a graduate level course on models of concurrency. For details, please visit the official website.
Models of Concurrency IN5170
Course, University of Oslo, 2023
In the autumn term of 2023 I am part of the lecturing team of IN5170, a graduate level course on models of concurrency. For details, please visit the official website.