NSF Student Travel Grant for 2018 SAT/SMT/AR Summer School (SSA)

2018 年 SAT/SMT/AR 暑期学校 (SSA) NSF 学生旅费补助

• 批准号: 1832999
• 负责人: Andrew Reynolds
• 金额: $ 1.5万
• 依托单位: University of Iowa
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-06-01 至 2020-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1832999&HistoricalAwards=false
• 关键词: NSF; Student; Travel; Grant; 2018

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. Due to their practical effectiveness and robust scalability, the most common constraint reasoning engines in use today are satisfiability (modulo theories) solvers (SAT and SMT). This award will provide travel grants for US-based students to attend the SAT/SMT summer school to be held in Manchester, UK, July 3-6, preceding the Federated Logic Conference (FLoC 2018).The SAT/SMT Summer School allows students to learn about the techniques underlying modern SAT and SMT solvers, and gives them a broad view of the field with many practical applications. Since the school is a separate event, in a less formal setting, the students have the opportunity to discuss the school topics (with lab assignments), discuss their own research ideas, and interact closely both with their peers and the leaders in the field. The summer school ignites the transfer and dissemination of knowledge that will lead to superior technology, better users, and exciting and far-reaching applications.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

在过去的十年中，正式方法取得了重大进展，现在形成了跨硬件和软件行业的正式保证的支柱。其中许多技术的基础是有效地对系统属性进行推理的能力，通常是通过将属性描述为约束满足问题并将推理委托给约束求解器来实现的。由于其实用的有效性和强大的可扩展性，目前使用的最常见的约束推理引擎是可满足性(模理论)求解器(SAT和SMT)。该奖项将为美国学生提供旅行津贴，让他们参加7月3日至6日在英国曼彻斯特举行的联合逻辑会议(Floc 2018)之前的SAT/SMT暑期班。SAT/SMT暑期班允许学生学习现代SAT和SMT解算器背后的技术，并让他们对具有许多实际应用的领域有一个广泛的看法。由于学校是一个单独的活动，在一个不那么正式的环境中，学生们有机会讨论学校主题(包括实验室作业)，讨论他们自己的研究想法，并与他们的同行和该领域的领导者密切互动。暑期班激发了知识的转移和传播，将导致更好的技术、更好的用户以及令人兴奋和深远的应用。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。