VeriQ

I am a co-PI of the NSF-funded VeriQ project.

The goal of the VeriQ project is to develop techniques for the formal verification of quantitative properties of software. Every program requires a certain amount of resources such as memory, power, and processor cycles to perform its task. A proof that the resources provided by the hardware of the system are sufficient to safely execute a program should be the first step in the verification of that program. In addition to the verification of such resource-usage bounds, there are a vast number of domain-specific quantitative properties that are crucial for the correctness of software. Finally, reasoning about quantities can simplify the verification of non-quantitative properties such as termination.

By advancing the state-of-the art in quantitative verification, VeriQ facilitates the development of reliable, efficient and predictable software systems. We focus on three technical goals that are among the most important problems in the field of quantitative verification. First, we develop an automatic and compositional resource analysis for programs that are written in high-level languages with garbage collection, side effects, and higher-order functions. Second, we apply the techniques from resource analysis for high-level languages to simplify the reasoning about quantitative properties of realistic system code with concurrent execution and advanced control flow. Third, we investigate the relationship between quantitative properties and liveness properties with the goal of utilizing quantitative reasoning techniques in correctness proofs of software verification.

Collaborators: Quentin Carbonneaux, Tahina Ramananandro, and Zhong Shao.

Resource Aware ML

I am actively developing Resource Aware ML (RAML), an ML-like functional programming language that implements an automatic static analysis of the quantitative resource requirements of a program.

For instance, RAML automatically derives symbolic worst-case bounds on memory and time usage of programs such as quick sort for lists of lists, in-place quick sort for arrays, Dijkstra's shortest-path algorithm, matrix operations, and longest common subsequence of two lists. The analysis is highly efficient and takes only a few seconds for the aforementioned programs.

We are constantly improving the range and the precision of the analysis. In the development of RAML we apply techniques from many interesting areas such as type systems, static analysis, constraint solving, analysis of algorithms, and design and implementation of programming languages.

Collaborators: Ankush Das, Martin Hofmann, Zhong Shao, and Shu-Chun Weng.