ADVANCE D3.2 Model Checking

Overview

TODO: Fill this paragraph.

• TLA to B conversion, support for TLA+ in ProB (motivation: TLA can deal with real numbers,...; extend reach of the project)

• Continuous improvements of constraint solving capabilities of ProB

• Work towards full support of Theory Plug-in: Support for external and recursive functions, translator, (work in progress)

• Finish conversion to Kodkod, experiments with Kodkod and SMT translators

• Maybe: initial work on physical units supprt

Motivations / Decisions

TODO: Fill this paragraph.

Available Documentation

TODO: Fill this paragraph.

Planning

TODO: Fill this paragraph.