{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T13:05:19Z","timestamp":1742389519775},"publisher-location":"New York, NY, USA","reference-count":11,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2006,11,10]]},"DOI":"10.1145\/1181195.1181200","type":"proceedings-article","created":{"date-parts":[[2007,1,16]],"date-time":"2007-01-16T20:15:56Z","timestamp":1168978556000},"page":"19-24","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["Soundness and completeness warnings in ESC\/Java2"],"prefix":"10.1145","author":[{"given":"Joseph R.","family":"Kiniry","sequence":"first","affiliation":[{"name":"University College Dublin, Belfield, Ireland"}]},{"given":"Alan E.","family":"Morkan","sequence":"additional","affiliation":[{"name":"University College Dublin, Belfield, Ireland"}]},{"given":"Barry","family":"Denby","sequence":"additional","affiliation":[{"name":"University College Dublin, Belfield, Ireland"}]}],"member":"320","published-online":{"date-parts":[[2006,11,10]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00020-8"},{"key":"e_1_3_2_1_2_1","volume-title":"CVC Lite: A new implementation of the cooperating validity checker","author":"Barrett Clark","year":"2004","unstructured":"Clark Barrett and Sergey Berezin . CVC Lite: A new implementation of the cooperating validity checker . In Rajeev Alur and Doron A. Peled, editors, CAV, Lecture Notes in Computer Science. Springer-Verlag , 2004 . Clark Barrett and Sergey Berezin. CVC Lite: A new implementation of the cooperating validity checker. In Rajeev Alur and Doron A. Peled, editors, CAV, Lecture Notes in Computer Science. Springer-Verlag, 2004."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0167-4"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_3_2_1_5_1","volume-title":"The Coq Proof Assistant User's Guide","author":"Dowek G.","year":"1993","unstructured":"G. Dowek , A. Felty , H. Herbelin , G. Huet , C. Murthy , C. Parent , C. Paulin-Mohring , and B. Werner . The Coq Proof Assistant User's Guide . INRIA , Rocquencourt, France , rapport techniques 154 edition, 1993 . G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. Paulin-Mohring, and B. Werner. The Coq Proof Assistant User's Guide. INRIA, Rocquencourt, France, rapport techniques 154 edition, 1993."},{"key":"e_1_3_2_1_6_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Proceedings of the 16th International Conference on Computer Aided Verification, CAV'04 (Boston, Massachusetts)","author":"Ganzinger Harald","year":"2004","unstructured":"Harald Ganzinger , George Hagen , Robert Nieuwenhuis , Albert Oliveras , and Cesare Tinelli . DPLL(T) : Fast decision procedures . In R. Alur and D. Peled, editors, Proceedings of the 16th International Conference on Computer Aided Verification, CAV'04 (Boston, Massachusetts) , volume 3114 of Lecture Notes in Computer Science , pages 175 -- 188 . Springer-Verlag , 2004 . Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. DPLL(T): Fast decision procedures. In R. Alur and D. Peled, editors, Proceedings of the 16th International Conference on Computer Aided Verification, CAV'04 (Boston, Massachusetts), volume 3114 of Lecture Notes in Computer Science, pages 175--188. Springer-Verlag, 2004."},{"key":"e_1_3_2_1_7_1","series-title":"Lecture Notes in Computer Science","volume-title":"Construction and Analysis of Safe, Secure and Interoperable Smart Devices: International Workshop, CASSIS","author":"Kiniry Joseph R.","year":"2004","unstructured":"Joseph R. Kiniry and David R. Cok . ESC\/Java2: Uniting ESC\/Java and JML: Progress and issues in building and using ESC\/Java2 and a report on a case study involving the use of ESC\/Java2 to verify portions of an Internet voting tally system . In Construction and Analysis of Safe, Secure and Interoperable Smart Devices: International Workshop, CASSIS 2004 , volume 3362 of Lecture Notes in Computer Science . Springer-Verlag , Jan 2005. Joseph R. Kiniry and David R. Cok. ESC\/Java2: Uniting ESC\/Java and JML: Progress and issues in building and using ESC\/Java2 and a report on a case study involving the use of ESC\/Java2 to verify portions of an Internet voting tally system. In Construction and Analysis of Safe, Secure and Interoperable Smart Devices: International Workshop, CASSIS 2004, volume 3362 of Lecture Notes in Computer Science. Springer-Verlag, Jan 2005."},{"key":"e_1_3_2_1_8_1","volume-title":"Literate Programming. Number 27 in CSLI Lecture Notes","author":"Knuth Donald E.","year":"1992","unstructured":"Donald E. Knuth . Literate Programming. Number 27 in CSLI Lecture Notes . Center for the Study of Language and Information, 1992 . Donald E. Knuth. Literate Programming. Number 27 in CSLI Lecture Notes. Center for the Study of Language and Information, 1992."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"S.\n      Owre J. M.\n      Rushby and \n      N.\n      Shankar\n  . \n  PVS: A prototype verification system\n  . In Deepak Kapur editor 11th International Conference on Automated Deduction (CADE) volume \n  607\n   of \n  Lecture Notes in Artificial Intelligence pages \n  748\n  --\n  752 Saratoga NY June \n  1992\n  . \n  Springer-Verlag\n  .   S. Owre J. M. Rushby and N. Shankar. PVS: A prototype verification system. In Deepak Kapur editor 11th International Conference on Automated Deduction (CADE) volume 607 of Lecture Notes in Artificial Intelligence pages 748--752 Saratoga NY June 1992. Springer-Verlag.","DOI":"10.1007\/3-540-55602-8_217"},{"key":"e_1_3_2_1_11_1","unstructured":"SMT-LIB: The satisfiability modulo theories library. http:\/\/goedel.cs.uiowa.edu\/smtlib\/.  SMT-LIB: The satisfiability modulo theories library. http:\/\/goedel.cs.uiowa.edu\/smtlib\/."}],"event":{"name":"SIGSOFT06\/FSE-14: SIGSOFT 2006 -14th International Symposium on the Foundations of Software Engineering","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Portland Oregon","acronym":"SIGSOFT06\/FSE-14"},"container-title":["Proceedings of the 2006 conference on Specification and verification of component-based systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1181195.1181200","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,10]],"date-time":"2023-01-10T00:00:40Z","timestamp":1673308840000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1181195.1181200"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,11,10]]},"references-count":11,"alternative-id":["10.1145\/1181195.1181200","10.1145\/1181195"],"URL":"https:\/\/doi.org\/10.1145\/1181195.1181200","relation":{},"subject":[],"published":{"date-parts":[[2006,11,10]]},"assertion":[{"value":"2006-11-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}