{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:42:04Z","timestamp":1725565324403},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540223429"},{"type":"electronic","value":"9783540278139"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27813-9_25","type":"book-chapter","created":{"date-parts":[[2010,9,14]],"date-time":"2010-09-14T04:57:57Z","timestamp":1284440277000},"page":"321-333","source":"Crossref","is-referenced-by-count":30,"title":["Widening Arithmetic Automata"],"prefix":"10.1007","author":[{"given":"Constantinos","family":"Bartzis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tevfik","family":"Bultan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"25_CR1","unstructured":"The Omega project.: http:\/\/www.cs.umd.edu\/projects\/omega\/"},{"key":"25_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-540-45069-6_26","volume-title":"Computer Aided Verification","author":"C. Bartzis","year":"2003","unstructured":"Bartzis, C., Bultan, T.: Efficient image computation in infinite state model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 249\u2013261. Springer, Heidelberg (2003)"},{"issue":"4","key":"25_CR3","first-page":"605","volume":"14","author":"C. Bartzis","year":"2003","unstructured":"Bartzis, C., Bultan, T.: Efficient symbolic representations for arithmetic constraints in verification. Computer Science\u00a014(4), 605\u2013624 (2003)","journal-title":"Computer Science"},{"key":"25_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-45069-6_24","volume-title":"Computer Aided Verification","author":"B. Boigelot","year":"2003","unstructured":"Boigelot, B., Legay, A., Wolper, P.: Iterating transducers in the large. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 223\u2013235. Springer, Heidelberg (2003)"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Computer Aided Verification, pp. 403\u2013418 (2000)","DOI":"10.1007\/10722167_31"},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1007\/3-540-61064-2_27","volume-title":"Trees in Algebra and Programming - CAAP \u201996","author":"A. Boudet","year":"1996","unstructured":"Boudet, A., Comon, H.: Diophantine equations, Presburger arithmetic and finite automata. In: Kirchner, H. (ed.) CAAP 1996. LNCS, vol.\u00a01059, pp. 30\u201343. Springer, Heidelberg (1996)"},{"issue":"4","key":"25_CR7","doi-asserted-by":"publisher","first-page":"747","DOI":"10.1145\/325478.325480","volume":"21","author":"T. Bultan","year":"1999","unstructured":"Bultan, T., Gerber, R., Pugh, W.: Model-checking concurrent systems with unbounded integer variables: Symbolic representations, approximations, and experimental results. ACM Transactions on Programming Languages and Systems\u00a021(4), 747\u2013789 (1999)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Bultan, T., Yavuz-Kahveci, T.: Action language verifier. In: Proceedings of the 16th IEEE International Conference on Automated Software Engineering (2001)","DOI":"10.1109\/ASE.2001.989834"},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th Annual ACM Symposium on Principles of Programming Languages, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th Annual ACM Symposium on Principles of Programming, pp. 84\u201397 (1978)","DOI":"10.1145\/512760.512770"},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/3-540-44585-4_27","volume-title":"Computer Aided Verification","author":"D. Dams","year":"2001","unstructured":"Dams, D., Lakhnech, Y., Steffen, M.: Iterating transducers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 286. Springer, Heidelberg (2001)"},{"key":"25_CR12","unstructured":"Halbwachs, N.: D\u00e9termination automatique de relations lin\u00e9aires v\u00e9rifi\u00e9es par les variables d\u2019un programme. PhD thesis, University of Grenoble (March 1979)"},{"issue":"2","key":"25_CR13","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N. Halbwachs","year":"1997","unstructured":"Halbwachs, N., Proy, Y.E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Methods in System Design\u00a011(2), 157\u2013185 (1997)","journal-title":"Formal Methods in System Design"},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"Jonsson, B., Nilsson Transitive, M.: closures of regular relations for verifying infinite-state systems. In: Tools and Algorithms for Construction and Analysis of Systems, pp. 220\u2013234 (2000)","DOI":"10.1007\/3-540-46419-0_16"},{"key":"25_CR15","doi-asserted-by":"crossref","unstructured":"Rybina, T., Voronkov, A.: Using canonical representations of solutions to speed up infinite-state model checking. In: Proceedings of the 14th International Conference on Computer Aided Verification, pp. 400\u2013411 (2002)","DOI":"10.1007\/3-540-45657-0_32"},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-46419-0_1","volume-title":"Proceedings of the 6th Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Wolper","year":"2000","unstructured":"Wolper, P., Boigelot, B.: On the construction of automata from linear arithmetic constraints. In: Proceedings of the 6th Conference on Tools and Algorithms for the Construction and Analysis of Systems, LNCS , April 2000. pp. 1\u201319. Springer, Heidelberg (2000)"},{"key":"25_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/3-540-45319-9_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Yavuz-Kahveci","year":"2001","unstructured":"Yavuz-Kahveci, T., Tuncer, M., Bultan, T.: Composite symbolic library. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 335\u2013344. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27813-9_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:22:02Z","timestamp":1605759722000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27813-9_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540223429","9783540278139"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27813-9_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}