A fully verified container library
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 correct...
| Main Authors: | , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | English |
| Published: |
Springer-Verlag
2018
|
| Online Access: | http://hdl.handle.net/1721.1/117422 https://orcid.org/0000-0001-5571-173X |
| _version_ | 1826188884471447552 |
|---|---|
| author | Tschannen, Julian Furia, Carlo A. Polikarpova, Nadezhda |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Tschannen, Julian Furia, Carlo A. Polikarpova, Nadezhda |
| author_sort | Tschannen, Julian |
| collection | MIT |
| description | 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 EiffelBase2: 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, 8400 LOC) is possible with moderate annotation overhead (1.4 lines of specification per LOC) and good performance (0.2 s per method on average). Keywords: Deductive verification; SMT; Object-oriented software; Containers; AutoProof |
| first_indexed | 2024-09-23T08:06:12Z |
| format | Article |
| id | mit-1721.1/117422 |
| institution | Massachusetts Institute of Technology |
| language | English |
| last_indexed | 2024-09-23T08:06:12Z |
| publishDate | 2018 |
| publisher | Springer-Verlag |
| record_format | dspace |
| spelling | mit-1721.1/1174222022-09-30T07:33:17Z A fully verified container library Tschannen, Julian Furia, Carlo A. Polikarpova, Nadezhda Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Polikarpova, Nadezhda 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 EiffelBase2: 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, 8400 LOC) is possible with moderate annotation overhead (1.4 lines of specification per LOC) and good performance (0.2 s per method on average). Keywords: Deductive verification; SMT; Object-oriented software; Containers; AutoProof 2018-08-20T17:56:27Z 2018-08-20T17:56:27Z 2017-09 2017-06 2018-08-18T03:40:11Z Article http://purl.org/eprint/type/JournalArticle 0934-5043 1433-299X http://hdl.handle.net/1721.1/117422 Polikarpova, Nadia et al. “A Fully Verified Container Library.” Formal Aspects of Computing 30, 5 (September 2017): 495–523 https://orcid.org/0000-0001-5571-173X en https://doi.org/10.1007/s00165-017-0435-1 Formal Aspects of Computing Creative Commons Attribution http://creativecommons.org/licenses/by/4.0/ The Author(s) application/pdf Springer-Verlag Springer London |
| spellingShingle | Tschannen, Julian Furia, Carlo A. Polikarpova, Nadezhda A fully verified container library |
| title | A fully verified container library |
| title_full | A fully verified container library |
| title_fullStr | A fully verified container library |
| title_full_unstemmed | A fully verified container library |
| title_short | A fully verified container library |
| title_sort | fully verified container library |
| url | http://hdl.handle.net/1721.1/117422 https://orcid.org/0000-0001-5571-173X |
| work_keys_str_mv | AT tschannenjulian afullyverifiedcontainerlibrary AT furiacarloa afullyverifiedcontainerlibrary AT polikarpovanadezhda afullyverifiedcontainerlibrary AT tschannenjulian fullyverifiedcontainerlibrary AT furiacarloa fullyverifiedcontainerlibrary AT polikarpovanadezhda fullyverifiedcontainerlibrary |