Crowbar
Crowbar is a deductive verification tool for ABS, based on heavyweight symbolical execution and behavioral contracts.
Software
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.