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项目的目标是开发用于对软件定量属性进行正式化的技术。 每个程序都有一定数量的资源，例如内存，功率和处理器周期来执行其任务。 证明系统硬件所提供的资源足以安全地执行程序，应该是验证该程序的第一步。 除了验证此类资源 - 使用权限外，还有大量域特异性定量验证对于软件的正确性至关重要。 最后，关于数量的推理可以简化非定量性能（例如终止）的验证。 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. 其次，它们从资源分析中的高级语言分析中使用的技术简化了有关现实系统代码的定量属性的推理，并同时执行和高级控制流程。他们研究了定量性属性和可笑性属性的关系，其目标是利用软件验证的正确性证明的量化推理技术的目标。