{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T03:47:10Z","timestamp":1760586430303},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540442356"},{"type":"electronic","value":"9783540457893"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45789-5_16","type":"book-chapter","created":{"date-parts":[[2007,8,11]],"date-time":"2007-08-11T13:50:10Z","timestamp":1186840210000},"page":"196-212","source":"Crossref","is-referenced-by-count":10,"title":["Compactly Representing First-Order Structures for Static Analysis"],"prefix":"10.1007","author":[{"given":"R.","family":"Manevich","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G.","family":"Ramalingam","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J.","family":"Field","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"D.","family":"Goyal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,9,5]]},"reference":[{"key":"16_CR1","volume-title":"Modern Compiler Implementation in C.","author":"A. Appel","year":"1998","unstructured":"A. Appel and M. Ginsburg. Modern Compiler Implementation in C. Cambridge University Press, New York, Cambridge, 1998."},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"R. E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. A CM Computing Surveys, 24(3):293\u2013318, Sept. 1992.","DOI":"10.1145\/136035.136043"},{"key":"16_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/BFb0053547","volume-title":"Proc. of Foundations of Software Science and Computation Structures (FoSSaCS)","author":"L. Cardelli","year":"1998","unstructured":"L. Cardelli and A. Gordon. Mobile ambients. In M. Nivat, editor, Proc. of Foundations of Software Science and Computation Structures (FoSSaCS), volume 1378 of LNCS, pages 140\u2013155. Springer-Verlag, Mar. 1998."},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"N. Dor, M. Rodeh, and M. Sagiv. Checking cleanness in linked lists. In Proc. Static Analysis Symp., pages 115\u2013134, July 2000.","DOI":"10.1007\/978-3-540-45099-3_7"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"N. Klarlund, A. Moller, and M. I. Schwartzbach. MONA implementation secrets. In CIAA, pages 182\u2013194, 2000.","DOI":"10.7146\/brics.v7i40.20206"},{"key":"16_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1007\/978-3-540-45099-3_15","volume-title":"Proc. Static Analysis Symp.","author":"T. Lev-Ami","year":"2000","unstructured":"T. Lev-Ami and M. Sagiv. TVLA: A framework for Kleene based static analysis. In J. Palsberg, editor, Proc. Static Analysis Symp., volume 1824 of Lecture Notes in Computer Science, pages 280\u2013301. Springer-Verlag, 2000. \n                  http:\/\/www.cs.tau.ac.i1\/~rumster\/TVLA\/\n                  \n                ."},{"issue":"1","key":"16_CR7","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/s100090050017","volume":"2","author":"F. Martin","year":"1998","unstructured":"F. Martin. PAG-an efficient program analyzer generator. International Journal on Software Tools for Technology Transfer, 2(1):46\u201367, 1998.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"1","key":"16_CR8","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1016\/S0167-6423(96)00042-1","volume":"31","author":"L. Mauborgne","year":"1998","unstructured":"L. Mauborgne. Abstract interpretation using typed decision graphs. Science of Computer Programming, 31(1):91\u2013112, May 1998.","journal-title":"Science of Computer Programming"},{"key":"16_CR9","unstructured":"Microsoft Research. The SLAM project. \n                  http:\/\/research.microsoft.com\/slam\/\n                  \n                , 2001."},{"key":"16_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/3-540-46425-5_20","volume-title":"Proc. of ESOP 2000","author":"F. Nielson","year":"2000","unstructured":"F. Nielson, H. Nielson, and M. Sagiv. A Kleene analysis of mobile ambients. In G. Smolka, editor, Proc. of ESOP 2000, volume 1782 of LNCS, pages 305\u2013319. Springer, 2000."},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"G. Ramalingam, A. Warshavsky, J. Field, D. Goyal, and M. Sagiv. Deriving specialized program analyses for certifying component-client conformance. In Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation, pages 83\u201394, Berlin, June 2002.","DOI":"10.1145\/512529.512540"},{"key":"16_CR12","unstructured":"T. Reps, M. Sagiv, and R. Wilhelm. Automatic verification of a simple mark and sweep garbabge collector. Presented in the 2001 University of Washington and Microsoft Research Summer Institute, Specifying and Checking Properties of Software, \n                  http:\/\/research.microsoft.com\/specncheck\/\n                  \n                , 2001."},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. In Proc. ACM Symp. on Principles of Programming Languages, pages 105\u2013118, 1999.","DOI":"10.1145\/292540.292552"},{"issue":"6","key":"16_CR14","doi-asserted-by":"crossref","first-page":"457","DOI":"10.1007\/s002360050128","volume":"35","author":"S. Sagiv","year":"1998","unstructured":"S. Sagiv, N. Francez, M. Rodeh, and R. Wilhelm. A logic-based approach to data flow analysis problems. Acta Inf., 35(6):457\u2013504, June 1998.","journal-title":"Acta Inf."},{"key":"16_CR15","unstructured":"F. Somenzi. Colorado University Decision Diagram Package (CUDD). Department of Electrical and Computer Engineering, University of Colorado at Boulder, 1998. \n                  http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/\n                  \n                ."},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"H. Veith. How to encode a logical structure by an OBDD. In IEEE Conference on Computational Complexity, pages 122\u2013131, 1998.","DOI":"10.1109\/CCC.1998.694598"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"E. Yahav. Verifying safety properties of concurrent Java programs using 3-valued logic. In Proc. ACM Symp. on Principles of Programming Languages, pages 27\u201340, 2001.","DOI":"10.1145\/360204.360206"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"B. Yang, R. E. Bryant, D. R. O\u2019Hallaron, A. Biere, O. Coudert, G. Janssen, R. K. Ranjan, and F. Somenzi. A performance study of BDD-based model checking. In Proceedings of the Formal Methods on Computer-Aided Design, pages 255\u2013289, November 1998.","DOI":"10.1007\/3-540-49519-3_18"},{"key":"16_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/3-540-45319-9_5","volume-title":"Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Yavuz-Kahveci","year":"2001","unstructured":"T. Yavuz-Kahveci, M. Tuncer, and T. Bultan. Composite symbolic library. In Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 2031 of Lecture Notes in Computer Science, pages 335\u2013344. Springer-Verlag, April 2001."}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45789-5_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,21]],"date-time":"2019-02-21T08:01:49Z","timestamp":1550736109000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45789-5_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540442356","9783540457893"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-45789-5_16","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}