[Pl-seminar] 10/31: Jan Hoffmann, Formal Reasoning about Quantitative Properties of Software

[Vincent St-Amour]

NUPRL Seminar presents

Jan Hoffmann
Yale University

1:30 - 3:00
Friday, 10/31
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)


Formal Reasoning about Quantitative Properties of Software

Abstract:
Quantitative properties such as execution time, memory consumption,
and power usage determine whether a software system is useful in
practice. A precise understanding of quantitative properties of
software is also essential to ensure safety (e.g., no stack overflow)
and security (e.g., no side-channel vulnerabilities). Yet, it is still
hard to reason about quantitative characteristics of software at
development time.

In this talk, I will present novel techniques for modeling and
analyzing quantitative properties of software. These techniques are
designed to meet two major challenges of quantitative analyses:
precision and compositionality.

First, I will present type-based amortized resource analysis, a static
analysis system that automatically derives worst-case resource bounds
for functional programs. The derived bounds are parametric in the
sizes of the inputs and defined by a novel algebraic structure that we
call multivariate resource polynomials. Experiments with a prototype
implementation in the programming language Resource Aware ML show that
the analysis is precise, efficient, and compositional.

Second, I will briefly describe three applications of the ideas of
type-based amortized resource analysis to real-world problems: (1) a
quantitative reasoning technique for proving lock freedom of
concurrent data structures, (2) a framework for deriving formally
verified stack-space bounds for compiled x86 assembly code at the C
level, and (3) the use of resource analysis to find and prevent
side-channel and algorithmic-complexity vulnerabilities. The two
latter applications are of increasing interest in industry. This is
amplified by the DARPA program "Space/Time Analysis for Cybersecurity"
($53M, October 2014).

The talk is based on joint work with Klaus Aehlig, Quentin
Carbonneaux, Martin Hofmann, Mike Marmar, Tahina Ramananandro, and
Zhong Shao.