We have implemented various symbolic model checking algorithms, like BMC, k-Induction and IC3 for B and Event-B. The high-level nature of B and Event-B accounts for complicated constraints arising in these symbolic analysis techniques. In this paper we suggest using static information stemming from proof obligations to simplify occurring constraints. We show how to include proof information in the aforementioned algorithms. Using different benchmarks we compare explicit state to symbolic model checking as well as techniques with and without proof assistance. In particular for models with large branching factor, e.g., due to complicated data values being manipulated, the symbolic techniques fare much better than explicit state model checking. The inclusion of proof information results in further clear performance improvements.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{KringsL16,
author = {Sebastian Krings and
Michael Leuschel},
editor = {Michael J. Butler and
Klaus{-}Dieter Schewe and
Atif Mashkoor and
Mikl{\'{o}}s Bir{\'{o}}},
title = {Proof Assisted Symbolic Model Checking for {B} and Event-B},
booktitle = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 5th International
Conference, {ABZ} 2016, Linz, Austria, May 23-27, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9675},
pages = {135--150},
publisher = {Springer},
year = {2016},
url = {https://doi.org/10.1007/978-3-319-33600-8\_8},
doi = {10.1007/978-3-319-33600-8\_8},
timestamp = {Tue, 14 May 2019 10:00:50 +0200},
biburl = {https://dblp.org/rec/conf/asm/KringsL16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}