{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:26:48Z","timestamp":1725492408163},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540403913"},{"type":"electronic","value":"9783540449775"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-44977-9_30","type":"book-chapter","created":{"date-parts":[[2007,10,16]],"date-time":"2007-10-16T14:20:28Z","timestamp":1192544428000},"page":"282-288","source":"Crossref","is-referenced-by-count":3,"title":["Automata-Based Representations for Arithmetic Constraints in Automated Verification"],"prefix":"10.1007","author":[{"given":"Constantinos","family":"Bartzis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tev.k","family":"Bultan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,6,24]]},"reference":[{"key":"30_CR1","unstructured":"C. Bartzis and T. Bultan. Efficient symbolic representations for arithmetic constraints in verification. Technical Report TRCS-2002-16, Computer Science Department, University of California, Santa Barbara, June 2002."},{"key":"30_CR2","series-title":"Lect Notes Comput Sci","volume-title":"Diophantine equations, Presburger arithmetic and finite automata","author":"A. Boudet","year":"1996","unstructured":"A. Boudet and H. Comon. Diophantine equations, Presburger arithmetic and finite automata. In H. Kirchner, editor, Proceedings of the 21st International Colloquium on Trees in Algebra and Programming-CAAP\u201996, volume 1059 of Lecture Notes in Computer Science, pages 30-43. Springer-Verlag, April 1996."},{"issue":"4","key":"30_CR3","doi-asserted-by":"publisher","first-page":"747","DOI":"10.1145\/325478.325480","volume":"21","author":"T. Bultan","year":"1999","unstructured":"Tevfik Bultan, Richard Gerber, and William 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"},{"key":"30_CR4","doi-asserted-by":"crossref","unstructured":"G. Delzanno and T. Bultan. Constraint-based verification of client-server protocols. In Proceedings of the 7th International Conference on Principles and Practice of Constraint Programming, 2001.","DOI":"10.1007\/3-540-45578-7_20"},{"issue":"3","key":"30_CR5","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/s100090100049","volume":"3","author":"G. Delzanno","year":"2001","unstructured":"Giorgio Delzanno and Andreas Podelski. Constraint-based deductive model checking. Journal of Software Tools and Technology Transfer, 3(3):250\u2013270, 2001.","journal-title":"Journal of Software Tools and Technology Transfer"},{"key":"30_CR6","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T. A. Henzinger","year":"1997","unstructured":"T. A. Henzinger, P. Ho, and H. Wong-Toi. Hytech: a model checker for hybrid systems. Software Tools for Technology Transfer, 1:110\u2013122, 1997.","journal-title":"Software Tools for Technology Transfer"},{"key":"30_CR7","unstructured":"Nils Klarlund and Anders M\u00f8ller. MONA Version 1.4 User Manual. BRICS Notes Series NS-01-1, Department of Computer Science, University of Aarhus, January 2001."},{"key":"30_CR8","doi-asserted-by":"crossref","unstructured":"T. R. Shiple, J. H. Kukula, and R. K. Ranjan. A comparison of Presburger engines for EFSM reachability. In Proceedings of the 10th International Conference on Computer-Aided Verification, 1998.","DOI":"10.1007\/BFb0028752"},{"key":"30_CR9","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"On the construction of automata from linear arithmetic constraints","author":"P. Wolper","year":"2000","unstructured":"P. Wolper and B. Boigelot. On the construction of automata from linear arithmetic constraints. In S. Graf and M. Schwartzbach, editors, Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, pages 1\u201319. Springer, April 2000."},{"key":"30_CR10","series-title":"Lect Notes Comput Sci","first-page":"335","volume-title":"Composite symbolic library","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","Implementation and Application of Automata"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44977-9_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,27]],"date-time":"2020-04-27T06:53:07Z","timestamp":1587970387000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44977-9_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540403913","9783540449775"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-44977-9_30","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}