{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:01:14Z","timestamp":1725454874392},"publisher-location":"New York, NY, USA","reference-count":28,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2002,1]]},"DOI":"10.1145\/503272.503279","type":"proceedings-article","created":{"date-parts":[[2003,6,2]],"date-time":"2003-06-02T17:12:42Z","timestamp":1054573962000},"update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":591,"title":["Lazy abstraction"],"prefix":"10.1145","author":[{"given":"Thomas A.","family":"Henzinger","sequence":"first","affiliation":[{"name":"University of California, Berkeley, CA"}]},{"given":"Ranjit","family":"Jhala","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, CA"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, CA"}]},{"given":"Gr\u00e9goire","family":"Sutre","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Bordeaux 1, 33405 Talence Cedex, France"}]}],"member":"320","published-online":{"date-parts":[[2002,1]]},"reference":[{"key":"e_1_3_2_1_1_2","volume-title":"Compilers: Principles, Techniques, and Tools","author":"Aho A.V.","year":"1986","unstructured":"A.V. Aho , R. Sethi , and J.D. Ullman . Compilers: Principles, Techniques, and Tools . Addison-Wesley , 1986 .]] A.V. Aho, R. Sethi, and J.D. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley, 1986.]]"},{"key":"e_1_3_2_1_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_3_2_1_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_3_2_1_4_2","first-page":"268","volume-title":"LNCS 2031","author":"Ball T.","year":"2001","unstructured":"T. Ball , A. Podelski , and S.K. Rajamani . Boolean and Cartesian abstractions for model checking C programs. In TACAS 01: Tools and Algorithms for Construction and Analysis of Systems , LNCS 2031 , pp. 268 - 283 . Springer , 2001 .]] T. Ball, A. Podelski, and S.K. Rajamani. Boolean and Cartesian abstractions for model checking C programs. In TACAS 01: Tools and Algorithms for Construction and Analysis of Systems, LNCS 2031, pp. 268-283. Springer, 2001.]]"},{"key":"e_1_3_2_1_5_2","doi-asserted-by":"publisher","DOI":"10.5555\/380921.380932"},{"key":"e_1_3_2_1_6_2","unstructured":"D. Blei etal. Vampyre: A proof generating theorem prover. http:\/\/www.eees.berkeley.edu\/rupak\/Vampyre.]] D. Blei etal. Vampyre: A proof generating theorem prover. http:\/\/www.eees.berkeley.edu\/rupak\/Vampyre.]]"},{"key":"e_1_3_2_1_7_2","first-page":"1","volume-title":"CAV 96: Computer Aided Verification, LNCS 1102","author":"Boigelot B.","year":"1996","unstructured":"B. Boigelot and P. Godefroid . Symbolic verification of communication protocols with infinite state spaces using QDDs . In CAV 96: Computer Aided Verification, LNCS 1102 , pp. 1 - 12 . Springer , 1996 .]] B. Boigelot and P. Godefroid. Symbolic verification of communication protocols with infinite state spaces using QDDs. In CAV 96: Computer Aided Verification, LNCS 1102, pp. 1-12. Springer, 1996.]]"},{"key":"e_1_3_2_1_8_2","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/3-540-58179-0_43","volume-title":"CAV 93: Computer Aided Verification, LNCS 818","author":"Boigelot B.","year":"1994","unstructured":"B. Boigelot and P. Wolper . Symbolic verification with periodic sets . In CAV 93: Computer Aided Verification, LNCS 818 , pp. 55 - 67 . Springer , 1994 .]] B. Boigelot and P. Wolper. Symbolic verification with periodic sets. In CAV 93: Computer Aided Verification, LNCS 818, pp. 55-67. Springer, 1994.]]"},{"key":"e_1_3_2_1_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00033-X"},{"key":"e_1_3_2_1_10_2","first-page":"154","volume-title":"CAV 00: Computer Aided Verification, LNCS","author":"Clarke E.","year":"1855","unstructured":"E. Clarke , O. Grumberg , S. Jha , Y. Lu , and H. Veith . Counterexample-guided abstraction refinement . In CAV 00: Computer Aided Verification, LNCS 1855 , pp. 154 - 169 . Springer , 2000.]] E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV 00: Computer Aided Verification, LNCS 1855, pp. 154-169. Springer, 2000.]]"},{"key":"e_1_3_2_1_11_2","volume-title":"Model Checking","author":"Clarke E.M.","year":"1999","unstructured":"E.M. Clarke , O. Grumberg , and D. Poled . Model Checking . MIT Press , 1999 .]] E.M. Clarke, O. Grumberg, and D. Poled. Model Checking. MIT Press, 1999.]]"},{"key":"e_1_3_2_1_12_2","first-page":"160","volume-title":"CA V 99: Computer Aided Verification, LNCS 1633","author":"Das S.","year":"1999","unstructured":"S. Das , D.L. Dill , and S. Park . Experience with predicate abstraction . In CA V 99: Computer Aided Verification, LNCS 1633 , pp. 160 - 171 . Springer , 1999 .]] S. Das, D.L. Dill, and S. Park. Experience with predicate abstraction. In CA V 99: Computer Aided Verification, LNCS 1633, pp. 160-171. Springer, 1999.]]"},{"key":"e_1_3_2_1_13_2","first-page":"51","volume-title":"LICS 01: Logic in Computer Science","author":"Das S.","year":"2001","unstructured":"S. Das and D.L. Dill . Successive approximation of abstract transition relations . In LICS 01: Logic in Computer Science , pp. 51 - 60 . IEEE , 2001 .]] S. Das and D.L. Dill. Successive approximation of abstract transition relations. In LICS 01: Logic in Computer Science, pp. 51-60. IEEE, 2001.]]"},{"key":"e_1_3_2_1_14_2","first-page":"223","volume-title":"TACAS 99: Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1579","author":"Delzanno G.","year":"1999","unstructured":"G. Delzanno and A. Podelski . Model checking in CLP . In TACAS 99: Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1579 , pp. 223 - 239 . Springer , 1999 .]] G. Delzanno and A. Podelski. Model checking in CLP. In TACAS 99: Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1579, pp. 223-239. Springer, 1999.]]"},{"key":"e_1_3_2_1_15_2","unstructured":"D. Detlefs G. Nelson and J. Saxe. Simplify theorem prover. http:\/\/researeh.eompaq.eom\/SRC\/ese\/Simplify.html.]] D. Detlefs G. Nelson and J. Saxe. Simplify theorem prover. http:\/\/researeh.eompaq.eom\/SRC\/ese\/Simplify.html.]]"},{"key":"e_1_3_2_1_16_2","volume-title":"A Discipline of Programming","author":"Dijkstra E.W.","year":"1977","unstructured":"E.W. Dijkstra . A Discipline of Programming . Prentice-Hall , 1977 6.]] E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 19776.]]"},{"key":"e_1_3_2_1_17_2","volume-title":"OSDI 00: Operating System Design and Implementation","author":"Engler D.","year":"2000","unstructured":"D. Engler , B. Chelf , A. Chou , and S. Hallem . Checking system rules using system-specific, programmer-written compiler extensions . In OSDI 00: Operating System Design and Implementation . Usenix Association , 2000 .]] D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In OSDI 00: Operating System Design and Implementation. Usenix Association, 2000.]]"},{"key":"e_1_3_2_1_18_2","first-page":"566","volume-title":"CONCUR 00: Concurrency Theory, LNCS 18777","author":"Finkel A.","year":"2000","unstructured":"A. Finkel , S. P. Iyer , and G. Sutre . Well-abstracted transition systems . In CONCUR 00: Concurrency Theory, LNCS 18777 , pp. 566 - 580 . Springer , 2000 .]] A. Finkel, S. P. Iyer, and G. Sutre. Well-abstracted transition systems. In CONCUR 00: Concurrency Theory, LNCS 18777, pp. 566-580. Springer, 2000.]]"},{"key":"e_1_3_2_1_20_2","first-page":"772","volume-title":"CAV 97: Computer Aided Verification, LNCS 1254","author":"Graf S.","year":"1997","unstructured":"S. Graf and H. Sa'fdi . Construction of abstract state graphs with PVS . In CAV 97: Computer Aided Verification, LNCS 1254 , pp. 772 - 783 . Springer , 1997 7.]] S. Graf and H. Sa'fdi. Construction of abstract state graphs with PVS. In CAV 97: Computer Aided Verification, LNCS 1254, pp. 772-83. Springer, 19977.]]"},{"key":"e_1_3_2_1_21_2","volume-title":"The Science of Programming","author":"Cries D.","year":"1981","unstructured":"D. Cries . The Science of Programming . Springer , 1981 .]] D. Cries. The Science of Programming. Springer, 1981.]]"},{"key":"e_1_3_2_1_22_2","first-page":"13","volume-title":"STACS 00: Theoretical Aspects of Computer Science, LNCS 1770","author":"Henzinger T. A.","year":"2000","unstructured":"T. A. Henzinger and R. Majumdar . A classification of symbolic transition systems . In STACS 00: Theoretical Aspects of Computer Science, LNCS 1770 , pp. 13 - 34 . Springer , 2000 .]] T. A. Henzinger and R. Majumdar. A classification of symbolic transition systems. In STACS 00: Theoretical Aspects of Computer Science, LNCS 1770, pp. 13-34. Springer, 2000.]]"},{"key":"e_1_3_2_1_23_2","unstructured":"C. Linet al. C-breeze: C compiler infrastructure. http:\/\/www.es.utexas.edu\/users\/e-breeze.]] C. Linet al. C-breeze: C compiler infrastructure. http:\/\/www.es.utexas.edu\/users\/e-breeze.]]"},{"key":"e_1_3_2_1_24_2","first-page":"25","volume-title":"International Summer School","author":"Morris J.M.","year":"1982","unstructured":"J.M. Morris . A general axiom of assignment. In Theoretical Foundations of Programming Methodology , International Summer School , pp. 25 - 34 . Reidel , 1982 .]] J.M. Morris. A general axiom of assignment. In Theoretical Foundations of Programming Methodology, International Summer School, pp. 25-34. Reidel, 1982.]]"},{"key":"e_1_3_2_1_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_3_2_1_27_2","first-page":"411","volume-title":"CAV 96: Computer Aided Verification, LNCS 1102","author":"Owre S.","year":"1996","unstructured":"S. Owre , S. Rajan , J.M. Rushby , N. Shankar , and M.K. Srivas . PVS: Combining specification, proof checking, and model checking . In CAV 96: Computer Aided Verification, LNCS 1102 , pp. 411 - 414 . Springer , 1996 .]] S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas. PVS: Combining specification, proof checking, and model checking. In CAV 96: Computer Aided Verification, LNCS 1102, pp. 411-414. Springer, 1996.]]"},{"key":"e_1_3_2_1_28_2","doi-asserted-by":"publisher","DOI":"10.5555\/647169.760067"},{"key":"e_1_3_2_1_29_2","unstructured":"F. Somenzi. Colorado university decision diagram package http:\/\/vlsi.eolorado.edu\/pub 1998.]] F. Somenzi. Colorado university decision diagram package http:\/\/vlsi.eolorado.edu\/pub 1998.]]"},{"key":"e_1_3_2_1_30_2","first-page":"977","volume-title":"USENIX","author":"Sterling N.","year":"1993","unstructured":"N. Sterling . Warlock : A static data race analysis tool . In USENIX Winter 1993 Technical Conference , pp. 977 - 106 , 1993.]] N. Sterling. Warlock: A static data race analysis tool. In USENIX Winter 1993 Technical Conference, pp. 977-106, 1993.]]"}],"event":{"name":"POPL02: The 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2002","location":"Portland Oregon","acronym":"POPL02","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 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/503272.503279","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T11:43:05Z","timestamp":1693827785000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/503272.503279"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,1]]},"references-count":28,"alternative-id":["10.1145\/503272.503279","10.1145\/503272"],"URL":"http:\/\/dx.doi.org\/10.1145\/503272.503279","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/565816.503279","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2002,1]]},"assertion":[{"value":"2002-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}