FMitF: Formal Methods in the Field Bootcamp

点击翻译按钮获取中文摘要

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.