{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:27:44Z","timestamp":1725488864359},"publisher-location":"Berlin, Heidelberg","reference-count":25,"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_7","type":"book-chapter","created":{"date-parts":[[2007,8,11]],"date-time":"2007-08-11T09:50:10Z","timestamp":1186825810000},"page":"52-68","source":"Crossref","is-referenced-by-count":6,"title":["Representing and Approximating Transfer Functions in Abstract Interpretation of Hetereogeneous Datatypes"],"prefix":"10.1007","author":[{"given":"B.","family":"Jeannet","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,9,5]]},"reference":[{"key":"7_CR1","series-title":"Lect Notes Comput Sci","volume-title":"Computer Aided Verification, CAV\u201998","author":"P. A. Abdulla","year":"1998","unstructured":"P. Aziz Abdulla, A. Bouajjani, and B. Jonsson. On-the-fly analysis of systems with unbounded, lossy fifo channels. In Computer Aided Verification, CAV\u201998, volume 1427 of LNCS, July 1998."},{"issue":"2\/3","key":"7_CR2","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1023\/A:1008699807402","volume":"10","author":"R. Bahar","year":"1997","unstructured":"R. Bahar, E. Frohm, C. Gaona, G. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Algebraic decision diagrams and their applications. Formal Methods in System Design, 10(2\/3):171\u2013206, April 1997.","journal-title":"Formal Methods in System Design"},{"key":"7_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6_30","volume-title":"Computer Aided Verification, CAV\u201999","author":"G. Behrmann","year":"1999","unstructured":"G. Behrmann, K. G. Larsen, J. Pearson, C. Weise, and W. Yi. Efficient timed reachability analysis using clock difference diagrams. In Computer Aided Verification, CAV\u201999, volume 1633 of LNCS, July 1999."},{"key":"7_CR4","series-title":"Lect Notes Comput Sci","volume-title":"Computer Aided Verification, CAV\u201996","author":"B. Boigelot","year":"1996","unstructured":"B. Boigelot and P. Godefroid. Symbolic verification of communication protocols with infinite state spaces using QDDs. In Computer Aided Verification, CAV\u201996, volume 1102 of LNCS, July 1996."},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"T. Bultan, R. Gerber, and C. League. Composite model checking: Verification with type-specific symbolic representations. ACM Transactions on Software Engineering and Methodology, 9(1), January 2000.","DOI":"10.1145\/332740.332746"},{"key":"7_CR6","series-title":"Lect Notes Comput Sci","volume-title":"Computer Aided Verification, CAV\u201997","author":"T. Bultan","year":"1997","unstructured":"T. Bultan, R. Gerber, and W. Pugh. Symbolic model checking of infinite state systems using presburger arithmetic. In Computer Aided Verification, CAV\u201997, volume 1254 of LNCS, June 1997."},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"A. Cortesi, B. Le Charlier, and P. Van Hentenryck. Combination of abstract domains for logic programming: open product and generic pattern construct. Science of Computer Programming, 38, 2000.","DOI":"10.1016\/S0167-6423(99)00045-3"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th ACM Symposium on Principles of Programming Languages, POPL\u201977, Los Angeles, January 1977.","DOI":"10.1145\/512950.512973"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In 6th ACM Symposium on Principles of Programming Languages, POPL\u201979, San Antonio, January 1979.","DOI":"10.1145\/567752.567778"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 1992.","DOI":"10.1093\/logcom\/2.4.511"},{"key":"7_CR11","series-title":"Lect Notes Comput Sci","volume-title":"Static Analysis Symposium, SAS\u201901","author":"R. Giacobazzi","year":"2001","unstructured":"R. Giacobazzi and E. Qintarelli. Incompleteness, counterexamples, and refinement in abstract model-checking. In Static Analysis Symposium, SAS\u201901, volume 2126 of LNCS, July 2001."},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"N. Halbwachs. Synchronous programming of reactive systems. Kluwer Academic Pub., 1993.","DOI":"10.1007\/978-1-4757-2231-4"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language lustre. Proceedings of the IEEE, 79(9):1305\u20131320, September 1991.","DOI":"10.1109\/5.97300"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, Y.E. Proy, and P. Roumanoff. Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 11(2), August 1997.","DOI":"10.1023\/A:1008678014487"},{"key":"7_CR15","series-title":"Lect Notes Comput Sci","volume-title":"Computer Aided Verification, CAV\u201997","author":"T. Henzinger","year":"1997","unstructured":"T. Henzinger, P.-H. Ho, and H. Wong-To\u00ef. HyTech: A Model Checker for Hybrid Systems. In Computer Aided Verification, CAV\u201997, number 1254 in LNCS, June 1997."},{"key":"7_CR16","unstructured":"B. Jeannet. Dynamic partitioning in linear relation analysis. Application to the verification of reactive systems. Formal Methods in System Design. 40 pages, to appear, available as a BRICS Research Report http:\/\/www.brics.dk\/RS\/00\/38 ."},{"key":"7_CR17","series-title":"Lect Notes Comput Sci","volume-title":"Static Analysis Symposium, SAS\u201999","author":"B. Jeannet","year":"1999","unstructured":"B. Jeannet, N. Halbwachs, and P. Raymond. Dynamic partitioning in analyses of numerical properties. In Static Analysis Symposium, SAS\u201999, volume 1694 of LNCS, Venezia (Italy), September 1999."},{"key":"7_CR18","unstructured":"C. Mauras. Calcul symbolique et automates interpr\u00e9t\u00e9s. Technical Report 10, IRCyN, November 1996."},{"key":"7_CR19","volume-title":"Computer Science Logic","author":"J. M\u00f8ller","year":"1999","unstructured":"J. M\u00f8ller, J. Lichtenberg, H. R. Andersen, and H. Hulgaard. Difference decision diagrams. In Computer Science Logic, The IT University of Copenhagen, Denmark, September 1999."},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"G. Nelson and C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2), 1979.","DOI":"10.1145\/357073.357079"},{"key":"7_CR21","unstructured":"F. Nielson. Tensor products generalize the relational data flow analysis method. In Fourth Hungarian Computer Science Conference, 1985."},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"F. Nielson and H. R. Nielson. The tensor product in wadler\u2019s analysis of list. Science of Computer Programming, 22, 1994.","DOI":"10.1016\/0167-6423(94)00009-3"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"R. Shostak. Deciding combination of theories. Journal of the ACM, 31(1), 1984.","DOI":"10.1145\/2422.322411"},{"key":"7_CR24","unstructured":"H. Sipma, T. Uribe, and Z. Manna. Model checking and deduction for infinite-state systems. In Logical Perspectives on Language and Information. CSLI publications, 2001."},{"key":"7_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45319-9_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, TACAS\u201901","author":"T. Yavuz-Kahveci","year":"2001","unstructured":"T. Yavuz-Kahveci, M. Tuncer, and T. Bultan. A library for composite symbolic representations. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS\u201901, volume 2031 of LNCS, 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_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T19:24:04Z","timestamp":1556738644000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45789-5_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540442356","9783540457893"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-45789-5_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}