University of Cambridge > > Computer Laboratory Programming Research Group Seminar > Program Verification Using Cyclic Proof

Program Verification Using Cyclic Proof

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


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