CISE/SHF: Summer School on Formal Techniques

正式核查涵盖了学术界广泛研究并在工业界经常使用的各种技术。这些技术知识的传播速度的任何加快都将带来上级技术、更好的用户以及令人兴奋和意义深远的应用。该补助金在2018 - 2020年期间组织了为期三年的形式技术暑期学校，让学生学习形式建模和验证的尖端技术。讲座是严格的，涵盖了形式化技术的频谱，包括静态分析，模型检查，定理证明，不变式生成，组合验证，安全和系统生物学。讲座由动手实验室支持。参加者在学校讨论自己的研究想法，并与讲师和其他学生密切互动。以往的暑期学校在向来自不同研究领域的学生传授理论知识和实践技能方面产生了广泛的影响。这些暑期学校受到参与者的热烈欢迎，并帮助发展了一个由年轻研究人员组成的紧密社区。组织者从学生那里收集了关于暑期学校讲座对他们的教育和研究的影响的宝贵反馈，以及对这些活动的过去参与者的纵向研究，以评估长期影响。大部分的反馈是积极的，有一个强烈的迹象表明，讲座涵盖的材料是新的和有用的学生，和实验室工作建立在使用特定的正式技术的信心。讲座，软件工具，和其他课程材料可从以前的暑期学校网站。这个奖项反映了NSF的法定使命，并已被认为是值得通过使用基金会的智力价值和更广泛的影响审查标准进行评估的支持。

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.