Automated Provers doing (Higher-Order) Proof search: A Case Study in the Verication of Pointer Programs
Farhad Mehta, Silvio Ranise · 2004
We would like to present results obtained after doing a case study on the possibilities of doing proof search in a higher-order logic using existing automated proof tools. A commonly occurring type of proof obligation necessary to prove the correctness of the Schorr-Waite algorithm in the interactive prover Isabelle/HOL is given as a problem to the automated prover haRVey. Preliminary experimental results are encouraging.