{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T04:37:08Z","timestamp":1778301428409,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540631668","type":"print"},{"value":"9783540691952","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63166-6_39","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:13:58Z","timestamp":1330298038000},"page":"400-411","source":"Crossref","is-referenced-by-count":57,"title":["Symbolic model checking of infinite state systems using presburger arithmetic"],"prefix":"10.1007","author":[{"given":"Tevfik","family":"Bultan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Richard","family":"Gerber","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"William","family":"Pugh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"issue":"1","key":"39_CR1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P. H. Ho, X. Nicollin, A. Olivero, J. Sifakis, S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138(1):3\u201334, 1995.","journal-title":"Theoretical Computer Science"},{"key":"39_CR2","unstructured":"G. R. Andrews. Concurrent Programming, Principles and Practice. The Benjamin\/Cummings Publishing Company, 1991."},{"key":"39_CR3","unstructured":"A. Arnold. Finite Transition Systems: Semantics of Communicating Systems. Prentice Hall, 1994."},{"issue":"3","key":"39_CR4","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R. E. Bryant","year":"1992","unstructured":"R. E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293\u2013318, 1992.","journal-title":"ACM Computing Surveys"},{"key":"39_CR5","doi-asserted-by":"crossref","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. H. Hwang. Symbolic model checking: 1020 states and beyond. In Proc. 5th Annual IEEE Symp. on Logic in Computer Science, pages 428\u2013439, 1990.","DOI":"10.1109\/LICS.1990.113767"},{"key":"39_CR6","doi-asserted-by":"crossref","unstructured":"T. Bultan, J. Fischer, and R. Gerber. Compositional verification by model checking for counter-examples. In Proc. 1996 Int. Symp. on Software Testing and Analysis, pages 224\u2013238, 1996.","DOI":"10.1145\/229000.226321"},{"issue":"2","key":"39_CR7","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finitestate concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263, 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"39_CR8","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, O. Grumberg, D. E. Long Model checking and abstraction. In Proc. 18th Annual ACM Symp. on Principles of Programming Languages, pages 343\u2013354, 1992.","DOI":"10.1145\/143165.143235"},{"key":"39_CR9","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, D. E. Long, and K. L. McMillan. Compositional model checking. In Proc. 4th Annual IEEE Symp. on Logic in Computer Science, pages 464\u2013475, 1989.","DOI":"10.1109\/LICS.1989.39190"},{"key":"39_CR10","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 Proc. 4th Annual ACM Symp. on Principles of Programming Languages, pages 238\u2013252, 1977.","DOI":"10.1145\/512950.512973"},{"key":"39_CR11","doi-asserted-by":"crossref","unstructured":"P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proc. 5th Annual ACM Symp. on Principles of Programming Languages, pages 84\u201397, 1978.","DOI":"10.1145\/512760.512770"},{"key":"39_CR12","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/3-540-60045-0_40","volume":"939","author":"J. Dingel","year":"1995","unstructured":"J. Dingel, and T. Filkorn. Model checking for infinite state systems using data abstraction, assumption-commitment style reasoning and theorem proving. In Proc. 7th Int. Conference on Computer Aided Verification, LNCS 939, pages 54\u201369, 1995.","journal-title":"Proc. 7th Int. Conference on Computer Aided Verification, LNCS"},{"key":"39_CR13","first-page":"27","volume":"7","author":"M. J. Fischer","year":"1974","unstructured":"M. J. Fischer and M. O. Rabin. Super-Exponential Complexity of Presburger Arithmetic. SIAM-AMS Proc., Volume 7, pages 27\u201341, 1974.","journal-title":"SIAM-AMS Proc."},{"key":"39_CR14","unstructured":"P. Godefroid. Partial-order methods for the verification of concurrent systems: An approach to the state-explosion problem. Ph.D. Thesis, Universite De Liege, 1994."},{"key":"39_CR15","unstructured":"W. Kelly, V. Maslov, W. Pugh, E. Rosser, T. Shpeisman and D. Wonnacott. The Omega Library (version 1.00) interface guide. Available at <http:\/\/www.cs.umd.edu\/projects\/omega>."},{"key":"39_CR16","unstructured":"W. Kelly, W. Pugh, E. Rosser and T. Shpeisman. Transitive closure of infinite graphs and its applications. Technical Report CS-TR-3457, UMIACS-TR-95-48, Department of Computer Science, University of Maryland, 1994."},{"key":"39_CR17","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1145\/135226.135233","volume":"8","author":"W. Pugh","year":"1992","unstructured":"W. Pugh. The Omega test: a fast and practical integer programming algorithm for dependence analysis. Communications of the ACM, 8:102\u2013104, 1992.","journal-title":"Communications of the ACM"},{"issue":"3","key":"39_CR18","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1145\/158439.158441","volume":"25","author":"A. U. Shankar","year":"1993","unstructured":"A. Udaya Shankar. An introduction to assertional reasoning for concurrent systems. ACM Computing Surveys, 25(3):225\u2013262, 1993.","journal-title":"ACM Computing Surveys"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63166-6_39.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:38:58Z","timestamp":1742600338000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63166-6_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631668","9783540691952"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-63166-6_39","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997]]}}}