CCR: The First Annual Conference on Verification, Model Checking and Abstract Interpretation 2003

CCR：2003 年第一届验证、模型检查和摘要解释年会

• 批准号: 0223760
• 负责人: Lenore Zuck
• 金额: $ 0.65万
• 依托单位: New York University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2002
• 资助国家: 美国
• 起止时间: 2002-09-01 至 2003-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0223760&HistoricalAwards=false
• 关键词: CCR; First; Annual; Conference; Verification

Embedded software is playing an important role in economy, government, and military. Since such software is often deployed in safety critical applications, correctness and reliability have become issues of utmost importance. Techniques for verification and validation traditionally fall into two main categories. One is formal verification, i.e., model checking and proof methodology. The other is abstract interpretation and static analysis. The goal of formal Verification is to prove that designs meet their specifications. Model Checking an automatic approach to verification, mainly useful when dealing with finite-state systems. Abstract Interpretation is a method for designing and comparing semantics of programs. It has been successfully used to infer run-time program properties that are instrumental for program optimization purposes.There are no clear dividing lines in between these different methodologies. In fact, they can be combined. An example is the exciting new research direction that combines abstraction (of infinite-state programs into finite-state ones) with model checking (of the finite-state system), that had produced formal and automatic verification of many complex systems. There is a growing conviction in the research community that hybrid methodologies are imperative for the process of formally verifying analyzing full-fledged reactive systems.

嵌入式软件在经济、政府、军事等领域发挥着重要的作用。由于此类软件通常部署在安全关键应用中，因此正确性和可靠性已成为最重要的问题。验证和确认技术传统上分为两大类。一种是形式验证，即，模型检验和证明方法。二是抽象解释和静态分析。形式验证的目标是证明设计满足其规格。模型检测是一种自动验证方法，主要用于处理有限状态系统。抽象解释是一种设计和比较程序语义的方法。它已经成功地用于推断运行时程序的属性，这些属性对于程序优化是有帮助的。事实上，它们可以结合起来。一个例子是令人兴奋的新的研究方向，结合抽象（无限状态程序到有限状态的）与模型检查（有限状态系统），这已经产生了许多复杂系统的正式和自动验证。研究界越来越相信，混合方法对于正式验证分析成熟的反应系统的过程是必不可少的。