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 |