FMitF: Formal Methods in the Field Bootcamp

形式化方法是计算机科学的一个分支，它寻求通过数学工具和技术严格描述计算机软件和硬件的行为。形式方法的工具在规模和成熟度方面迅速增长，但与此同时，数字应用程序本身也达到了成本、复杂性和关键程度的水平，这就要求甚至需要由形式工具支持的高级严格设计方法。在过去的几年里，在编译器、操作系统、文件系统、实时系统和网络人类系统等领域中，正式工具的采用迅速增加。该奖项组织了实地正式方法训练营(FMitF)，目的是培训学生在特定领域应用正式技术的最新进展，以便他们能够开展雄心勃勃的项目。研讨会定于2020年5月的最后一周举行，紧接着第十届正规技术暑期学校(SSFT)。FMitF训练营旨在创建一个处于正式方法应用前沿的自给自足的研究人员社区。FMitF训练营在领域专家、正式方法专家和学生研究人员之间建立了合作伙伴关系，以在这些单独的领域开发高影响力、尖端的想法和应用程序。FMitF训练营是学生开发经过验证的构件的机会，包括算法、库、基础设施和应用程序。这些构件可以为更雄心勃勃的研究项目提供种子，这些项目承担着创建具有清晰和精确规范的可信应用程序的挑战。SSFT受到了与会者的热烈欢迎，并帮助发展了一个紧密联系的年轻研究人员社区。与SSFT共同举办研讨会，可以更容易地吸引已经接受过培训的学生参加FMitF训练营。训练营组织者将寻求通过鼓励计算机领域代表不足的群体参加来扩大参与。这一奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Formal methods are a branch of computer science that seek to rigorously characterize the behavior of computer software and hardware through mathematical tools and techniques. Formal methods' tools have been rapidly gaining in scale and maturity, but at the same time, digital applications themselves are reaching a level of cost, complexity, and criticality that call out for even advanced rigorous design methodologies supported by formal tools. The past few years have seen rapidly growing adoption of formal tools in domains such as compilers, operating systems, file systems, real-time systems, and cyber-human systems, among others. This award organizes a Bootcamp on Formal Methods in the Field (FMitF) with the objective of training students in the latest advances in the applications of formal techniques in specific domains so that they can undertake ambitious projects. The workshop is scheduled for the last week of May 2020, immediately following the tenth Summer School on Formal Techniques (SSFT). The FMitF Bootcamp aims to create a self-sustaining community of researchers at the cutting-edge of the application of formal methods. The FMitF Bootcamp creates a partnership between domain experts, formal methods experts, and student researchers for developing high-impact, cutting-edge ideas and applications in these individual domains. The FMitF bootcamp is an opportunity for students to develop verified artifacts including algorithms, libraries, infrastructure, and applications. These artifacts can seed more ambitious research projects that take on the challenge of creating trustworthy applications with clear and precise specifications. The SSFT has been received enthusiastically by the participants, and helped develop a well-knit community of young researchers. Co-locating the workshop with the SSFT makes it easier to attract already trained students to the FMitF Bootcamp. The Bootcamp organizers will seek to broaden participation by encouraging attendance from under-represented groups in the computing domain.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.