CISE/SHF: Summer School on Formal Techniques

CISE/SHF：形式技术暑期学校

• 批准号: 1822342
• 负责人: Natarajan Shankar
• 金额: $ 29.94万
• 依托单位: SRI International
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-04-01 至 2023-03-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1822342&HistoricalAwards=false
• 关键词: CISE; SHF; Summer; Formal; Techniques

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.

正式验证涵盖了广泛的技术范围，这些技术在学术界被广泛研究，并在工业中经常使用。关于这些技术的知识传播的任何加速都将导致更先进的技术、更好的用户以及令人兴奋和深远的应用。这项资助在2018年至2020年期间组织了一所为期三年的正式技术暑期学校，让学生学习正式建模和验证方面的前沿技术。讲座内容严谨，涵盖了各种形式技术，包括静态分析、模型检查、定理证明、不变量生成、组合验证、安全性和系统生物学。讲座由动手实验支持。与会者在学校讨论自己的研究思路，并与讲师和其他学生密切互动。以往的暑期学校在向来自不同研究领域的学生传授理论知识和实践技能方面产生了重大的广泛影响。这些暑期学校受到了参与者的热烈欢迎，并帮助建立了一个由年轻研究人员组成的紧密联系的社区。组织者收集了学生们关于暑期学校讲座对他们的教育和研究的影响的宝贵反馈，并对过去参加这些活动的人进行了纵向研究，以评估长期影响。许多反馈是积极的，并且有强烈的迹象表明，讲座涵盖了对学生来说是新的和有用的材料，并且实验室工作建立了对使用特定形式技术的信心。讲座、软件工具和其他课程材料可以从以前的暑期学校网站上获得。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。