University of Cambridge > Talks.cam > Computer Laboratory Automated Reasoning Group Lunches > Diagrammatic Reasoning in Separation Logic

Diagrammatic Reasoning in Separation Logic

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

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

Diagrammatic reasoning seeks to put the use of diagrams on a par with the use of logic, in terms of formality and automation. Humans often use diagrams informally to reason about specific instances of a general problem, in order to work out a proof that applies to all cases. This can be modelled using the notion of a “schematic proof”. I show how this applies to proving the specification of simple programs, using execution traces to automatically suggest a complete program proof.

This will be a short talk, probably around 15 minutes, with hopefully plenty of questions and discussion afterwards. I’m showing a poster at a conference the following weekend, so it will essentially be a slightly extended poster presentation in order to get some feedback.

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