{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:25:35Z","timestamp":1725560735292},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540281955"},{"type":"electronic","value":"9783540318996"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11537328_9","type":"book-chapter","created":{"date-parts":[[2010,7,22]],"date-time":"2010-07-22T20:02:25Z","timestamp":1279828945000},"page":"75-90","source":"Crossref","is-referenced-by-count":30,"title":["Symbolic Model Checking for Asynchronous Boolean Programs"],"prefix":"10.1007","author":[{"given":"Byron","family":"Cook","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/10722468_7","volume-title":"SPIN Model Checking and Software Verification","author":"T. Ball","year":"2000","unstructured":"Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for Boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 113\u2013130. Springer, Heidelberg (2000)"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/3-540-44585-4_30","volume-title":"Computer Aided Verification","author":"J. Esparza","year":"2001","unstructured":"Esparza, J., Schwoon, S.: A BDD-based model checker for recursive programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 324\u2013336. Springer, Heidelberg (2001)"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/3-540-45319-9_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2001","unstructured":"Ball, T., Chaki, S., Rajamani, S.K.: Parameterized verification of multithreaded software libraries. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, p. 158. Springer, Heidelberg (2001)"},{"key":"9_CR5","first-page":"7","volume-title":"Proceedings of MEMOCODE 2004","author":"H. Jain","year":"2004","unstructured":"Jain, H., Clarke, E., Kroening, D.: Verification of SpecC and Verilog using predicate abstraction. In: Proceedings of MEMOCODE 2004, pp. 7\u201316. IEEE, Los Alamitos (2004)"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and Static Driver Verifier: Technology transfer of formal methods inside Microsoft. In: IFM (2004)","DOI":"10.1007\/978-3-540-24756-2_1"},{"key":"9_CR7","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1145\/503272.503279","volume-title":"POPL 2002: Symposium on Principles of Programming Languages","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL 2002: Symposium on Principles of Programming Languages, pp. 58\u201370. ACM Press, New York (2002)"},{"key":"9_CR8","first-page":"78","volume-title":"ICCAD","author":"O. Coudert","year":"1990","unstructured":"Coudert, O., Madre, J.: A unified framework for the formal verification of sequential circuits. In: ICCAD, pp. 78\u201382. IEEE, Los Alamitos (1990)"},{"key":"9_CR9","doi-asserted-by":"crossref","first-page":"402","DOI":"10.1145\/309847.309968","volume-title":"DAC","author":"M.D. Aagaard","year":"1999","unstructured":"Aagaard, M.D., Jones, R.B., Seger, C.J.H.: Formal verification using parametric representations of boolean constraints. In: DAC, pp. 402\u2013407. ACM Press, New York (1999)"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/11527695_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"A. Biere","year":"2005","unstructured":"Biere, A.: Resolve and expand. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 59\u201370. Springer, Heidelberg (2005)"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: ICCAD (2002)","DOI":"10.1145\/774572.774637"},{"key":"9_CR12","unstructured":"Leino, K.R.M.: A SAT characterization of Boolean-program correctness. In: SPIN (2003)"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., et al.: NuSMV 2: An opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"9_CR14","volume-title":"POPL 2005: Symposium on Principles of Programming Languages","author":"C. Flanagan","year":"2005","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: POPL 2005: Symposium on Principles of Programming Languages. ACM Press, New York (2005)"},{"key":"9_CR15","first-page":"197","volume-title":"Proc. Formal Description Techniques, FORTE 1994","author":"G. Holzmann","year":"1994","unstructured":"Holzmann, G., Peled, D.: An improvement in formal verification. In: Proc. Formal Description Techniques, FORTE 1994, pp. 197\u2013211. Chapman & Hall, Boca Raton (1994)"},{"key":"9_CR16","first-page":"97","volume":"18","author":"R. Alur","year":"2001","unstructured":"Alur, R., Brayton, R.K., Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Partial-order reduction in symbolic state-space exploration. FMSD\u00a018, 97\u2013116 (2001)","journal-title":"FMSD"},{"key":"9_CR17","unstructured":"Jussila, T., Niemel\u00e4, I.: Parallel program verification using BMC. In: ECAI 2002 Workshop on Model Checking and Artificial Intelligence, pp. 59\u201366 (2002)"},{"key":"9_CR18","first-page":"122","volume-title":"POPL","author":"O. Grumberg","year":"2005","unstructured":"Grumberg, O., Lerda, F., Strichman, O., Theobald, M.: Proof-guided underapproximation-widening for multi-process systems. In: POPL, pp. 122\u2013131. ACM Press, New York (2005)"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Lerda, F., Sinha, N., Theobald, M.: Symbolic model checking of software. In: Software Model Checking (SoftMC). ENTCS (2003)","DOI":"10.1016\/S1571-0661(05)80008-8"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/BFb0028774","volume-title":"Computer Aided Verification","author":"R. Alur","year":"1998","unstructured":"Alur, R., Henzinger, T., Mang, F., Qadeer, S., Rajamani, S., Tasiran, S.: Mocha: Modularity in model checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 521\u2013525. Springer, Heidelberg (1998)"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-540-45069-6_27","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Qadeer, S.: Thread modular abstraction refinement. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 262\u2013274. Springer, Heidelberg (2003)"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-31980-1_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Qadeer","year":"2005","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 93\u2013107. Springer, Heidelberg (2005)"},{"key":"9_CR23","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":"9_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/BFb0028753","volume-title":"Computer Aided Verification","author":"M. Col\u00f3n","year":"1998","unstructured":"Col\u00f3n, M., Uribe, T.: Generating finite-state abstractions of reactive systems using decision procedures. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 293\u2013304. Springer, Heidelberg (1998)"},{"key":"9_CR25","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"Holzmann, G.: The model checker SPIN. IEEE Trans. on Software Engineering\u00a023, 279\u2013295 (1997)","journal-title":"IEEE Trans. on Software Engineering"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"D. Peled","year":"1993","unstructured":"Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697. Springer, Heidelberg (1993)"},{"key":"9_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-540-39724-3_6","volume-title":"Correct Hardware Design and Verification Methods","author":"S. Barner","year":"2003","unstructured":"Barner, S., Rabinovitz, I.: Effcient symbolic model checking of software using partial disjunctive partitioning. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 35\u201350. Springer, Heidelberg (2003)"},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-28644-8_1","volume-title":"CONCUR 2004 - Concurrency Theory","author":"T. Andrews","year":"2004","unstructured":"Andrews, T., et al.: Zing: Exploiting program structure for model checking concurrent software. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 1\u201315. Springer, Heidelberg (2004)"},{"key":"9_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/11513988_30","volume-title":"Computer Aided Verification","author":"B. Cook","year":"2005","unstructured":"Cook, B., Kroening, D., Sharygina, N.: Cogent: Accurate theorem proving for program verification. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 296\u2013300. Springer, Heidelberg (2005)"},{"key":"9_CR30","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1145\/996566.996711","volume-title":"DAC 2004","author":"P. Chauhan","year":"2004","unstructured":"Chauhan, P., Clarke, E., Kroening, D.: A SAT-based algorithm for reparameterization in symbolic simulation. In: DAC 2004, pp. 524\u2013529. ACM Press, New York (2004)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11537328_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,2]],"date-time":"2023-06-02T07:49:20Z","timestamp":1685692160000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11537328_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540281955","9783540318996"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/11537328_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}