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

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

New for: D1, D2, D3, D4, D5
<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Proving Performance Properties of Higher-order Functions with Memoization
Speaker:Ravi Madhavan
coming from:EPFL
Speakers Bio:Ravichandhran Madhavan is a fifth year Ph.D student at EPFL, Switzerland, where he is advised by Prof. Viktor Kuncak.
His research interests lie in the areas of programming languages, static program analysis and software verification.
Before joining EPFL, he spent a couple of years as a research assistant in the Programming Languages and Tools group of Microsoft Research India, where he developed a static, side-effects analysis for C# programs (seal.codeplex.com).
His Ph.D thesis is focused on resource verification of higher-order programs.
Website: lara.epfl.ch/~kandhada
Event Type:SWS Colloquium
Visibility:D1, D2, D3, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:AG Audience
Language:English
Date, Time and Location
Date:Tuesday, 20 December 2016
Time:11:30
Duration:60 Minutes
Location:Kaiserslautern
Building:G26
Room:112
Abstract
Static verification of performance properties of programs is an important problem that has attracted great deal of research. However, most existing tools infer best-effort upper bounds and hope that they match users expectations. In this talk, I will present a system for specifying and verifying bounds on resources such as the number of evaluation steps and heap-allocated objects, for functional Scala programs that may rely on lazy evaluation and memoization. In our system, users can specify the desired resource bound as a template with numerical holes in the contracts of functions e.g. as "steps <= ? * size(list) + ?", along with other functional properties necessary for establishing the bounds. The system automatically infers values for the holes that will make the templates hold for all executions of the functions. For example, the property that a function converting a propositional formula f into negation-normal form (NNF) takes time linear in the size of f can be expressed in the post-condition of the function using the predicate "steps <= ? * size(f) + ?", where size is a user-defined function counting the number of nodes in the syntax tree of the formula.
Using our tool, we have verified asymptotically precise bounds of several algorithms and data structures that rely on complex sharing of higher-order functions and memoization. Our benchmarks include balanced search trees like red-black trees and AVL trees, Okasaki’s constant-time queues, deques, lazy data structures based on numerical representations such as lazy binomial heaps, cyclic streams, and dynamic programming algorithms.
Some of the benchmarks have posed serious challenges to automatic as well as manual reasoning.
The system is a part of the Leon verifier and can be tried online at "http://leondev.epfl.ch" ("Resource bounds" section).
Contact
Name(s):Susanne Girard
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:YesTo Location:Saarbrücken
To Building:E1 5To Room:029
Tags, Category, Keywords and additional notes
Note:
Attachments, File(s):
Created by:Susanne Girard/MPI-SWS, 12/21/2016 09:25 AMLast modified by:Susanne Girard/MPI-SWS, 12/21/2016 09:34 AM
  • Susanne Girard, 12/21/2016 09:34 AM -- Created document.