Continuous Reasoning Scaling the Impact of Formal Methods
Continuous Reasoning: Scaling the impact of formal
methods
Peter W. O'Hearn
Facebook and University College London
Abstract
This paper describes work in continuous reasoning , 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 indus-
try. We suggest that advances in continuous reasoning will
allow formal reasoning to scale to more programs, and more
programmers. The paper describes the rationale for contin-
uous reasoning, outlines some success cases from within
industry, and proposes directions for work by the scientic
community.
CCS Concepts • Theory of computation → Program
reasoning; • Software and its engineering;
Keywords Reasoning, Continuous Integration
ACM Reference Format:
Peter W. O'Hearn. 2018. Continuous Reasoning: Scaling the impact
of formal methods. In LICS '18: 33rd Annual ACM/IEEE Symposium
on Logic in Computer Science, July 9–12, 2018, Oxford, United King-
dom. ACM, New York, NY, USA, 13 pages. hps://doi.org/10.1145/
3209108.3209109
1 Introduction
An increasing trend in software engineering is the practice
of continuous development , where a number of programmers
work together sending, sometimes concurrent, updates to a
shared codebase [
35
,
36
]. The code is not viewed as a xed ar-
tifact implementing a nished product, but continues evolv-
ing. In some organizations a codebase in the millions of lines
can undergo rapid modication by thousands of program-
mers. Their work is often backed by a continuous integration
system (CI system) which ensures that the code continues to
be buildable, and that certain tests pass, as the code evolves.
CI-backed development extends and automates aspects of
prior informal practice [
50
]. People naturally develop pro-
grams in an iterative style, where coding and testing feed
back on design, and so on. The iterative model of software
Permission to make digital or hard copies of part or all of this work for
personal or classroom use is granted without fee provided that copies are
not made or distributed for prot or commercial advantage and that copies
bear this notice and the full citation on the rst page. Copyrights for third-
party components of this work must be honored. For all other uses, contact
the owner/author(s).
LICS '18, July 9–12, 2018, Oxford, United Kingdom
© 2018 Copyright held by the owner/author(s).
ACM ISBN 978-1-4503-5583-4/18/07.
hps://doi.org/10.1145/3209108.3209109
development can be contrasted with the waterfall model –
where one proceeds successively from requirements to de-
sign, implementation, testing and deployment. Of course,
the way that humans construct proofs has iterative aspects
as well; e.g., trying to develop a proof of a mathematical the-
orem can cause one to update the statement of the theorem,
try to prove and use a dierent lemma, etc.
The purpose of this paper is to suggest that signicant
benets could accrue if formal reasoning about code can
be done in an automatic continuous fashion which mirrors
the iterative, continuous model of software development.
Then, formal reasoning could more easily scale to many pro-
grams and many programmers. Continuous reasoning views
a codebase as a changing artifact that evolves through modi-
cations submitted by programmers. Continuous reasoning is
done quickly with the code changes, and feeds back informa-
tion to programmers in tune with their workow rather than
outside of it. To be eective a reasoning technique ideally
should scale to a large codebase (sometimes in the millions
of lines of code), but run quickly on code modications (on
the order of low tens of minutes). Then, it can participate as
a bot in the code review system that often accompanies CI.
This paper describes context for work on continuous rea-
soning, but does not set out to be a comprehensive survey.
We have seen continuous reasoning deployed industrially
in ways that have signicantly boosted impact; we mention
several of the prominent cases in the next section, and then
attempt a synthesis. This paper draws on experience work-
ing with the Infer program analysis platform at Facebook,
and we describe that experience and generalize from it. The
purpose of the paper, however, is not to mainly recount what
we have done at Facebook; it is rather to connect a number
of related developments, as well as to tell you some of the
things we don't know . We believe that there is much more
that can be done with continuous formal reasoning, that can
benet the research community (in the form of challeng-
ing and relevant problems) as well as software development
practice (through wider impact of reasoning tools).
2 Continuous Reasoning
Rather than attempt a general denition of continuous rea-
soning, we start with examples. As this paper draws on our
experience at Facebook, it is natural to start there. Then we
mention relevant work from the scientic literature, as well
as experiences from other companies. Finally, we summarize
key aspects of continuous reasoning along with its rationale.
Source: https://docslib.org/doc/4973288/continuous-reasoning-scaling-the-impact-of-formal-methods-peter-w
0 Response to "Continuous Reasoning Scaling the Impact of Formal Methods"
Post a Comment