Cise/SHF: summer school on formal techniques

This Project Grant from the National Science Foundation's Computer and Information Science and Engineering program, CFDA 47.070, provides $499,526 to Sri International for a Summer School on Formal Techniques from April 1, 2023 to December 31, 2025.

The Summer School addresses the lack of trained users and developers in formal modeling and verification techniques, which are increasingly critical to ensuring the safety and security of software-reliant infrastructure. It exposes students to cutting-edge research through lectures covering a spectrum of formal methods, applications, verification tools, and state-of-the-art developments from academia and industry. Students gain hands-on experience through interactive laboratory sessions using these tools and techniques. Feedback collected has indicated the lectures cover new, useful material and labs build confidence in specific formal methods. The School also fosters collaboration within an emerging community.

Abstract

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.