Veuillez choisir le dossier dans lequel vous souhaitez ajouter ce contenu :
Filtrer les résultats
Colloque
In this work, we provide all the necessary infrastructure to define a high level states exploration approach within the HOL theorem prover. While related work has tackled the same problem by representing primitive BDD operations as inference rules added to the core of the theorem prover, we have based our approach on the Multiway Decision Graphs (MDGs). We define canonic MDGs as well-formed directed for- mulae in HOL. Then, we formalize the basic MDG operations following a deep embedding approach and we derive the correctness proof for each operation. Finally, a high level reachability analysis is implemented as a tactic …
