{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:19:59Z","timestamp":1775053199600,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":34,"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.1146255","type":"proceedings-article","created":{"date-parts":[[2006,7,24]],"date-time":"2006-07-24T16:53:01Z","timestamp":1153759981000},"page":"145-156","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":52,"title":["Testing, abstraction, theorem proving"],"prefix":"10.1145","author":[{"given":"Greta","family":"Yorsh","sequence":"first","affiliation":[{"name":"Tel Aviv University, Israel"}]},{"given":"Thomas","family":"Ball","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}]}],"member":"320","published-online":{"date-parts":[[2006,7,21]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11561163_1"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_3_2_1_3_1","volume-title":"International Journal of Artificial Intelligence Tools","author":"Baumgartner P.","year":"2005","unstructured":"P. Baumgartner , A. Fuchs , and C. Tinelli . Implementing the Model Evolution Calculus. In Stephan Schulz, Geoff Sutcliffe, and Tanel Tammet, editors, Special Issue of the International Journal of Artificial Intelligence Tools (IJAIT) , International Journal of Artificial Intelligence Tools , 2005 . Preprint. P. Baumgartner, A. Fuchs, and C. Tinelli. Implementing the Model Evolution Calculus. In Stephan Schulz, Geoff Sutcliffe, and Tanel Tammet, editors, Special Issue of the International Journal of Artificial Intelligence Tools (IJAIT), International Journal of Artificial Intelligence Tools, 2005. Preprint."},{"key":"e_1_3_2_1_4_1","volume-title":"CADE-19 Workshop: Model Computation - Principles","author":"Claessen K.","year":"2003","unstructured":"K. Claessen and N. Sorensson . New techniques that improve mace-style finite model finding . In CADE-19 Workshop: Model Computation - Principles , Algorithms, Applications , 2003 . K. Claessen and N. Sorensson. New techniques that improve mace-style finite model finding. In CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications, 2003."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1062455.1062533"},{"key":"e_1_3_2_1_9_1","volume-title":"Eindhoven","author":"Dams D.","year":"1996","unstructured":"D. Dams . Abstract Interpretation and Partial Refinement for Model Checking. PhD thesis, Technical Univ. of Eindhoven , Eindhoven , The Netherlands , July 1996 . D. Dams. Abstract Interpretation and Partial Refinement for Model Checking. PhD thesis, Technical Univ. of Eindhoven, Eindhoven, The Netherlands, July 1996."},{"key":"e_1_3_2_1_11_1","volume-title":"A Discipline of Programming","author":"Dijksta E.W.","year":"1976","unstructured":"E.W. Dijksta . A Discipline of Programming . Prentice-Hall , 1976 . E.W. Dijksta. A Discipline of Programming. Prentice-Hall, 1976."},{"key":"e_1_3_2_1_12_1","volume-title":"Generating concrete counter examples for arbitrary abstract domains. Master's thesis","author":"Erez G.","year":"2004","unstructured":"G. Erez . Generating concrete counter examples for arbitrary abstract domains. Master's thesis , Tel-Aviv University , Israel , 2004 . G. Erez. Generating concrete counter examples for arbitrary abstract domains. Master's thesis, Tel-Aviv University, Israel, 2004."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/996821.996823"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.908957"},{"key":"e_1_3_2_1_15_1","first-page":"19","volume-title":"Proceedings of Symposia in Applied Mathematics 19","author":"Floyd R. W.","year":"1967","unstructured":"R. W. Floyd . Assigning meanings to programs. In J. T. Schwartz, editor, Mathematical Aspects of Computer Science , Proceedings of Symposia in Applied Mathematics 19 , pages 19 -- 32 , Providence , 1967 . American Mathematical Society. R. W. Floyd. Assigning meanings to programs. In J. T. Schwartz, editor, Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics 19, pages 19--32, Providence, 1967. American Mathematical Society."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_3_2_1_17_1","first-page":"72","volume-title":"CAV","author":"Graf S.","year":"1997","unstructured":"S. Graf and H. Sa\u00efdi . Construction of abstract state graphs with PVS . In CAV , pages 72 -- 83 , June 1997 . S. Graf and H. Sa\u00efdi. Construction of abstract state graphs with PVS. In CAV, pages 72--83, June 1997."},{"key":"e_1_3_2_1_18_1","volume-title":"SoftMC","author":"Grieskamp W.","year":"2005","unstructured":"W. Grieskamp , N. Tillmann , and W. Schulte . Xrt exploring runtime for .net: Architecture and applications . In SoftMC , 2005 . W. Grieskamp, N. Tillmann, and W. Schulte. Xrt exploring runtime for .net: Architecture and applications. In SoftMC, 2005."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/336512.336532"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/1767111.1767128"},{"key":"e_1_3_2_1_21_1","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"Holzmann G. J.","year":"2003","unstructured":"G. J. Holzmann . The Spin Model Checker: Primer and Reference Manual . Addison-Wesley , 2003 . G. J. Holzmann. The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, 2003."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/129712.129738"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/647169.718161"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/1060289.1060297"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/555142"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/587051.587054"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_7"},{"key":"e_1_3_2_1_30_1","first-page":"376","volume-title":"IJCAR","author":"Riazanov A.","year":"2001","unstructured":"A. Riazanov and A. Voronkov . Vampire 1.1 (system description) . In IJCAR , pages 376 -- 380 , 2001 . A. Riazanov and A. Voronkov. Vampire 1.1 (system description). In IJCAR, pages 376--380, 2001."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081750"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_21"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022920129859"},{"key":"e_1_3_2_1_35_1","unstructured":"C. Weidenbach. SPASS: An automated theorem prover for first-order logic with equality. Available at \"http:\/\/spass.mpi-sb.mpg.de\/index.html\".  C. Weidenbach. SPASS: An automated theorem prover for first-order logic with equality. Available at \"http:\/\/spass.mpi-sb.mpg.de\/index.html\"."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_39"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/267580.267590"}],"event":{"name":"ISSTA06: International Symposium on Software Testing and Analysis 2006","location":"Portland Maine USA","acronym":"ISSTA06","sponsor":["ACM Association for Computing Machinery","SIGSOFT ACM Special Interest Group on Software Engineering"]},"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.1146255","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,12]],"date-time":"2023-01-12T08:30:22Z","timestamp":1673512222000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1146238.1146255"}},"subtitle":["better together!"],"short-title":[],"issued":{"date-parts":[[2006,7,21]]},"references-count":34,"alternative-id":["10.1145\/1146238.1146255","10.1145\/1146238"],"URL":"https:\/\/doi.org\/10.1145\/1146238.1146255","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"}}]}}