Mechanically Proving Hoare Formulae

Add to your list(s) Download to your calendar using vCal

• Mike Gordon (University of Cambridge)
• Tuesday 28 April 2009, 13:00-14:00
• Computer Laboratory, William Gates Building, Room SS03.

If you have a question about this talk, please contact Thomas Tuerk.

The Hoare formula P {Q} R had its 40th birthday this year! The ideas appearing in Hoare’s 1969 paper are the basis for program verification today, but now they are mechanised inside complex and sophisticated verification systems. I will compare automated methods for proving Hoare formulae based both on the forward computation of postconditions and on the backwards computation of preconditions. Although precondition methods are better known, I will argue the case for computing postconditions as this provides a verification spectrum ranging from symbolic execution (e.g. bounded model checking) to full proof of correctness.

My talk is a revised and extended version of what I presented at the recent Tony Hoare 75 birthday celebration event. I have made a few corrections and added some details on the semantic encoding in HOL .

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Automated Reasoning Group Lunches
• Computer Laboratory, William Gates Building, Room SS03
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.