The comprehensive functionality and nontrivial design of realistic general- purpose container libraries pose challenges to formal verification that go beyond those of individual benchmark problems mainly targeted by the state of the art. We present our experience verifying the full functional correctness of Eiffel- Base2: a container library offering all the features customary in modern language frameworks, such as external iterators, and hash tables with generic mutable keys and load balancing. Verification uses the automated deductive verifier AutoProof, which we extended as part of the present work. Our results indicate that verification of a realistic container library (135 public methods, 8,400 LOC) is possible with moderate annotation overhead (1.4 lines of specification per LOC) and good performance (0.2 seconds per method on average).
CITATION STYLE
Polikarpova, N., Tschannen, J., & Furia, C. A. (2015). A fully verified container library. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9109, pp. 414–434). Springer Verlag. https://doi.org/10.1007/978-3-319-19249-9_26
Mendeley helps you to discover research relevant for your work.