Full Functional Verification of Linked Data Structures

paper ps   
We present the first verification of full functional correctness for a range of linked data structure implementations, including mutable lists, trees, graphs, and hash tables. Specifically, we present the use of the Jahob verification system to verify formal specifications, written in classical higher-order logic, that completely capture the desired behavior of the Java data structure implementations (with the exception of properties involving execution time and/or memory consumption). Given that the desired correctness properties include intractable constructs such as quantifiers, transitive closure, and lambda abstraction, it is a challenge to successfully prove the generated verification conditions. Our verification system uses 'integrated reasoning' to split each verification condition into a conjunction of simpler subformulas, then apply a diverse collection of specialized decision procedures, first-order theorem provers, and, in the worst case, interactive theorem provers to prove each subformula. Techniques such as replacing complex subformulas with stronger but simpler alternatives, exploiting structure inherently present in the verification conditions, and, when necessary, inserting verified lemmas and proof hints into the imperative source code make it possible to seamlessly integrate all of the specialized decision procedures and theorem provers into a single powerful integrated reasoning system. By appropriately applying multiple proof techniques to discharge different subformulas, this reasoning system can effectively prove the complex and challenging verification conditions that arise in this context.

Citation

Karen Zee, Viktor Kuncak, and Martin Rinard. Full functional verification of linked data structures. In ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2008. see also [61].

BibTex Entry

@inproceedings{ZeeETAL08FullFunctionalVerificationofLinkedDataStructures,
  title = {Full Functional Verification of Linked Data Structures},
  author = {Karen Zee and Viktor Kuncak and Martin Rinard},
  booktitle = {ACM SIGPLAN Conf. Programming Language Design and Implementation  (PLDI)},
  abstract = {
We present the first verification of full functional correctness
for a range of linked data structure implementations, including
mutable lists, trees, graphs, and hash tables.  Specifically, we
present the use of the Jahob verification system to verify formal
specifications, written in classical higher-order logic, that
completely capture the desired behavior of the Java data structure
implementations (with the exception of properties involving execution
time and/or memory consumption). Given that the desired correctness
properties include intractable constructs such as quantifiers,
transitive closure, and lambda abstraction, it is a challenge to
successfully prove the generated verification conditions.

Our verification system uses 'integrated reasoning' to
split each verification condition into a conjunction of simpler
subformulas, then apply a diverse collection of specialized decision
procedures, first-order theorem provers, and, in the worst case,
interactive theorem provers to prove each subformula. Techniques such
as replacing complex subformulas with stronger but simpler
alternatives, exploiting structure inherently present in the
verification conditions, and, when necessary, inserting verified
lemmas and proof hints into the imperative source code make it
possible to seamlessly integrate all of the specialized decision
procedures and theorem provers into a single powerful integrated
reasoning system. By appropriately applying multiple proof techniques
to discharge different subformulas, this reasoning system can
effectively prove the complex and challenging verification conditions
that arise in this context.
},
  note = {see also \cite{Kuncak07DecisionProceduresModularDataStructureVerification}},
  year = 2008
}