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

SHF：小型：VeriQ：现实应用场景中的形式化定量软件验证

• 批准号: 1319671
• 负责人: Zhong Shao
• 金额: $ 44.97万
• 依托单位: Yale University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-07-01 至 2018-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1319671&HistoricalAwards=false
• 关键词: SHF; Small; VeriQ; Formal; Quantitative

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.

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