Long gone are the days when program verification was a task
carried out merely by hand with paper and pen. For one, we
are increasingly interested in proving actual program
artifacts, not just abstractions thereof or core algorithms.
The programs we want to verify today are thus longer,
including whole classes and modules. As we consider larger
programs, the number of cases to be considered in a proof
increases. The creative and insightful parts of a proof can
easily be lost in scores of mundane cases. Another problem
with paper-and-pen proofs is that the features of the
programming languages we employ in these programs are
plentiful, including object-oriented organizations of data,
facilities for specifying different control flow for rare
situations, constructs for iterating over the elements of a
collection, and the grouping together of operations into
atomic transactions. These language features were designed
to facilitate simpler and more natural encodings of
programs, and ideally they are accompanied by simpler proof
rules. But the variety and increased number of these
features make it harder to remember all that needs to be
proved about their uses. As a third problem, we have come
to expect a higher degree of rigor from our proofs. A proof
carried out or replayed by a machine somehow gets more
credibility than one that requires human intellect to
understand.

@Book{KeYBook2007,
editor = {Bernhard Beckert and Reiner H\"ahnle and Peter H. Schmitt},
title = {Verification of Object-Oriented Software: The {\KeY} Approach},
series = {Lecture Notes in Computer Science},
volume = {4334},
publisher = {Springer},
year = {2007},
doi = {10.1007/978-3-540-69061-0},
abstract = {Long gone are the days when program verification was a task
carried out merely by hand with paper and pen. For one, we
are increasingly interested in proving actual program
artifacts, not just abstractions thereof or core algorithms.
The programs we want to verify today are thus longer,
including whole classes and modules. As we consider larger
programs, the number of cases to be considered in a proof
increases. The creative and insightful parts of a proof can
easily be lost in scores of mundane cases. Another problem
with paper-and-pen proofs is that the features of the
programming languages we employ in these programs are
plentiful, including object-oriented organizations of data,
facilities for specifying different control flow for rare
situations, constructs for iterating over the elements of a
collection, and the grouping together of operations into
atomic transactions. These language features were designed
to facilitate simpler and more natural encodings of
programs, and ideally they are accompanied by simpler proof
rules. But the variety and increased number of these
features make it harder to remember all that needs to be
proved about their uses. As a third problem, we have come
to expect a higher degree of rigor from our proofs. A proof
carried out or replayed by a machine somehow gets more
credibility than one that requires human intellect to
understand.}
}