OGST - Quentin Carbonneaux

Event time: 
Tuesday, April 21, 2015 - 10:30am
AKW 200 See map
51 Prospect Street
New Haven, CT 06511
Event description: 

Quentin Carbonneaux - 3rd Year
Advisor: Zhong Shao

Title: Tools and Techniques for Resource Bound Analysis of Imperative Programs

Typical complexity analysis of computer programs proceeds by informal considerations of quantities like “the number of times loop L is executed”; it also often relies on tricky combinatorics techniques and ad-hoc reasoning.  We propose to use and apply techniques from Programming Languages like Hoare logic, formal operational semantics, and proof assistants to the problem of resource analysis.  By doing so, we provide a solid ground for sound reasoning on the resource consumption of programs.  Moreover, by noticing how classic reasoning patterns like amortized reasoning fit in this new presentation we are able to develop automatic tools to compute automatically high-assurance worst-case resource bounds.

There will be a demo!