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.