Fisler's NSF CAREER award
The CS department is very pleased to announce that Prof. Kathi Fisler has won a prestigious NSF CAREER award for her proposal "A Computational Infrastructure for Timing Diagrams in Computer-Aided Verification". The award, worth $370,000 over five years, will support both graduate and undergraduate researchers.
The abstract for the award is as follows
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.