Program Verification Using Cyclic Proof

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

• Reuben Rowe, UCL
• Thursday 19 May 2016, 13:00-14:00
• FW26.

If you have a question about this talk, please contact Dominic Orchard.

I will talk about the work I have been doing extending the Cyclist automatic verification tool. I will first give an overview of the cyclic proof technique, which generalises infinite descent style proof-by-contradiction, and explain how it can be used to prove entailments in both first order logic, and separation logic. I will then describe how it can also be used in a Hoare-style system for proving the safety and termination of heap-manipulating procedural programs, and some of the technical challenges this involves.

This talk is part of the Computer Laboratory Programming Research Group Seminar series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Programming Research Group Seminar
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.