Campus Event Calendar
Event Entry
What and Who
Automated Complexity Analysis for Java Programs with AProVE
Jürgen Giesl
RWTH Aachen
Talk
AG 1, AG 2, AG 3, INET, AG 4, AG 5, SWS, RG1, MMCI
Public Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 25 January 2019
10:00
60 Minutes
E1 5
002
Saarbrücken
Abstract
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.
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.
Contact
Jennifer Müller
2900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 01/21/2019 09:06 -- Created document.