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

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

Program Verification Using Cyclic Proof

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.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

*LECTURE THEATRE 1* Talks1 Talk by Dr Jane Gilbert: Maps and Monsters in the Middle Ages

Other talks

Unveiling the curtain with ukubuyisa or go lata: complicated roles of museums and nation states in the cultural repatriation discourse and practice in southern Africa Feedback and the circumgalactic medium The spread of environmental cost-benefit analysis in UK government, c.1966-1995: representing the public in the Anthropocene Title to be confirmed Director's Briefing Group Presentation 5
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity