{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T18:39:27Z","timestamp":1730313567124,"version":"3.28.0"},"publisher-location":"New York, NY, USA","reference-count":22,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2006,7,21]]},"DOI":"10.1145\/1146238.1146256","type":"proceedings-article","created":{"date-parts":[[2006,7,24]],"date-time":"2006-07-24T16:53:01Z","timestamp":1153759981000},"page":"157-168","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":40,"title":["Using model checking with symbolic execution to verify parallel numerical programs"],"prefix":"10.1145","author":[{"given":"Stephen F.","family":"Siegel","sequence":"first","affiliation":[{"name":"University of Massachusetts, Amherst, MA"}]},{"given":"Anastasia","family":"Mironova","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, UT"}]},{"given":"George S.","family":"Avrunin","sequence":"additional","affiliation":[{"name":"University of Massachusetts"}]},{"given":"Lori A.","family":"Clarke","sequence":"additional","affiliation":[{"name":"University of Massachusetts"}]}],"member":"320","published-online":{"date-parts":[[2006,7,21]]},"reference":[{"key":"e_1_3_2_1_1_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/3-540-45420-9","volume-title":"Model Checking Software: 8th International SPIN Workshop","author":"Ball T.","year":"2001","unstructured":"T. Ball and S. K. Rajamani . Automatically validating temporal safety properties of interfaces . In M. B. Dwyer, editor, Model Checking Software: 8th International SPIN Workshop , Toronto, Canada, May 19-20, 2001 , Proceedings, volume 2057 of Lecture Notes in Computer Science , pages 103 -- 122 . Springer , 2001. T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In M. B. Dwyer, editor, Model Checking Software: 8th International SPIN Workshop, Toronto, Canada, May 19-20, 2001, Proceedings, volume 2057 of Lecture Notes in Computer Science, pages 103--122. Springer, 2001."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/800027.808445"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1976.233817"},{"key":"e_1_3_2_1_4_1","volume-title":"Abstract Interpretation: 6th International Conference, VMCAI 2005, Paris, January 17-19, 2005, Proceedings","volume":"3385","author":"Cousot R.","year":"2005","unstructured":"R. Cousot , editor. Verification, Model Checking , and Abstract Interpretation: 6th International Conference, VMCAI 2005, Paris, January 17-19, 2005, Proceedings , volume 3385 of Lecture Notes in Computer Science , 2005 . R. Cousot, editor. Verification, Model Checking, and Abstract Interpretation: 6th International Conference, VMCAI 2005, Paris, January 17-19, 2005, Proceedings, volume 3385 of Lecture Notes in Computer Science, 2005."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065015"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/103162.103163"},{"key":"e_1_3_2_1_7_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/b96721","volume-title":"Barcelona","author":"Graf S.","year":"2004","unstructured":"S. Graf and L. Mounier , editors . Model Checking Software: 11th International SPIN Workshop , Barcelona , Spain, April 1-3, 2004 , Proceedings, volume 2989 of Lecture Notes in Computer Science . Springer , 2004. S. Graf and L. Mounier, editors. Model Checking Software: 11th International SPIN Workshop, Barcelona, Spain, April 1-3, 2004, Proceedings, volume 2989 of Lecture Notes in Computer Science. Springer, 2004."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/330577"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/356674.356677"},{"key":"e_1_3_2_1_10_1","volume-title":"The Spin Model Checker","author":"Holzmann G. J.","year":"2004","unstructured":"G. J. Holzmann . The Spin Model Checker . Addison-Wesley , 2004 . G. J. Holzmann. The Spin Model Checker. Addison-Wesley, 2004."},{"key":"e_1_3_2_1_11_1","volume-title":"754-1985 IEEE standard for binary floating-point arithmetic","author":"IEEE.","year":"1985","unstructured":"IEEE. 754-1985 IEEE standard for binary floating-point arithmetic , 1985 . IEEE. 754-1985 IEEE standard for binary floating-point arithmetic, 1985."},{"key":"e_1_3_2_1_12_1","volume-title":"854-1987 IEEE standard for radix-independent floating-point arithmetic","author":"IEEE.","year":"1987","unstructured":"IEEE. 854-1987 IEEE standard for radix-independent floating-point arithmetic , 1987 . IEEE. 854-1987 IEEE standard for radix-independent floating-point arithmetic, 1987."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/861343"},{"key":"e_1_3_2_1_14_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"553","DOI":"10.1007\/3-540-36577-X_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS","author":"Khurshid S.","year":"2003","unstructured":"S. Khurshid , C. S. P\u01ces\u01cereanu , and W. Visser . Generalized symbolic execution for model checking and testing . In H. Garavel and J. Hatcliff, editors, Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003 , Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, volume 2619 of Lecture Notes in Computer Science , pages 553 -- 568 . Springer , 2003. S. Khurshid, C. S. P\u01ces\u01cereanu, and W. Visser. Generalized symbolic execution for model checking and testing. In H. Garavel and J. Hatcliff, editors, Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, volume 2619 of Lecture Notes in Computer Science, pages 553--568. Springer, 2003."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_4"},{"key":"e_1_3_2_1_16_1","unstructured":"Message Passing Interface Forum. MPI: A Message-Passing Interface standard version 1.1. http:\/\/www.mpi-forum.org\/docs\/ 1995.  Message Passing Interface Forum. MPI: A Message-Passing Interface standard version 1.1. http:\/\/www.mpi-forum.org\/docs\/ 1995."},{"key":"e_1_3_2_1_17_1","unstructured":"Message Passing Interface Forum. MPI-2: Extensions to the Message-Passing Interface. http:\/\/www.mpi-forum.org\/docs\/ 1997.  Message Passing Interface Forum. MPI-2: Extensions to the Message-Passing Interface. http:\/\/www.mpi-forum.org\/docs\/ 1997."},{"key":"e_1_3_2_1_18_1","first-page":"164","volume-title":"Graf and Mounier 7","author":"P\u01ces\u01cereanu C. S.","unstructured":"C. S. P\u01ces\u01cereanu and W. Visser . Verification of Java programs using symbolic execution and invariant generation . In Graf and Mounier 7 , pages 164 -- 181 . C. S. P\u01ces\u01cereanu and W. Visser. Verification of Java programs using symbolic execution and invariant generation. In Graf and Mounier 7, pages 164--181."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/940071.940107"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_27"},{"key":"e_1_3_2_1_21_1","first-page":"286","volume-title":"Graf and Mounier 7","author":"Siegel S. F.","unstructured":"S. F. Siegel and G. S. Avrunin . Verification of MPI-based software for scientific computation . In Graf and Mounier 7 , pages 286 -- 303 . S. F. Siegel and G. S. Avrunin. Verification of MPI-based software for scientific computation. In Graf and Mounier 7, pages 286--303."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065944.1065957"}],"event":{"name":"ISSTA06: International Symposium on Software Testing and Analysis 2006","sponsor":["ACM Association for Computing Machinery","SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Portland Maine USA","acronym":"ISSTA06"},"container-title":["Proceedings of the 2006 international symposium on Software testing and analysis"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1146238.1146256","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,12]],"date-time":"2023-01-12T08:30:00Z","timestamp":1673512200000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1146238.1146256"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,7,21]]},"references-count":22,"alternative-id":["10.1145\/1146238.1146256","10.1145\/1146238"],"URL":"https:\/\/doi.org\/10.1145\/1146238.1146256","relation":{},"subject":[],"published":{"date-parts":[[2006,7,21]]},"assertion":[{"value":"2006-07-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}