![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Tuesday 25 May 2010, 13:00-14:00
Local Reasoning about While-Loops
- đ¤ Speaker: Thomas Tuerk (University of Cambridge)
- đ Date & Time: Tuesday 25 May 2010, 13:00 - 14:00
- đ Venue: Computer Laboratory, William Gates Building, Room SS03
Abstract
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.
Series This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- 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
- Martin's interesting talks
- School of Technology
- Trust & Technology Initiative - interesting events
- yk373's list
- yk449
Note: Ex-directory lists are not shown.