CISE/CCF: 2014 Summer School on Formal Techniques

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

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

Formal verification techniques such as model checking, satisfiability solving, theorem proving, and static analysis have matured rapidly in recent years. These techniques have a number of important applications ranging from the modeling and analysis of biological and cyber-physical systems to the verification of the safety and security of complex software systems. The Summer School on Formal Techniques trains students in the principles and practice of formal verification, with a strong emphasis on the hands-on use and development of this technology. It primarily targets graduate students and young researchers who are interested in using verification technology in their own research in fields such as computing, engineering, biology, and mathematics. Students at the school are given the opportunity to experiment with the tools and techniques presented in the lectures.The 2014 edition of the Summer School is the fourth in the series takes place during May 19-23, 2014. Topics covered in this school include logic, formalization, interactive theorem proving, SAT and SMT solving, model checking, program semantics, modeling and verification of security protocols, and software reliability. The students cooperate in solving challenging problems while learning to use cutting-edge tools and techniques.

形式化验证技术，如模型检查，可满足性求解，定理证明和静态分析，近年来迅速成熟。 这些技术具有许多重要的应用，从生物和网络物理系统的建模和分析到复杂软件系统的安全性和安全性的验证。 形式化技术暑期学校培训学生形式化验证的原则和实践，特别强调这种技术的实际使用和开发。 它主要针对研究生和年轻研究人员，他们有兴趣在计算，工程，生物和数学等领域的研究中使用验证技术。 在学校的学生有机会与讲座中提出的工具和技术进行实验。2014年版的暑期学校是在2014年5月19日至23日举行的系列第四次。 这个学校涵盖的主题包括逻辑，形式化，交互式定理证明，SAT和SMT解决，模型检查，程序语义，安全协议的建模和验证，以及软件可靠性。 学生合作解决具有挑战性的问题，同时学习使用尖端的工具和技术。