COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Computer Laboratory Automated Reasoning Group Lunches > Local Reasoning about While-Loops

## Local Reasoning about While-LoopsAdd 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 talks
- Computer Laboratory, William Gates Building, Room SS03
- Interested Talks
- School of Technology
- Trust & Technology Initiative - interesting events
- bld31
- yk373's list
Note that ex-directory lists are not shown. |
## Other listsCambridge Rape Crisis Public Lectures Speech Seminars Cambridge University Expeditions Society## Other talksImaging surfaces with atoms The interpretation of black hole solutions in general relativity “Structural Biology and Chemistry of Histone Deacetylases in Human Disease and Drug Discover Positive definite kernels for deterministic and stochastic approximations of (invariant) functions CANCELLED - Mathematical methods in reacting flows: From spectral to Lyapunov analysis What is the History of the Book? |