CAREER: A Computational Infrastructure for Timing Diagrams in Computer-Aided Verification

本研究建议利用时序图来改进系统设计的形式化验证。形式验证是一种有价值的调试技术，但可伸缩性和可用性问题阻碍了它的广泛使用。时序图承诺缓解这两个问题，因为它们来自设计社区，并产生比现有验证符号更严格的计算模型。建议的研究(1)使用捕捉现实验证问题所需的构造来增强时序图，以及(2)开发可扩展的和组合的验证技术，该技术利用时序图的独特计算特性来提高可伸缩性和效率。该项目的教育方面侧重于通过课程改进和实践项目的结合，提高学生对系统设计进行建模和推理的技能。这些研究和教育目标的结合使正式验证在现实世界的设计实践中得到更广泛的采用和更大的可行性。

This research proposes to exploit timing diagrams to improve formal verification for system designs. Formal verification is a valuable debugging technique, but scalability and usability problems hinder its broader use. Timing diagrams promise to alleviate both problems because they arise from the design community and engender more restrictive computational models than existing verification notations. The proposed research (1) enhances timing diagrams with constructs needed to capture realistic verification problems and (2) develops scalable and compositional verification techniques that exploit timing diagrams' unique computational characteristics for improved scalability and efficiency. The educational aspect of this project focuses on increasing students' skills in modeling and reasoning about system designs through a combination of curricular enhancements and hands-on projects. The combination of these research and educational objectives enables wider adoption and increased feasibility of formal verification in real-world design practice.