![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
James Brotherston, Imperial College
Friday 15 June 2007, 14:00-15:00
Cyclic Proofs of Program Termination in Separation Logic
- đ¤ Speaker: James Brotherston, Imperial College
- đ Date & Time: Friday 15 June 2007, 14:00 - 15:00
- đ Venue: FW11
Abstract
We present a new approach to proving termination of simple imperative programs, encapsulated in a Hoare-style proof system whose judgements express termination from a given program index and under a given separation logic precondition. Moreover, proofs in our system are cyclic proofs (i.e. tree proofs containing some loops) which satisfy a global trace condition – corresponding to an infinite descent principle for the inductively defined predicates in the preconditions – that ensures soundness. We demonstrate the viability of our system via simple examples, and speculate on its potential applications.
This is joint work with Cristiano Calcagno, also at Imperial, and Richard Bornat, at Middlesex University, London.
Series This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Computing and Mathematics
- Department of Computer Science and Technology talks and seminars
- FW11
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- Martin's interesting talks
- School of Technology
- tcw57âs list
- Trust & Technology Initiative - interesting events
- yk373's list
- yk449
Note: Ex-directory lists are not shown.