SHF: Small: VeriQ: Formal Quantitative Software Verification in Realistic Application Scenarios

VeriQ项目的目标是开发对软件的定量特性进行正式验证的技术。每个程序都需要一定数量的资源，如内存、电源和处理器周期来执行其任务。系统硬件提供的资源足以安全执行程序的证明应该是验证该程序的第一步。除了验证这样的资源使用边界之外，还有大量特定于领域的定量属性，这些属性对于软件的正确性至关重要。最后，关于数量的推理可以简化非数量性质（如终止）的验证。通过推进最先进的定量验证，VeriQ促进了可靠，高效和可预测的软件系统的开发。研究人员集中在三个技术目标，其中最重要的问题在定量验证领域。首先，他们为带有垃圾收集、副作用和高阶函数的高级语言编写的程序开发了自动和组合资源分析。其次，他们应用高级语言的资源分析技术来简化对具有并发执行和高级控制流的实际系统代码的定量特性的推理。第三，他们研究了定量属性和活动性属性之间的关系，目的是在软件验证的正确性证明中利用定量推理技术。

The goal of the VeriQ project is to develop techniques for the formalverification of quantitative properties of software. Every programrequires a certain amount of resources such as memory, power, andprocessor cycles to perform its task. A proof that the resourcesprovided by the hardware of the system are sufficient to safelyexecute a program should be the first step in the verification of thatprogram. In addition to the verification of such resource-usagebounds, there are a vast number of domain-specific quantitativeproperties that are crucial for the correctness of software. Finally,reasoning about quantities can simplify the verification ofnon-quantitative properties such as termination. By advancing thestate-of-the art in quantitative verification, VeriQ facilitates thedevelopment of reliable, efficient and predictable software systems.The investigators focus on three technical goals that are among themost important problems in the field of quantitative verification.First, they develop an automatic and compositional resource analysisfor programs that are written in high-level languages with garbagecollection, side effects, and higher-order functions. Second, theyapply the techniques from resource analysis for high-level languagesto simplify the reasoning about quantitative properties of realisticsystem code with concurrent execution and advanced control flow.Third, they investigate the relationship between quantitativeproperties and liveness properties with the goal of utilizingquantitative reasoning techniques in correctness proofs of softwareverification.