D45 Model Checking
From Event-B
Overview
TODO An overview of the work done about model checking.
Driven by SSF usage of ProB: state compression: simplify states stored and also detect common (sub-)expressions and store them only once. E.g., when several states have the same same value for a given variable x then its value will only be stored once. This was achieved without compromising speed.
Motivations
TODO To be completed.
Choices / Decisions
TODO To be completed.
Available Documentation
TODO To be completed.
Status
TODO To be completed.
