Formal Methods in the Field (FMitF)

View Guidelines

20-613

Important Information for Proposers

A revised version of the NSF Proposal & Award Policies & Procedures Guide (PAPPG) (NSF 22-1), is effective for proposals submitted, or due, on or after October 4, 2021. Please be advised that, depending on the specified due date, the guidelines contained in NSF 22-1 may apply to proposals submitted in response to this funding opportunity.

Synopsis

The Formal Methods in the Field (FMitF) program aims to bring together researchers in formal methods with researchers in other areas of computer and information science and engineering to jointly develop rigorous and reproducible methodologies for designing and implementing correct-by-construction systems and applications with provable guarantees. FMitF encourages close collaboration between two groups of researchers. The first group consists of researchers in the area of formal methods, which, for the purposes of this solicitation, is broadly defined as principled approaches based on mathematics and logic to system modeling, specification, design, analysis, verification, and synthesis. The second group consists of researchers in the “field,” which, for the purposes of this solicitation, is defined as a subset of areas within computer and information science and engineering that currently do not benefit from having established communities already developing and applying formal methods in their research. This solicitation limits the field to the following areas that stand to directly benefit from a grounding in formal methods: computer networks, distributed/operating systems, embedded systems, human centered computing, and machine learning. A proposal pursuing a different field area must make a strong case for why the field area of interest is one that does not currently benefit from formal methods but would be a strong candidate for inclusion as a field area.

The FMitF program solicits two classes of proposals:

  • Track I: Research proposals: Each proposal must have at least one Principal Investigator (PI) or co-PI with expertise in formal methods and at least one with expertise in one or more of these fields: computer networks, distributed/operating systems, embedded systems, human centered computing, and machine learning. Proposals are expected to address fundamental contributions to both formal methods and the respective field(s) and should include a proof of concept in the field along with a detailed evaluation plan that discusses intended scope of applicability, trade-offs, and limitations. All proposals are expected to contain a detailed collaboration plan that clearly highlights and justifies the complementary expertise of the PIs/co-PIs in the designated areas and describes the mechanisms for continuous bi-directional interaction. Projects are limited to $750,000 in total budget, with durations of up to four years.
  • Track II: Transition to Practice (TTP) proposals: The objective of this track is to support the ongoing development of extensible and robust formal-methods research prototypes/tools to facilitate usability and accessibility to a larger and more diverse community of users. These proposals are expected to support the development, implementation, and deployment of later-stage successful formal methods research and tools into operational environments in order to bridge the gap between research and practice. A TTP proposal must include a project plan that addresses major tasks and system development milestones as well as an evaluation plan for the working system. Proposals are expected to identify a target user community or organization that will serve as an early adopter of the technology. Collaborations with industry are strongly encouraged. Projects are limited to $100,000 in total budget, with durations of up to 18 months.

The Project Description can be up to 15 pages for Track I proposals, and up to 7 pages for the Track II proposals.

Program Contacts

Nina Amla
Program Director, CISE/CCF
namla@nsf.gov (703) 292-7991 CISE/OAD
Anindya Banerjee
Program Director, CISE/CCF
abanerje@nsf.gov (703) 292-7885 CISE/CCF
Daniel R. Cosley
Program Director, CISE/IIS
dcosley@nsf.gov (703) 292-8832 CISE/IIS
Damian Dechev
Program Director, CISE/CCF
ddechev@nsf.gov (703) 292-8910 CISE/CCF
Wei Ding
Program Director, CISE/IIS
weiding@nsf.gov (703) 292-8017 CISE/IIS
Daniela Oliveira
Program Director, CISE/CNS
doliveir@nsf.gov (703) 292-4352 CISE/CNS
Sandip Roy
Program Director, CISE/CNS
saroy@nsf.gov (703) 292-8950 CISE/CNS
Alexander Sprintson
Program Director, CISE/CNS
asprints@nsf.gov (703) 292-8950 CISE/CNS

Awards Made Through This Program

Browse projects funded by this program
Map of recent awards made through this program