{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:29:18Z","timestamp":1725560958914},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540206804"},{"type":"electronic","value":"9783540245971"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-24597-1_34","type":"book-chapter","created":{"date-parts":[[2010,7,29]],"date-time":"2010-07-29T07:39:20Z","timestamp":1280389160000},"page":"399-407","source":"Crossref","is-referenced-by-count":0,"title":["Reasoning about Infinite State Systems Using Boolean Methods"],"prefix":"10.1007","author":[{"given":"Randal E.","family":"Bryant","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"34_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/BFb0031808","volume-title":"Formal Methods in Computer-Aided Design","author":"C. Barrett","year":"1996","unstructured":"Barrett, C., Dill, D., Levitt, J.: Validity checking for combinations of theories with equality. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 187\u2013201. Springer, Heidelberg (1996)"},{"key":"34_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/3-540-48683-6_40","volume-title":"Computer Aided Verification","author":"R.E. Bryant","year":"1999","unstructured":"Bryant, R.E., German, S., Velev, M.N.: Exploiting positive equality in a logic of equality with uninterpreted functions. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 470\u2013482. Springer, Heidelberg (1999)"},{"key":"34_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-45657-0_7","volume-title":"Computer Aided Verification","author":"R.E. Bryant","year":"2002","unstructured":"Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 78\u201392. Springer, Heidelberg (2002)"},{"key":"34_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"400","DOI":"10.1007\/3-540-63166-6_39","volume-title":"Computer Aided Verification","author":"T. Bultan","year":"1997","unstructured":"Bultan, T., Gerber, R., Pugh, W.: Symbolic model checking of infinite state systems using Presburger arithmetic. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 400\u2013411. Springer, Heidelberg (1997)"},{"key":"34_CR5","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L.: Sequential circuit verification using symbolic model checking. In: 27th Design Automation Conference (DAC 1990), pp. 46\u201351 (1990)","DOI":"10.1145\/123186.123223"},{"key":"34_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","volume-title":"Computer Aided Verification","author":"J.R. Burch","year":"1994","unstructured":"Burch, J.R., Dill, D.L.: Automated verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 68\u201380. Springer, Heidelberg (1994)"},{"issue":"1","key":"34_CR7","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E.M. Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design\u00a019(1), 7\u201334 (2001)","journal-title":"Formal Methods in System Design"},{"key":"34_CR8","unstructured":"German, S.: Personal communication"},{"key":"34_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"34_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/3-540-48683-6_7","volume-title":"Computer Aided Verification","author":"R. Hosabettu","year":"1999","unstructured":"Hosabettu, R., Gopalakrishnan, G., Srivas, M.: Proof of correctness of a processor with reorder buffer using the completion function approach. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 47\u201359. Springer, Heidelberg (1999)"},{"key":"34_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/3-540-36126-X_9","volume-title":"Formal Methods in Computer-Aided Design","author":"S.K. Lahiri","year":"2002","unstructured":"Lahiri, S.K., Seshia, S.A., Bryant, R.E.: Modeling and verification of out-oforder microprocessors in UCLID. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 142\u2013159. Springer, Heidelberg (2002)"},{"key":"34_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-540-45069-6_33","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2003","unstructured":"Lahiri, S.K., Bryant, R.E.: Deductive verification of advanced out-of-order microprocessors. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 341\u2013354. Springer, Heidelberg (2003)"},{"key":"34_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-540-45069-6_15","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2003","unstructured":"Lahiri, S.K., Bryant, R.E., Cook, B.: A symbolic approach to predicate abstraction. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 141\u2013153. Springer, Heidelberg (2003)"},{"key":"34_CR14","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L. Lamport","year":"1974","unstructured":"Lamport, L.: A new solution of Dijkstra\u2019s concurrent programming problem. Communications of the ACM\u00a017, 453\u2013455 (1974)","journal-title":"Communications of the ACM"},{"issue":"1-3","key":"34_CR15","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/S0167-6423(99)00030-1","volume":"37","author":"K. McMillan","year":"2000","unstructured":"McMillan, K.: A methodology for hardware verification using compositional model checking. Science of Computer Programming\u00a037(1-3), 279\u2013309 (2000)","journal-title":"Science of Computer Programming"},{"key":"34_CR16","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: 38th Design Automation Conference (DAC 2001), pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"34_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"2001","unstructured":"Pnueli, A., Ruah, S., Zuck, L.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 82\u201397. Springer, Heidelberg (2001)"},{"key":"34_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/BFb0028740","volume-title":"Computer Aided Verification","author":"J. Sawada","year":"1998","unstructured":"Sawada, J., Hunt Jr., W.A.: Processor verification with precise exceptions and speculative execution. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 135\u2013146. Springer, Heidelberg (1998)"},{"key":"34_CR19","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"A.P. Sistla","year":"1992","unstructured":"Sistla, A.P., German, S.M.: Reasoning about systems with many processes. J. ACM\u00a039, 675\u2013735 (1992)","journal-title":"J. ACM"},{"key":"34_CR20","doi-asserted-by":"crossref","unstructured":"Velev, M.N., Bryant, R.E.: Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. In: 38th Design Automation Conference (DAC 2001), pp. 226\u2013231 (2001)","DOI":"10.1145\/378239.378469"}],"container-title":["Lecture Notes in Computer Science","FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24597-1_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T20:46:37Z","timestamp":1558298797000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24597-1_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540206804","9783540245971"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24597-1_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}