{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:06:43Z","timestamp":1725484003344},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439974"},{"type":"electronic","value":"9783540456575"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45657-0_32","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T10:59:43Z","timestamp":1179572383000},"page":"386-400","source":"Crossref","is-referenced-by-count":13,"title":["Using Canonical Representations of Solutions to Speed Up Infinite-State Model Checking"],"prefix":"10.1007","author":[{"given":"Tatiana","family":"Rybina","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,9,20]]},"reference":[{"issue":"1\u20132","key":"32_CR1","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1006\/inco.1999.2843","volume":"160","author":"P. A. Abdulla","year":"2000","unstructured":"P. A. Abdulla, K. Cerans, B. Jonsson, and Y.-K. Tsay. Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation, 160(1\u20132): 109\u2013127, January 2000.","journal-title":"Information and Computation"},{"issue":"1","key":"32_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/S0304-3975(96)00195-8","volume":"173","author":"F. Ajili","year":"1997","unstructured":"F. Ajili and E. Contejean. Avoiding slack variables in the solving of linear Diophantine equations and inequations. Theoretical Computer Science, 173(1):183\u2013208, 1997.","journal-title":"Theoretical Computer Science"},{"key":"32_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/3-540-48320-9_14","volume-title":"CONCUR\u201999: Concurrency Theory, 10th International Conference","author":"B. B\u00e9rard","year":"1999","unstructured":"B. B\u00e9rard and L. Fribourg. Reachability analysis of (timed) Petri nets using real arithmetic. In J. C. M. Baeten and S. Mauw, editors, CONCUR\u201999: Concurrency Theory, 10th International Conference, volume 1664 of Lecture Notes in Computer Science, pages 178\u2013193. Springer Verlag, 1999."},{"key":"32_CR4","doi-asserted-by":"crossref","unstructured":"T. Bultan. Action Language: a specification language for model checking reactive systems. In ICSE 2000, Proceedings of the 22nd International Conference on Software Engineering, pages 335\u2013344, Limerick, Ireland, 2000. ACM.","DOI":"10.1145\/337180.337219"},{"issue":"4","key":"32_CR5","doi-asserted-by":"publisher","first-page":"747","DOI":"10.1145\/325478.325480","volume":"21","author":"T. Bultan","year":"1999","unstructured":"T. Bultan, R. Gerber, and W. Pugh. Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results. ACM Transactions on Programming Languages and Systems, 21(4):747\u2013789, 1999.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1","key":"32_CR6","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1006\/inco.1994.1067","volume":"113","author":"E. Contejean","year":"1994","unstructured":"E. Contejean and H. Devie. An efficient incremental algorithm for solving of systems of linear diophantine equations. Information and Computation, 113(1):143\u2013172, 1994.","journal-title":"Information and Computation"},{"key":"32_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/10722167_8","volume-title":"Computer Aided Verification, 12th International Conference, CAV 2000","author":"G. Delzanno","year":"2000","unstructured":"G. Delzanno. Automatic verification of parametrized cache coherence protocols. In A. E. Emerson and A. P. Sistla, editors, Computer Aided Verification, 12th International Conference, CAV 2000, volume 1855 of Lecture Notes in Computer Science, pages 53\u201368. Springer Verlag, 2000."},{"issue":"3","key":"32_CR8","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/s100090100049","volume":"3","author":"G. Delzanno","year":"2001","unstructured":"G. Delzanno and A. Podelski. Constraint-based deductive model checking. International Journal on Software Tools for Technology Transfer, 3(3):250\u2013270, 2001.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"32_CR9","doi-asserted-by":"crossref","unstructured":"J. Esparza, A. Finkel, and R. Mayr. On the verification of broadcast protocols. In 14th Annual IEEE Symposium on Logic in Computer Science (LICS\u201999), pages352\u2013359, Trento, Italy, 1999. IEEE Computer Society.","DOI":"10.1109\/LICS.1999.782630"},{"issue":"2","key":"32_CR10","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N. Halbwachs","year":"1997","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):157\u2013185, 1997.","journal-title":"Formal Methods in System Design"},{"issue":"1\u20132","key":"32_CR11","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T. A. Henzinger","year":"1997","unstructured":"T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. Hy-tech: a model checker for hybrid systems. International Journal on Software Tools for Technology Transfer, 1(1\u20132): 110\u2013122, 1997.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"32_CR12","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/BF01208503","volume":"36","author":"D. Hilbert","year":"1890","unstructured":"D. Hilbert. \u00dcber die Theorie der algebraischen Formen. Mathematische Annalen, 36:473\u2013534, 1890.","journal-title":"Mathematische Annalen"},{"issue":"3","key":"32_CR13","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O. Kupferman","year":"2001","unstructured":"O. Kupferman and M. Vardi. Model checking of safety properties. Formal Methods in System Design, 19(3):291\u2013314, 2001.","journal-title":"Formal Methods in System Design"},{"key":"32_CR14","doi-asserted-by":"crossref","unstructured":"W. Pugh. Counting solutions to Presburger formulas: how and why. ACM SIGPLAN Notices, 29(6):121\u2013134, June 1994. Proceedings of the ACM SIGPLAN\u201994 Conference on Programming Languages Design and Implementation (PLDI).","DOI":"10.1145\/178243.178254"},{"key":"32_CR15","unstructured":"T. Rybina and A. Voronkov. A logical reconstruction of reachability. submitted, 2002."},{"key":"32_CR16","unstructured":"A. Schrijver. Theory of Linear and Integer Programming. John Wiley and Sons, 1998."},{"key":"32_CR17","doi-asserted-by":"crossref","unstructured":"A. P. Tom\u00e1s and M. Filgueiras. An algorithm for solving systems of linear diophantine equations in naturals. In E. Costa and A. Cardoso, editors, Progress in Artificial Intelligence, 8th Portugese Conference on Artificial Intelligence, EPIA\u2019 97, volume 1323 of Lecture Notes in Artificial Intelligence, pages 73\u201384, Coimbra, Portugal, 1997. Springer Verlag.","DOI":"10.1007\/BFb0023912"},{"key":"32_CR18","unstructured":"A. Voronkov. An incremental algorithm for finding the basis of solutions to systems of linear Diophantine equations and inequations. unpublished, January 2002."},{"key":"32_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/3-540-45319-9_5","volume-title":"Tools and Algorithms for Construction and Analysis of Systems, 7th International Conference, TACAS 2001","author":"T. Yavuz-Kahveci","year":"2001","unstructured":"T. Yavuz-Kahveci, M. Tuncer, and T. Bultan. A library for composite symbolic representations. In T. Margaria, editor, Tools and Algorithms for Construction and Analysis of Systems, 7th International Conference, TACAS 2001, volume 1384 of Lecture Notes in Computer Science, pages 52\u201366, Genova, Italy, 2001. Springer Verlag."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45657-0_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,22]],"date-time":"2020-04-22T01:21:03Z","timestamp":1587518463000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45657-0_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439974","9783540456575"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-45657-0_32","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}