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

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

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.