BSF:2012259:Circular compositional reasoning by learning and abstraction-refinement

该项目是美国-以色列计算机科学合作（USICCS）计划的一部分。 通过该计划，NSF和美国-以色列两国科学基金会（BSF）共同支持美国研究人员和以色列研究人员之间的合作。该项目的目标是通过组合技术对并发软件进行可扩展性验证。组合技术将整个程序分解为单独检查的较小组件。通常，组件不能独立于由其他组件组成的环境进行验证。因此，该组件是在对其环境的相对较小的假设下进行验证的。在过去，在简单推理规则的上下文中，假设和属性以非循环的方式相关，在自动化假设生成方面已经取得了进展。然而，在某些情况下，系统中的循环依赖是一种真实的现象，需要更复杂的循环规则，通常使用归纳参数。尽管这些规则在扩大验证方面是有效的，但其适用性受到了定义假设所涉及的手动工作的限制。该项目在现有循环规则和根据需要开发的新规则的背景下解决了假设发现过程的自动化问题。抽象和学习技术用于迭代地建立假设，并根据分别检查组件获得的反例对其进行细化。开发的算法结合了3值推理，以允许更精确而简洁的假设。该技术的目的是增加通用并发和分布式软件的保证，通过扩大现有的验证技术，通过新的自动循环组合推理。两个具体的应用领域进行了研究，即基于UML的软件和安全协议，这两个领域可以高度受益于组合推理。

This project is funded as part of the United States-Israel Collaboration in Computer Science (USICCS) program. Through this program, NSF and the United States - Israel Binational Science Foundation (BSF) jointly support collaborations among US-based researchers and Israel-based researchers. The project targets scalable verification of concurrent software via compositional techniques. Compositional techniques break-up the full program into smaller components that are checked separately. Typically, a component cannot be verified in isolation from its environment, consisting of the other components. The component is therefore verified under a relatively small assumption on its environment. Progress has been made in the past on automating assumption generation in the context of a simple reasoning rule, where assumptions and properties are related in an acyclic manner. However, there are cases where circular dependency within a system is a real phenomenon that requires more complex, circular rules, which typically use inductive arguments. Although effective in scaling up verification, the applicability of these rules has been limited by the manual effort involved in defining the assumptions.The project addresses the automation of the assumption discovery process in the context of existing circular rules and of new rules, developed as needed. Abstraction and learning techniques are used to iteratively build assumptions and refine them based on counterexamples obtained from checking components separately. The algorithms developed incorporate 3-valued reasoning to allow for more precise yet concise assumptions. The techniques aim at increasing the assurance of general-purpose concurrent and distributed software, by scaling up existing verification techniques through novel automated circular compositional reasoning. Two specific application areas are investigated, namely UML-based software and security protocols; both these areas can highly benefit from compositional reasoning.