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.