Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Automated Complexity Analysis for Java Programs with AProVE
Speaker:Jürgen Giesl
coming from:RWTH Aachen
Speakers Bio:
Event Type:Talk
Visibility:D1, D2, D3, INET, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:Public Audience
Date, Time and Location
Date:Friday, 25 January 2019
Duration:60 Minutes
Building:E1 5
Automated termination analysis is an important area in program
verification. While AProVE is one of the most powerful tools for
termination analysis of Java programs since many years, we now
extended our technique in order to analyze the complexity of Java
programs as well.

Our approach first executes the program symbolically on a
suitable abstract domain. Based on this symbolic execution, we
develop a novel transformation of (possibly heap-manipulating)
Java programs to integer transition systems (ITSs). This allows
us to apply existing complexity analyzers for standard ITSs in
order to infer runtime bounds for Java programs. We demonstrate
the power of our implementation on an established benchmark set.

Moreover, we give a general overview of the AProVE tool and show
how it can be used to analyze termination and complexity of
programs for several different programming paradigms.
Name(s):Jennifer Müller
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Attachments, File(s):
Jennifer Müller/MPI-INF, 01/21/2019 09:05 AM
Last modified:
Uwe Brahm/MPII/DE, 01/25/2019 07:01 AM
  • Jennifer Müller, 01/21/2019 09:06 AM -- Created document.