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.


KeY is a theorem prover for Java Dynamic Logic based on a sequent calculus.