Sebastian Krings
Sebastian Krings
Home
Posts
Projects
Publications
Contact
Light
Dark
Automatic
Model Checking
Experience Report on An Inquiry-Based Course on Model Checking
The development and improvement of model checkers for the validation of hard- and software is an ongoing research topic in computer …
Sebastian Krings
,
Philipp Körner
,
Joshua Schmidt
PDF
Cite
Project
Project
BMoth
A prototypical model checker focussing on reusable libraries.
Source Code
Formal Methods Accessibility
Lower barriers and learning curves to enable the usage of formal methods in mainstream industries.
ProB
Animator, constraint solver and (symbolic) model checker for the B-Method.
Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation
During a course on model checking we developed BMoth, a full-stack model checker for classical B, featuring both explicit-state and …
Jessica Petrasch
,
Jan-Hendrik Oepen
,
Sebastian Krings
,
Moritz Gericke
PDF
Cite
Project
DOI
A Translation from Alloy to B
In this paper, we introduce a translation of the specification language Alloy to classical B. Our translation closely follows the Alloy …
Sebastian Krings
,
Joshua Schmidt
,
Carola Brings
,
Marc Frappier
,
Michael Leuschel
PDF
Cite
Project
DOI
Using a Formal B Model at Runtime in a Demonstration of the ETCS Hybrid Level 3 Concept with Real Trains
In this article, we present a concrete realisation of the ETCS Hybrid Level 3 concept, whose practical viability was evaluated in a …
Dominik Hansen
,
Michael Leuschel
,
David Schneider
,
Sebastian Krings
,
Philipp Körner
,
Thomas Naulin
,
Nader Nayeri
,
Frank Skowron
PDF
Cite
Project
DOI
Proof Assisted Bounded and Unbounded Symbolic Model Checking of Software and System Models
We have implemented various symbolic model checking algorithms, such as BMC, k-Induction and IC3 for B, Event-B and other modeling …
Sebastian Krings
,
Michael Leuschel
Cite
Project
DOI
The Burden of High-Level Languages: Complicated Symbolic Model Checking
Symbolic model checking algorithms like IC3 have proven to be an effective technique for hardware model checking. Extensions to …
Sebastian Krings
PDF
Cite
Project
Proof Assisted Symbolic Model Checking for B and Event-B
We have implemented various symbolic model checking algorithms, like BMC, k-Induction and IC3 for B and Event-B. The high-level nature …
Sebastian Krings
,
Michael Leuschel
PDF
Cite
Project
DOI
«
»
Cite
×