2014 SAT/SMT Summer School

形式化方法在过去十年中取得了重大进展，现在形成了硬件和软件行业形式化保证的支柱。这些技术的基础是对系统属性进行有效推理的能力，通常是将属性描述为约束满足问题，并将推理委托给约束求解器。目前使用的最常见的约束推理引擎是可满足性（模理论）求解器（SAT和SMT）。作为一个快速发展的领域，缺乏训练有素的用户和研究人员来维持和进一步推进该领域。SAT/SMT暑期学校通过让年轻的研究人员熟悉尖端的求解器技术及其应用来解决这个问题。SAT/SMT暑期学校通过让年轻的研究人员熟悉尖端的求解器技术及其应用来解决这个问题。学校的讲师都是世界知名的专家，三天的聚会让学生有机会与这些专家讨论讲座主题，自己的研究，以及面临的挑战和未来的方向。材料涵盖严格，深度和广度，但以适合学生观众的速度，使学校成为一个独特的地方，传播新的研究，以未来的用户和研究人员。

Formal methods have made significant advances during the last decade, and now form the backbone of formal assurance across hardware and software industries. Underlying many of these techniques is the capability to effectively reason about system properties, often by describing the properties as constraint satisfaction problems and delegating the reasoning to a constraint solver. The most common constraint reasoning engines in use today are satisfiability (modulo theories) solvers (SAT and SMT). As a rapidly developing field, there is a lack of highly trained users and researchers that will sustain and further advance the field. The SAT/SMT summer school addresses this issue by familiarizing young researchers with cutting-edge solver technologies and their applications.The SAT/SMT summer school addresses this issue by familiarizing young researchers with cutting-edge solver technologies and their applications. The lecturers at the school are world-renown experts, and the three day gathering gives the students the opportunity to discuss the lecture topics, their own research, and the challenges and future directions with these experts. The material is covered rigorously, with depth and breadth, but at a pace appropriate for a student audience, making the school a unique place for disseminating new research to the future users and researchers.