Institute for Computer Architecture
and Parallel Computing
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