Published on March 01, 2021.

MBMV Workshop 2021

Picture: Astrid Eckert / TUM
Picture: Astrid Eckert / TUM
18. - 19. March 2021

Location: Online (virtual conference)

The MBMV Workshop of the GMM/ITG/GI-Fachgruppen 3 und 4 is a forum to discuss trends in modeling, verification, and generation of embedded systems, software and hardware. While the workshop language is German and English, most of the program this year will be in English.

BTC Embedded Systems is contributing two papers together with the University of Freiburg:

18.03.2021 09:45 Lukas Mentel (BTC-ES) "Benchmarking SMT Solvers on Automotive Code"

Abstract: Using embedded systems in safety-critical environments requires a rigorous testing of the components these systems are composed of. For example, the software running on such a system has to be evaluated regarding its code coverage -- in particular, unreachable code fragments have to be avoided according to the ISO 26262 standard. Software model checking allows to detect such dead code automatically. While a recent case study compares several academic software model checkers with the commercial test and verification tool BTC EmbeddedPlatform (BTC EP), we want to focus on a lower level -- i.e. the back-end solvers within BTC EP. Therefore, we evaluate the performance of off-the-shelf SMT solvers supporting the theory of floating-point as well as the theory of bit vectors on floating-point dominated benchmark instances originating from the automotive domain. Furthermore, we compare these off-the-shelf SMT solvers with the back-end solvers used by BTC EP.

18.03.2021 14:15 Felix Winterer (Uni Freiburg) "ICP and IC3 with Stronger Generalization"

Abstract: Most recently, IC3 was integrated into the SMT solver iSAT3.Thus, iSAT3+IC3 introduces the first IC3 variant based on interval abstraction and Interval Constraint Propagation (ICP). As strong generalization is one of the key aspects for the IC3 algorithm to be successful, we integrate two additional generalization schemes from literature into iSAT3+IC3: Inductive Generalization and Counterexamples To Generalization (CTG). Furthermore, we evaluate the benefits and the drawbacks of different variants of these methods in the context ofinterval abstraction and ICP.

Please find more information and the full program on