CPA-SEL: Practical Typestate Verification with Assume-Guarantee Reasoning

CCF-0811592CPA-SEL：带假设保证推理的实用类型状态验证Jonathan Aldrich现代软件开发的主要困难之一是正确使用软件库和框架。该项目正在开发新的工具来验证库和框架的临时使用属性，捕获对对象的允许调用顺序以及进行调用时该对象的状态。该项目解决的关键验证挑战包括继承和子类型化、从库到客户端的递归回调以及指向库对象的多个别名指针。该项目正在将假设-保证推理应用于这些挑战：允许多个客户端协作访问一个对象，并就如何使用该对象达成协议，以便每个客户端可以安全地对其他客户端进行假设？行为，并反过来每个客户端保证它不会侵犯其他客户端？假设。该项目正在开发该方法背后的基本理论，但也在构建实用工具，并通过科学案例研究在现实世界的应用程序和图书馆上对它们进行评估。如果成功，该项目将提高软件工程师使用库的生产率，减少软件中的缺陷数量，并帮助学生了解轻量级软件验证工具的理论和实践。

CCF-0811592CPA-SEL: Practical Typestate Verification with Assume-Guarantee ReasoningJonathan AldrichOne of the main difficulties in modern software development is using software libraries and frameworks correctly. This project is developing new tools to verify temporal usage properties of libraries and frameworks, capturing the permitted ordering of calls to an object and the state of that object when the calls are made.Key verification challenges addressed by this project include inheritance and subtyping, recursive callbacks from a library into the client and back, and multiple aliased pointers to a library object. The project is applying assume-guarantee reasoning to these challenges: allowing multiple clients to access an object cooperatively, with an agreement about how that object should be used so that each client can safely make assumptions about other clients? behavior, and in turn each client guarantees that it will not violate other clients? assumptions.The project is developing the underlying theory behind the approach, but is also building practical tools and evaluating them on real-world applications and libraries through scientific case studies. If successful, the project will increase the productivity of software engineers when using libraries, reduce the number of defects in software, and help students to learn about the theory and practice of lightweight software verification tools.