Diagrammatic Reasoning in Separation Logic

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

• Matt Ridsdale (University of Cambridge)
• Wednesday 17 September 2008, 13:00-14:00
• Computer Laboratory, William Gates Building, Room SS03.

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.

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.