Posts by Collection




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.

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 is a theorem prover for Java Dynamic Logic based on a sequent calculus.


The ABS Simulator Toolchain

Published in SCP, 2022

Preprint DOI

Recommended citation: Rudolf Schlatte, Einar Broch Johnsen, Eduard Kamburjan, Silvia Lizeth Tapia Tarifa. (2022). Sci. Comput. Program.. Vol 223, 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.

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. Accepted for Publication, ACM.



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.