CISE/CCF: 2012 Summer School on Formal Techniques

CISE/CCF：2012 年形式技术暑期学校

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

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, as 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. To address this gap, we started the Summer School in Formal Techniques. The first such school was held in the Summer of 2011 at Menlo College in Atherton, California, with support from the National Science Foundation and SRI International. The school attracted 80 participants with a diverse range of interests and backgrounds. The lectures were rigorous and covered the spectrum of formal techniques including static analysis, model checking, theorem proving, invariant generation, compositional verification, and systems biology. The second edition of the school builds on the success of the first one to develop a well-knit community of young researchers with a deep interest in formal methods.

形式化建模和验证技术在过去的二十年里取得了显著的进步。 像模型检查和定理证明这样的技术现在在硬件和软件行业都有应用。 形式化技术也越来越多地用于科学建模，例如系统生物学和复杂的网络物理系统的工程。 这项技术面临的最大挑战是缺乏训练有素的用户和开发人员。 为了弥补这一差距，我们开始了正式技术暑期学校。 第一所这样的学校于2011年夏天在加州阿瑟顿的门洛学院举办，得到了国家科学基金会和SRI国际的支持。 学校吸引了80名具有不同兴趣和背景的参与者。 这些讲座是严格的，涵盖了形式化技术的范围，包括静态分析，模型检查，定理证明，不变式生成，组合验证和系统生物学。 学校的第二版建立在第一个成功的基础上，发展了一个对正式方法有浓厚兴趣的年轻研究人员的紧密社区。