Proving Termination of Heap-Manipulating Java Programs
- 👤 Speaker: Marc Brockschmidt, RWTH Aachen
- 📅 Date & Time: Tuesday 26 March 2013, 11:00 - 12:00
- 📍 Venue: Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB
Abstract
Automated termination analysis of imperative programs has seen great improvements in the past few years, but many of the presented methods are restricted to integer programs. To lift this restriction, we developed symbolic evaluation graphs for Java programs, a finite over-approximation of all possible program runs of heap-manipulating Java programs. The graphs are obtained by symbolic evaluation using a simple abstract domain and can serve as basis for a range of further analyses. One such use, termination analysis by a sound transformation to Integer Term Rewriting, will be discussed in detail.
Series This talk is part of the Microsoft Research Cambridge, public talks series.
Included in Lists
- All Talks (aka the CURE list)
- Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB
- bld31
- Cambridge Centre for Data-Driven Discovery (C2D3)
- Cambridge talks
- Chris Davis' list
- Guy Emerson's list
- Interested Talks
- Microsoft Research Cambridge, public talks
- ndk22's list
- ob366-ai4er
- Optics for the Cloud
- personal list
- PMRFPS's
- rp587
- School of Technology
- Trust & Technology Initiative - interesting events
- yk449
Note: Ex-directory lists are not shown.
![[Talks.cam]](/static/images/talkslogosmall.gif)

Marc Brockschmidt, RWTH Aachen
Tuesday 26 March 2013, 11:00-12:00