Research

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.

To apply

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.

Additional information

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 closed.
• Notifications will be sent by email to selected applicants in September, 2018.