Formal reasoning about programs is one of the oldest dreams in computer science. At Facebook, our teams have been working on applying formal reasoning in practice in the last five years.
In this time, one approach stands out as having made the biggest difference in applying formal methods at scale: continuous reasoning. Continuous reasoning is where formal reasoning about a (changing) codebase is done in a fashion which mirrors the iterative, continuous model of software development that is increasingly practiced in industry (which stands in contrast to the more static waterfall model). It views a codebase not as a fixed entity, but as a changing artifact that evolves through modifications submitted by programmers; ideally, reasoning is done quickly with the code changes, and feeds back information to programmers in tune with their workflow rather than outside of it.
Facebook is pleased to invite university faculty to respond to this call for research proposals: We anticipate awarding a total of 5 awards in the $50,000 range.
While we have seen benefits from continuous reasoning, industrial deployments are going beyond the usual assumptions of the scientific field. This presents an opportunity to the scientist to re-examine assumptions and, consequently, provide a better basis for the engineering of reasoning tools in the future. In particular, we have found that tools which adopt an Open World Assumption rather than Closed World (whole program) have increased opportunities to mirror the way that software is developed, but their foundations are not as clear. We are interested in proposals that address fundamental problems in the area, including:
- Development of compositional versions of existing whole-program analysis techniques (interpolation, CEGAR, fuzz, concolic, numeric abstract domains…) demonstrating scalability proportional to the code changes and addressing the question of effective signal.
- Addressing fundamental problems for mostly-automatic or interactive verifiers concerning the effort of obtaining specs or the effort of maintaining a proof over time.
- Assumptions for techniques that can be applied at diff-submission or code-review time (e.g., 15mins/diff on large code bases). Assumptions for build or IDE-time (seconds/diff).
- Abstract theory for program analysis addressing efficiency and open world challenges of continuous reasoning.
The paper, Continuous Reasoning Scaling the Impact of Formal Methods, published at LICS’18 outlines some of these challenges in more detail. These topics are given as an indication, and we are open to proposals attacking other problems than those described.
We aim to make the process light touch to reduce the burden of preparing an application. Applicants should submit a proposal consisting of a (maximum of) 2 pages. Proposals should focus on the scientific contribution and means of (experimental or theoretical) evaluation, together with a budget overview (maximum of $50,000 USD), outlining how the proposed funding will be used. In place of proposer CVs please simply include links to DBLP and/or Google Scholar™ pages for the proposers.
Facebook will organize a one-day conference at which recipients will attend, present and discuss their work.
Successful awardees will be listed on the Facebook Research website and will be encouraged to openly publish any findings/insights from their work.
Galois Inc have offered to provide some free consulting to help teams demonstrate their research on open-source CI infrastructure. Galois is a research consultancy with a focus on transitioning academic ideas to industrial practice.
Award amount: Awards up to $50,000 USD will be given. Payment will be made to the proposer’s host university as an unrestricted gift.
Proposals should include
- Names of the researcher(s) involved in the proposed work with links to their DBLP and/or Google Scholar pages
- Host academic research institution
- Clear and concise statement of the the scientific contribution and routes to eventual deployment
- Indication of any previous or current connections/collaborations with Facebook (in which case please name any Facebook contacts)
- A proposed budget
Timing and dates
- Applications are now open.
- Applications close August 31, 2018, 5pm PST.
- Notifications will be sent by email to selected applicants in September, 2018.