University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Cyclic Proofs of Program Termination in Separation Logic

Cyclic Proofs of Program Termination in Separation Logic

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

  • UserJames Brotherston, Imperial College
  • ClockFriday 15 June 2007, 14:00-15:00
  • HouseFW11.

If you have a question about this talk, please contact Matthew Parkinson.

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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

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