CISE/SHF: Summer School on Formal Techniques

Software plays an increasingly significant role in the infrastructure supporting transportation, manufacturing, entertainment, agriculture, and government. The safety and security of this infrastructure depends critically on the level of rigor with which software-based systems are designed and verified. Formal modeling and verification technology has made significant advances in the last two decades. Techniques like model checking and theorem proving are now used in both the hardware and software industries. Formal techniques are also increasingly being used in scientific modeling, for example in systems biology and in the engineering of complex cyber-physical systems. The biggest challenge facing this technology is the lack of trained users and developers of this technology. The annual Summer School in Formal Techniques addresses this training gap by exposing students to cutting-edge research and technology. The project's novelties are in backing the lectures with hands-on laboratories where the students gain first-hand experience with the technology. To gauge the project's impact, the program will collect valuable feedback from the students on the impact of the summer school lectures on their education and research. The data has shown a strong indication that the lectures cover material that is new and deeply useful to the students, and the laboratory work builds confidence in the use of specific formal techniques. The school also helps to build a social network among the students from which they can draw motivation and support. The lectures in these schools cover the spectrum of formal techniques; e.g., static analysis, dynamic analysis, model checking, theorem proving, invariant generation, program synthesis, software specification, program verification, and compositional verification, as well as applications in computer security, systems biology, and cyber-physical systems. The lectures at the summer school span a variety of advanced verification techniques, problem domains, and state-of-the-art tools from both academia and industry. The first-hand use of these tools in interactive laboratory sessions is helping the students integrate these technologies into their own research. It is also helping seed a community around these individual tools. 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.