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

CPA-SEL：使用假设保证推理进行实用类型状态验证

• 批准号: 0811592
• 负责人: Jonathan Aldrich
• 金额: --
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2008
• 资助国家: 美国
• 起止时间: 2008-09-01 至 2011-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0811592&HistoricalAwards=false
• 关键词: CPA; SEL; Practical; Typestate; Verification

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.

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