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

Local Reasoning about While-Loops

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2021 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity