Local Reasoning about While-Loops

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

• Thomas Tuerk (University of Cambridge)
• Tuesday 25 May 2010, 13:00-14:00
• Computer Laboratory, William Gates Building, Room SS03.

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

Separation logic is an extension of Hoare logic that allows local reasoning. Local reasoning is a powerful feature that often allows simpler specifications and proofs. However, this power is not used to reason about while-loops.

In this talk an inference rule for the verification of the partial correctness of while-loops in Hoare logic is presented. In contrast to classical loop-invariants this inference uses pre- and post-conditions for loops. It is not specific to separation logic. Instead, it represents a slightly different view on loops. It specifies what the loop will do instead of what has already been done. However, the presented inference gains its full potential by utilising the local reasoning provided by separation logic.

The inference rule has been implemented in the separation logic tool Holfoot.

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.