A Deep Embedding of a Decidable Fragment of Separation Logic in HOL

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

• Thomas Tuerk (University of Cambridge)
• Tuesday 26 June 2007, 13:00-14:00
• Computer Laboratory, William Gates Building, Room GS15.

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

Smallfoot is a tool to automatically check separation logic specifications of imperative programs. It uses a decidable fragment of separation logic. In this talk, I will present a deep embedding of this fragment of separation logic in HOL . Additionally, I will present a HOL implementation of a decision procedure for entailments, which is based on the inferences used by Smallfoot.

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 GS15
• 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.