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

Worcester Polytechnic Institute, Worcester MA

Investigators

Abstract

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.