{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T10:22:28Z","timestamp":1790850148110,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540441441","type":"print"},{"value":"9783540457190","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45719-4_33","type":"book-chapter","created":{"date-parts":[[2007,10,9]],"date-time":"2007-10-09T10:55:00Z","timestamp":1191927300000},"page":"489-494","source":"Crossref","is-referenced-by-count":6,"title":["BRAIN: Backward Reachability Analysis with Integers"],"prefix":"10.1007","author":[{"given":"Tatiana","family":"Rybina","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2002,9,2]]},"reference":[{"issue":"1","key":"33_CR1","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":"33_CR2","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":"33_CR3","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":"3","key":"33_CR4","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"},{"issue":"1","key":"33_CR5","doi-asserted-by":"publisher","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":"33_CR6","unstructured":"J. Rushby. Specification, proof checking and model checking for protocols and distributed systems with PVS, November 1997. Tutorial notes for FORTE\/PSTV\u201997, http:\/\/pvs.csl.sri.com\/pvs\/examples\/forte97-tutorial\/forte97.html ."},{"key":"33_CR7","unstructured":"T. Rybina and A. Voronkov. A logical reconstruction of reachability. In Submitted, 2002."},{"key":"33_CR8","doi-asserted-by":"crossref","unstructured":"T. Rybina and A. Voronkov. Using canonical representations of solutions to speed up infinite-state model checking. In Proceedings of CAV 2002, 2002. To appear.","DOI":"10.1007\/3-540-45657-0_32"},{"key":"33_CR9","unstructured":"A. Voronkov. An incremental algorithm for finding the basis of solutions to systems of linear Diophantine equations and inequations. unpublished, January 2002."}],"container-title":["Lecture Notes in Computer Science","Algebraic Methodology and Software Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45719-4_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,26]],"date-time":"2020-04-26T23:37:52Z","timestamp":1587944272000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45719-4_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540441441","9783540457190"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/3-540-45719-4_33","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}