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

AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI   Info

AG Audience

English

60 Minutes

Kaiserslautern

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).

Susanne Girard

--email hidden

Yes

Saarbrücken

E1 5

029

passcode not visible

logged in users only