Full functional verification of linked data structures Export

@inproceedings{citeulike:4056843, 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.}, address = {New York, NY, USA}, author = {Zee, Karen and Kuncak, Viktor and Rinard, Martin}, booktitle = {PLDI '08: Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation}, citeulike-article-id = {4056843}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1375581.1375624}, citeulike-linkout-1 = {http://dx.doi.org/10.1145/1375581.1375624}, doi = {10.1145/1375581.1375624}, isbn = {978-1-59593-860-2}, keywords = {788, aliases, jahob, verification}, location = {Tucson, AZ, USA}, pages = {349--361}, posted-at = {2009-02-15 20:22:59}, priority = {3}, publisher = {ACM}, title = {Full functional verification of linked data structures}, url = {http://dx.doi.org/10.1145/1375581.1375624}, year = {2008} }

TY - CONF ID - citeulike:4056843 L3 - citeulike-article-id:4056843 N2 - 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. CY - Tucson, AZ, USA SN - 978-1-59593-860-2 AD - New York, NY, USA EP - 361 TI - Full functional verification of linked data structures PB - ACM T2 - PLDI '08: Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation SP - 349 KW - 788 KW - aliases KW - jahob KW - verification AU - Zee, Karen AU - Kuncak, Viktor AU - Rinard, Martin PY - 2008/// UR - http://dx.doi.org/10.1145/1375581.1375624 ER -