Home → News and Events → Colloquia → Colloquium
When: 10:00AM - 11:30AM , March 07, 2018
Speaker: Dr. Van Chan Ngo
Today, software is often developed without any formal assurance that the software satisfies its specification. To fulfill this need, especially for safety-critical software as found in automotive, avionic, and health-care systems where there is very little room for error, software has to be certified using mathematical reasoning-based verification. Recent advances in formal methods and programming language techniques make it possible to perform quantitative verification for analyzing both qualitative and quantitative aspects of a program such as correctness, timeliness, resource consumption, probabilities, reliability, or performance.
In the first part of the talk, I present a novel type system for verifying that programs correctly implement constant-resource behavior. The type system incorporates information flow tracking into resource usage analysis. This allows our system to certify programs that do not leak confidential data to attackers via side channels. We formalize this guarantee by defining a new notion of resourceaware noninterference, and prove that our type system enforces it. The second part focuses on a new static analysis for deriving upper bounds on the expected resource consumption of probabilistic programs. The analysis is fully automatic and derives symbolic bounds that are multivariate polynomials of the inputs. I present Absynth, a prototype implementation of this technique, to show that the derived constant factors in the bounds are very precise and even optimal for many programs.
Dr. Van Chan Ngo is a postdoctoral researcher at the School of Computer Science, CMU. He obtained his PhD from INRIA, France and his MSc from University of Grenoble under a French government scholarship. His research interests span programming languages, compilers, and formal verification, including verification of compiler correctness, statistical model checking, resource bound analysis, and language-based security.