University of Twente

Model checking algorithms will never be bug free because they are complex and have to be implemented manually. I don't agree with this statement and I am currently working to show that. I proof the said algorithms correct in the theorem prover Isabelle/HOL and then generate correct-by-construction code from these algorithms.