2014 SAT/SMT Summer School

2014年SAT/SMT暑期学校

• 批准号: 1440070
• 负责人: Clark Barrett
• 金额: $ 2万
• 依托单位: New York University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2014
• 资助国家: 美国
• 起止时间: 2014-04-01 至 2015-03-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1440070&HistoricalAwards=false
• 关键词: 2014; SAT; SMT; Summer

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.

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