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促进了可靠、高效和可预测的软件系统的开发。研究人员专注于定量验证领域中最重要的三个技术目标。首先，他们为用高级语言编写的具有垃圾收集、副作用和高阶函数的程序开发了一种自动化的组合资源分析。其次，利用高级语言资源分析中的技术，简化并发执行和高级控制流的真实系统代码数量属性的推理；第三，研究数量属性与活性属性之间的关系，目的是将数量推理技术用于软件验证的正确性证明。