Colloque

A High Level Reachability Analysis using Multiway Decision Graph in the HOL Theorem Prover

Saed Abed

Membre a labase

Saed Abed

Résumé de la communication

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 that uses our MDG theory within HOL

Résumé du colloque

Notre colloque accueillera un conférencier invité de marque, expert reconnu internationalement et chef de fil dans l’un des thèmes liés au sujet principal. Ceci permettra de hausser le calibre du colloque et s’assurer d’une participation maximale de nos membres et leurs étudiants aux cycles supérieurs, ainsi que de la part de tous ceux qui sont impliqués dans la recherche tant au niveau académique qu’industriel.