{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,25]],"date-time":"2026-06-25T03:41:02Z","timestamp":1782358862774,"version":"3.54.5"},"publisher-location":"New York, NY, USA","reference-count":28,"publisher":"ACM","license":[{"start":{"date-parts":[[2005,1,12]],"date-time":"2005-01-12T00:00:00Z","timestamp":1105488000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2005,1,12]]},"DOI":"10.1145\/1040305.1040316","type":"proceedings-article","created":{"date-parts":[[2005,1,30]],"date-time":"2005-01-30T12:58:48Z","timestamp":1107089928000},"page":"122-131","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":34,"title":["Proof-guided underapproximation-widening for multi-process systems"],"prefix":"10.1145","author":[{"given":"Orna","family":"Grumberg","sequence":"first","affiliation":[{"name":"Technion Haifa, Israel"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Flavio","family":"Lerda","sequence":"additional","affiliation":[{"name":"Carnegie Mellon, Pittsburgh, PA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ofer","family":"Strichman","sequence":"additional","affiliation":[{"name":"Technion Haifa, Israel"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael","family":"Theobald","sequence":"additional","affiliation":[{"name":"Carnegie Mellon, Pittsburgh, PA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2005,1,12]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/647766.733599"},{"key":"e_1_3_2_1_2_1","volume-title":"9th Intl. Conf. on Tools And Algorithms For The Construction And Analysis Of Systems (TACAS'03)","volume":"2619","author":"Amla N.","year":"2003","unstructured":"N. Amla and K. McMillan . Automatic abstraction without counterexamples. In H. Garavel and J. Hatcliff, editors , 9th Intl. Conf. on Tools And Algorithms For The Construction And Analysis Of Systems (TACAS'03) , volume 2619 of Lect. Notes in Comp. Sci. , 2003 .]] N. Amla and K. McMillan. Automatic abstraction without counterexamples. In H. Garavel and J. Hatcliff, editors, 9th Intl. Conf. on Tools And Algorithms For The Construction And Analysis Of Systems (TACAS'03), volume 2619 of Lect. Notes in Comp. Sci., 2003.]]"},{"key":"e_1_3_2_1_3_1","series-title":"Lect","first-page":"29","volume-title":"Proc. 5th Intl. Conference on Computer Aided Verification (CAV'94)","author":"Balarin F.","year":"1993","unstructured":"F. Balarin and A. Sangiovanni-Vinventelli . An iterative approah to language containment . In C. Courcoubetis, editor, Proc. 5th Intl. Conference on Computer Aided Verification (CAV'94) , volume 697 of Lect . Notes in Comp. Sci., pages 29 -- 40 . Springer-Verlag , 1993 .]] F. Balarin and A. Sangiovanni-Vinventelli. An iterative approah to language containment. In C. Courcoubetis, editor, Proc. 5th Intl. Conference on Computer Aided Verification (CAV'94), volume 697 of Lect. Notes in Comp. Sci., pages 29--40. Springer-Verlag, 1993.]]"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/647771.734429"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/647771.734424"},{"key":"e_1_3_2_1_6_1","volume-title":"Bounded Model Checking, volume~58 of Advances in computers","author":"Biere A.","year":"2003","unstructured":"A. Biere , A. Cimatti , E. Clarke , O. Strichman , and Y. Zue . Bounded Model Checking, volume~58 of Advances in computers . Academic Press , 2003 .]] A. Biere, A. Cimatti, E. Clarke, O. Strichman, and Y. Zue. Bounded Model Checking, volume~58 of Advances in computers. Academic Press, 2003.]]"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/309847.309942"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/646483.691738"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/646187.683250"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_3_2_1_11_1","series-title":"LNCS","first-page":"265","volume-title":"Proc. 14th Intl. Conference on Computer Aided Verification (CAV'02)","author":"Clarke E.","year":"2002","unstructured":"E. Clarke , A. Gupta , J. Kukula , and O. Strichman . SAT based abstraction - refinement using ILP and machine learning techniques . In E. Brinksma and K. Larsen, editors, Proc. 14th Intl. Conference on Computer Aided Verification (CAV'02) , volume 2404 of LNCS , pages 265 -- 279 , Copenhagen, Denmark, July 2002 . Springer-Verlag .]] E. Clarke, A. Gupta, J. Kukula, and O. Strichman. SAT based abstraction - refinement using ILP and machine learning techniques. In E. Brinksma and K. Larsen, editors, Proc. 14th Intl. Conference on Computer Aided Verification (CAV'02), volume 2404 of LNCS, pages 265--279, Copenhagen, Denmark, July 2002. Springer-Verlag.]]"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_9"},{"key":"e_1_3_2_1_13_1","series-title":"Lect","volume-title":"Proc. 12th Intl. Conference on Computer Aided Verification (CAV'00)","author":"Clarke E. M.","year":"2000","unstructured":"E. M. Clarke , O. Grumberg , S. Jha , Y. Lu , and H. Veith . Counterexample-guided abstraction refinement . In E. A. Emerson and A. P. Sistla, editors, Proc. 12th Intl. Conference on Computer Aided Verification (CAV'00) , volume 1855 of Lect . Notes in Comp. Sci. Springer-Verlag , 2000 .]] E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In E. A. Emerson and A. P. Sistla, editors, Proc. 12th Intl. Conference on Computer Aided Verification (CAV'00), volume 1855 of Lect. Notes in Comp. Sci. Springer-Verlag, 2000.]]"},{"key":"e_1_3_2_1_14_1","volume-title":"A discipline of programming","author":"Dijkstra E. W.","year":"1976","unstructured":"E. W. Dijkstra . A discipline of programming . Prentice Hall , 1976 .]] E. W. Dijkstra. A discipline of programming. Prentice Hall, 1976.]]"},{"key":"e_1_3_2_1_15_1","volume-title":"Model Checking","author":"Clarke E.M.","year":"1999","unstructured":"E.M. Clarke , O. Grumberg , and D. Peled . Model Checking . MIT Press , Cambridge, MA , 1999 .]] E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, Cambridge, MA, 1999.]]"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1024746015231"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1007\/3-540-55179-4_32","volume-title":"Workshop on Computer-Aided Verification (CAV'91)","volume":"575","author":"Godefroid P.","year":"1991","unstructured":"P. Godefroid and P. Wolper . Using partial orders for the efficient verification of deadlock freedom and safety properties . In Workshop on Computer-Aided Verification (CAV'91) , volume 575 of LNCS, pages 332 -- 342 , 1991 .]] P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. In Workshop on Computer-Aided Verification (CAV'91), volume 575 of LNCS, pages 332--342, 1991.]]"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02252682"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/646542.696213"},{"key":"e_1_3_2_1_20_1","volume-title":"Computer aided verification of coordinating processes","author":"Kurshan R.","year":"1994","unstructured":"R. Kurshan . Computer aided verification of coordinating processes . Princeton University Press , 1994 .]] R. Kurshan. Computer aided verification of coordinating processes. Princeton University Press, 1994.]]"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1020383505582"},{"key":"e_1_3_2_1_22_1","series-title":"Lect","first-page":"316","volume-title":"Proc. 11th Intl. Conference on Computer Aided Verification (CAV'99)","author":"Lind-Nielsen J.","year":"1999","unstructured":"J. Lind-Nielsen and H. Andersan . Stepwise CTL model checking of state\/event systems . In N. Halbwachs and D. Peled, editors, Proc. 11th Intl. Conference on Computer Aided Verification (CAV'99) , volume 1633 of Lect . Notes in Comp. Sci., pages 316 -- 327 . Springer-Verlag , 1999 .]] J. Lind-Nielsen and H. Andersan. Stepwise CTL model checking of state\/event systems. In N. Halbwachs and D. Peled, editors, Proc. 11th Intl. Conference on Computer Aided Verification (CAV'99), volume 1633 of Lect. Notes in Comp. Sci., pages 316--327. Springer-Verlag, 1999.]]"},{"key":"e_1_3_2_1_23_1","volume-title":"Interpolation and sat-based model checking","author":"McMillan K. L.","year":"2003","unstructured":"K. L. McMillan . Interpolation and sat-based model checking . In J. Warren A. Hunt and F. Somenzi, editors, cav03, Lect. Notes in Comp. Sci ., Jul 2003 .]] K. L. McMillan. Interpolation and sat-based model checking. In J. Warren A. Hunt and F. Somenzi, editors, cav03, Lect. Notes in Comp. Sci., Jul 2003.]]"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/647763.735529"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/224841.224874"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/646704.702017"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/646186.683237"},{"key":"e_1_3_2_1_28_1","volume-title":"Workshop on Computer-Aided Verification (CAV'90)","volume":"531","author":"Valmari A.","year":"1990","unstructured":"A. Valmari . A stubborn attack on state explosion . In Workshop on Computer-Aided Verification (CAV'90) , volume 531 of LNCS, New Brunswick , 1990 .]] A. Valmari. A stubborn attack on state explosion. In Workshop on Computer-Aided Verification (CAV'90), volume 531 of LNCS, New Brunswick, 1990.]]"}],"event":{"name":"POPL05: The 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2005","location":"Long Beach California USA","acronym":"POPL05","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1040305.1040316","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1040305.1040316","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:25:00Z","timestamp":1750249500000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1040305.1040316"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,1,12]]},"references-count":28,"alternative-id":["10.1145\/1040305.1040316","10.1145\/1040305"],"URL":"https:\/\/doi.org\/10.1145\/1040305.1040316","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1047659.1040316","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2005,1,12]]},"assertion":[{"value":"2005-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}