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.
