CISE/SHF: Summer School on Formal Techniques

Sri International, Menlo Park CA

Investigators

Abstract

Formal verification covers a wide range of technologies that are widely studied in academia and routinely used in industry. Any acceleration in the diffusion of knowledge about these techniques will lead to superior technology, better users, and exciting and far-reaching applications. This grant organizes a Summer School on Formal Techniques over three years, during 2018 - 2020, for students to learn about cutting-edge techniques in formal modeling and verification. The lectures are rigorous and cover the spectrum of formal techniques including static analysis, model checking, theorem proving, invariant generation, compositional verification, security and systems biology. The lectures are supported by hands-on laboratories. Attendees at the school discuss their own research ideas and interact closely with both the lecturers and other students. The previous summer schools have had a significant broad impact in terms of imparting theoretical knowledge as well as practical skills to the students from many different research areas. These summer schools have been received enthusiastically by the participants, and helped develop a well-knit community of young researchers. The organizers collected valuable feedback from the students on the impact of the summer school lectures on their education and research, as well as longitudinal study across past attendees of these events to evaluate longer-term impacts. Much of the feedback has been positive, and there is a strong indication that the lectures cover material that is new and useful to the students, and the laboratory work builds confidence in the use of specific formal techniques. The lectures, software tools, and other course material are available from the previous summer school web sites. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.