CISE/CCF: 2012 Summer School on Formal Techniques

在过去的二十年里，形式化建模和验证技术取得了重大进展。像模型检查和定理证明这样的技术现在被用于硬件和软件行业。形式技术也越来越多地被用于科学建模，例如在系统生物学和复杂的网络物理系统的工程中。这项技术面临的最大挑战是缺乏训练有素的用户和开发人员。为了解决这一差距，我们开设了正规技术暑期学校。第一所这样的学校于2011年夏天在加利福尼亚州阿瑟顿的门罗学院举行，得到了国家科学基金会和SRI国际的支持。这所学校吸引了80名兴趣各异、背景各异的学员。这些讲座非常严格，涵盖了形式技术的范围，包括静态分析、模型检查、定理证明、不变量生成、成分验证和系统生物学。该学院的第二版建立在第一版的成功基础上，培养了对正式方法有着浓厚兴趣的年轻研究人员组成的紧密联系的社区。

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.