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.
The investigators focus on three technical goals that are among the most important problems in the field of quantitative verification. First, they 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, they 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, they investigate the relationship between quantitative properties and liveness properties with the goal of utilizing quantitative reasoning techniques in correctness proofs of software verification.
