CISE/SHF: Summer School on Formal Techniques

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

• 批准号: 2308981
• 负责人: Natarajan Shankar
• 金额: $ 49.95万
• 依托单位: SRI International
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-04-01 至 2025-12-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2308981&HistoricalAwards=false
• 关键词: CISE; SHF; Summer; 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.

软件在支持交通、制造、娱乐、农业和政府的基础设施中发挥着越来越重要的作用。这一基础设施的安全性和保障性在很大程度上取决于基于软件的系统设计和验证的严格程度。形式化建模和验证技术在过去的二十年里取得了显著的进步。像模型检查和定理证明这样的技术现在在硬件和软件行业都有应用。形式化技术也越来越多地用于科学建模，例如系统生物学和复杂的网络物理系统的工程。这项技术面临的最大挑战是缺乏训练有素的用户和开发人员。一年一度的正规技术暑期学校通过让学生接触尖端研究和技术来解决这一培训缺口。该项目的新颖之处在于通过动手实验室来支持讲座，学生们在实验室中获得了使用该技术的第一手经验。为了衡量该项目的影响，该计划将收集学生对暑期学校讲座对他们的教育和研究的影响的宝贵反馈。这些数据表明，讲座涵盖了对学生非常有用的新材料，实验室工作建立了使用特定形式技术的信心。学校还帮助学生建立一个社会网络，他们可以从中获得动力和支持。这些学校的讲座涵盖了正式技术的范围;例如，静态分析、动态分析、模型检验、定理证明、不变量生成、程序综合、软件规范、程序验证和组合验证，以及在计算机安全、系统生物学和网络物理系统中的应用。暑期学校的讲座涵盖了来自学术界和工业界的各种先进的验证技术、问题领域和最先进的工具。在互动实验室会议中使用这些工具的第一手资料有助于学生将这些技术融入自己的研究中。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。