Proving Performance Properties of Higher-order Functions with Memoization
Ravi Madhavan
EPFL
20 Dec 2016, 11:30 am - 12:30 pm
Kaiserslautern building G26, room 112
simultaneous videocast to Saarbrücken building E1 5, room 029
simultaneous videocast to Saarbrücken building E1 5, room 029
SWS Colloquium
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. ...
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
Read more