Main page |
| Project overview |
| The goal of this project is to automate large parts of the interactive VAMP proof. We therefore integrate several automated tools into Isabelle/HOL and let them solve as many lemmas and subgoals as possible. |
| Project status |
| The model checker NuSMV is linked to Isabelle/HOL through Oracle-Interface. The interface supports CTL and LTL. A sequential processor is verified with the help of NuSMV. All hardware circuits of the microprocessor are verified with the help of NuSMV as well. |
| Project members |
|
Dr. Sergey Tverdyshev Pavel Emeliyanenko |
