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.