乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T19:45:54Z","timestamp":1730317554061,"version":"3.28.0"},"publisher-location":"New York, NY, USA","reference-count":31,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,10,26]],"date-time":"2015-10-26T00:00:00Z","timestamp":1445817600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2015,10,26]]},"DOI":"10.1145\/2846680.2846691","type":"proceedings-article","created":{"date-parts":[[2016,1,29]],"date-time":"2016-01-29T10:05:10Z","timestamp":1454061910000},"page":"57-60","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Some usability hypotheses for verification"],"prefix":"10.1145","author":[{"given":"David J.","family":"Pearce","sequence":"first","affiliation":[{"name":"Victoria University of Wellington, New Zealand"}]}],"member":"320","published-online":{"date-parts":[[2015,10,26]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289504"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/535661"},{"key":"e_1_3_2_1_4_1","volume-title":"Carnegie-Mellon University","author":"King S.","year":"1969","unstructured":"S. King . A Program Verifier. PhD thesis , Carnegie-Mellon University , 1969 . S. King. A Program Verifier. PhD thesis, Carnegie-Mellon University, 1969."},{"key":"e_1_3_2_1_5_1","volume-title":"Reasoned Programming","author":"Broda K.","year":"1994","unstructured":"K. Broda , S. Eisenbach , H. Khoshnevisan , and Steven Vickers . Reasoned Programming . Prentice Hall , 1994 . K. Broda, S. Eisenbach, H. Khoshnevisan, and Steven Vickers. Reasoned Programming. Prentice Hall, 1994."},{"key":"e_1_3_2_1_6_1","unstructured":"Roland Backhouse. Program Construction. Wiley 2003. Roland Backhouse. Program Construction. Wiley 2003."},{"key":"e_1_3_2_1_7_1","volume-title":"An Introduction to Program Verification","author":"Almeida J.B.","year":"2011","unstructured":"J.B. Almeida , M.J. Frade , J.S. Pinto , and S Melo de Sousa . Rigorous Software Development , An Introduction to Program Verification . Springer-Verlag , 2011 . J.B. Almeida, M.J. Frade, J.S. Pinto, and S Melo de Sousa. Rigorous Software Development, An Introduction to Program Verification. Springer-Verlag, 2011."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-27919-5","volume-title":"The Correctness-by-Construction Approach to Programming","author":"Kourie Derrick G.","year":"2012","unstructured":"Derrick G. Kourie and Bruce W. Watson . The Correctness-by-Construction Approach to Programming . Springer , 2012 . Derrick G. Kourie and Bruce W. Watson. The Correctness-by-Construction Approach to Programming. Springer, 2012."},{"key":"e_1_3_2_1_9_1","volume-title":"The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport L.","year":"2002","unstructured":"L. Lamport . Specifying Systems , The TLA+ Language and Tools for Hardware and Software Engineers . Addison-Wesley , 2002 . L. Lamport. Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/602382.602403"},{"key":"e_1_3_2_1_11_1","volume-title":"An interactive program verifier. Ph.D","author":"Deutsch L. Peter","year":"1973","unstructured":"L. Peter Deutsch . An interactive program verifier. Ph.D ., 1973 . L. Peter Deutsch. An interactive program verifier. Ph.D., 1973."},{"key":"e_1_3_2_1_12_1","first-page":"75","volume-title":"Mathematical logic and programming languages","author":"Good D. I.","year":"1985","unstructured":"D. I. Good . Mechanical proofs about computer programs. In Mathematical logic and programming languages , pages 55\u2013 75 , 1985 . D. I. Good. Mechanical proofs about computer programs. In Mathematical logic and programming languages, pages 55\u2013 75, 1985."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.05.015"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1953122.1953145"},{"key":"e_1_3_2_1_18_1","series-title":"LNCS","first-page":"370","volume-title":"Proc. LPAR","author":"Leino K. Rustan M.","unstructured":"K. Rustan M. Leino . Dafny: An automatic program verifier for functional correctness . In Proc. LPAR , volume 6355 of LNCS , pages 348\u2013 370 . Springer-Verlag, 2010. K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In Proc. LPAR, volume 6355 of LNCS, pages 348\u2013370. Springer-Verlag, 2010."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_2_1_20_1","volume-title":"Springer-Verlag","author":"Jacobs B.","year":"2011","unstructured":"B. Jacobs , J. Smans , P. Philippaerts , F. Vogels , W. Penninckx , and F. Piessens . Verifast: A powerful, sound, predictable, fast verifier for C and Java. pages 41\u201355 . Springer-Verlag , 2011 . B. Jacobs, J. Smans, P. Philippaerts, F. Vogels, W. Penninckx, and F. Piessens. Verifast: A powerful, sound, predictable, fast verifier for C and Java. pages 41\u201355. Springer-Verlag, 2011."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-02654-1_13"},{"key":"e_1_3_2_1_22_1","first-page":"159","volume-title":"Proc. FTSCS","author":"Pearce D. J.","year":"2013","unstructured":"D. J. Pearce and Lindsay Groves . Reflections on verifying software with Whiley . In Proc. FTSCS , pages 142\u2013 159 , 2013 . D. J. Pearce and Lindsay Groves. Reflections on verifying software with Whiley. In Proc. FTSCS, pages 142\u2013159, 2013."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.35"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.402054"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2736348"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.375178"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/2486788.2486823"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593882.2593898"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1085313.1085331"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2010.10.004"},{"key":"e_1_3_2_1_31_1","first-page":"31","volume-title":"Proceedings of Symposia in Applied Mathematics","volume":"19","author":"Floyd R. W.","unstructured":"R. W. Floyd . Assigning meaning to programs . In Proceedings of Symposia in Applied Mathematics , volume 19 , pages 19\u2013 31 . American Mathematical Society, 1967. R. W. Floyd. Assigning meaning to programs. In Proceedings of Symposia in Applied Mathematics, volume 19, pages 19\u2013 31. American Mathematical Society, 1967."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1207\/s15327051hci0304_2"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1080\/08993400802114508"}],"event":{"name":"SPLASH '15: Conference on Systems, Programming, Languages, and Applications: Software for Humanity","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGAda ACM Special Interest Group on Ada Programming Language"],"location":"Pittsburgh PA USA","acronym":"SPLASH '15"},"container-title":["Proceedings of the 6th Workshop on Evaluation and Usability of Programming Languages and Tools"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2846680.2846691","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,7]],"date-time":"2023-01-07T19:45:23Z","timestamp":1673120723000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2846680.2846691"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,10,26]]},"references-count":31,"alternative-id":["10.1145\/2846680.2846691","10.1145\/2846680"],"URL":"https:\/\/doi.org\/10.1145\/2846680.2846691","relation":{},"subject":[],"published":{"date-parts":[[2015,10,26]]},"assertion":[{"value":"2015-10-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}