Verification of Object-Oriented Software: The KeY Approach

Book

Editor(s):Bernhard Beckert, Reiner Hähnle, and Peter H. Schmitt
Publisher:Springer
Series:Lecture Notes in Computer Science
Volume:4334
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.

BibTeX

@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.}
}