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