{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T20:06:15Z","timestamp":1773086775621,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":47,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540213772","type":"print"},{"value":"9783540247562","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24756-2_8","type":"book-chapter","created":{"date-parts":[[2010,7,27]],"date-time":"2010-07-27T20:18:31Z","timestamp":1280261911000},"page":"128-147","source":"Crossref","is-referenced-by-count":79,"title":["State\/Event-Based Software Model Checking"],"prefix":"10.1007","author":[{"given":"Sagar","family":"Chaki","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edmund M.","family":"Clarke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jo\u00ebl","family":"Ouaknine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nishant","family":"Sinha","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Anantharaman, T.S., Clarke, E.M., Foster, M.J., Mishra, B.: Compiling path expressions into VLSI circuits. In: Proceedings of POPL, pp. 191\u2013204 (1985)","DOI":"10.1145\/318593.318638"},{"key":"8_CR2","unstructured":"BLAST website, http:\/\/www-cad.eecs.berkeley.edu\/~rupak\/blast"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BFb0028755","volume-title":"Computer Aided Verification","author":"S. Bensalem","year":"1998","unstructured":"Bensalem, S., Lakhnech, Y., Owre, S.: Computing abstractions of infinite state systems compositionally and automatically. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 319\u2013331. Springer, Heidelberg (1998)"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: SIGPLAN Conference on Programming Language Design and Implementation, pp. 203\u2013213 (2001)","DOI":"10.1145\/378795.378846"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-45139-0_7","volume-title":"Model Checking Software","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 103\u2013122. Springer, Heidelberg (2001)"},{"key":"8_CR6","unstructured":"Browne, M.C.: Automatic verification of finite state machines using temporal logic. PhD thesis, Carnegie Mellon University, Technical report no. CMU-CS-89-117 (1989)"},{"key":"8_CR7","series-title":"Handbook of Process Algebra","first-page":"293","volume-title":"Modal Logics and Mu-Calculi : An Introduction","author":"J. Bradfield","year":"2001","unstructured":"Bradfield, J., Stirling, C.: Modal Logics and Mu-Calculi: An Introduction. Handbook of Process Algebra, pp. 293\u2013330. Elsevier, Amsterdam (2001)"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Burch, J.: Trace algebra for automatic verification of real-time concurrent systems. PhD thesis, Carnegie Mellon University, Technical report no. CMU-CS-92-179 (1992)","DOI":"10.21236\/ADA256199"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E.M., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: Proceedings of ICSE 2003, pp. 385\u2013395 (2003)","DOI":"10.1109\/ICSE.2003.1201217"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Chauhan, P., Clarke, E.M., Kukula, J.H., Sapra, S., Veith, H., Wang, D.: Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis. In: Proceedings of FMCAD, pp. 33\u201351 (2002)","DOI":"10.1007\/3-540-36126-X_3"},{"key":"8_CR11","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1145\/337180.337234","volume-title":"Proceedings of ICSE","author":"J.C. Corbett","year":"2000","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., P\u0103s\u0103reanu, C.S., Robby, Zheng, H.: Bandera: extracting finite-state models from Java source code. In: Proceedings of ICSE, pp. 439\u2013448. IEEE Computer Society, Los Alamitos (2000)"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, Springer, Heidelberg (1982)"},{"issue":"2","key":"8_CR13","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems\u00a08(2), 244\u2013263 (1986)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample guided abstraction refinement. Computer Aided Verification, 154\u2013169 (2000)","DOI":"10.1007\/10722167_15"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Gupta, A., Kukula, J.H., Shrichman, O.: SAT based abstraction-refinement using ILP and machine learning techniques. In: Proceedings of CAV, pp. 265\u2013279 (2002)","DOI":"10.1007\/3-540-45657-0_20"},{"key":"8_CR16","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking, December 1999. MIT Press, Cambridge (1999)"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-36577-X_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.M. Cobleigh","year":"2003","unstructured":"Cobleigh, J.M., Giannakopoulou, D., P\u0103s\u0103reanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 331\u2013346. Springer, Heidelberg (2003)"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Chaki, S., Ouaknine, J., Yorav, K., Clarke, E.M.: Automated compositional abstraction refinement for concurrent C programs: A two-level approach. In: Proceedings of SoftMC 2003. ENTCS, vol.\u00a089(3) (2003)","DOI":"10.1016\/S1571-0661(05)80004-0"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Dill, D.L.: Trace theory for automatic hierarchical verification of speedindependent circuits. PhD thesis, Carnegie Mellon University, Technical report no. CMU-CS-88-119 (1988)","DOI":"10.7551\/mitpress\/6874.001.0001"},{"issue":"3","key":"8_CR20","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Trans. on Programming Languages and Systems\u00a016(3), 843\u2013871 (1994)","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"8_CR21","volume-title":"Proceedings of FSE","author":"D. Giannakopoulou","year":"2003","unstructured":"Giannakopoulou, D., Magee, J.: Fluent model checking for event-based systems. In: Proceedings of FSE, ACM Press, New York (2003)"},{"key":"8_CR22","first-page":"3","volume-title":"Protocol Specification Testing and Verification","author":"R. Gerth","year":"1995","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Protocol Specification Testing and Verification, Warsaw, Poland, pp. 3\u201318. Chapman & Hall, Sydney (1995)"},{"key":"8_CR23","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":"8_CR24","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of POPL, pp. 58\u201370 (2002)","DOI":"10.1145\/503272.503279"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/3-540-45309-1_11","volume-title":"Programming Languages and Systems","author":"M. Huth","year":"2001","unstructured":"Huth, M., Jagadeesan, R., Schmidt, D.: Modal transition systems: A foundation for three-valued program analysis. In: Sands, D. (ed.) ESOP 2001. LNCS, vol.\u00a02028, p. 155. Springer, Heidelberg (2001)"},{"key":"8_CR26","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)"},{"key":"8_CR27","first-page":"245","volume-title":"Proceedings of ICCAD","author":"T.A. Henzinger","year":"2000","unstructured":"Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Decomposing refinement proofs using assume-guarantee reasoning. In: Proceedings of ICCAD, pp. 245\u2013252. IEEE Computer Society Press, Los Alamitos (2000)"},{"key":"8_CR28","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional mu-calculus. Theoretical Computer Science\u00a027, 333\u2013354 (1983)","journal-title":"Theoretical Computer Science"},{"key":"8_CR29","volume-title":"Computer-aided verification of coordinating processes: the automata-theoretic approach","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer-aided verification of coordinating processes: the automata-theoretic approach. Princeton University Press, Princeton (1994)"},{"key":"8_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/3-540-69108-1_20","volume-title":"Application and Theory of Petri Nets 1998","author":"E. Kindler","year":"1998","unstructured":"Kindler, E., Vesper, T.: ESTL: A temporal logic for events and states. In: Desel, J., Silva, M. (eds.) ICATPN 1998. LNCS, vol.\u00a01420, p. 365. Springer, Heidelberg (1998)"},{"key":"8_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/3-540-45319-9_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y. Lakhnech","year":"2001","unstructured":"Lakhnech, Y., Bensalem, S., Berezin, S., Owre, S.: Incremental verification by abstraction. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 98\u2013112. Springer, Heidelberg (2001)"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Proceedings of POPL (1985)","DOI":"10.1145\/318593.318622"},{"key":"8_CR33","unstructured":"MAGIC website, http:\/\/www.cs.cmu.edu\/~chaki\/magic"},{"key":"8_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/3-540-63166-6_6","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"1997","unstructured":"McMillan, K.L.: A compositional rule for hardware design refinement. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 24\u201335. Springer, Heidelberg (1997)"},{"key":"8_CR35","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall International, London (1989)"},{"key":"8_CR36","doi-asserted-by":"publisher","first-page":"594","DOI":"10.1145\/253228.253489","volume-title":"Proceedings of ICSE","author":"G. Naumovich","year":"1997","unstructured":"Naumovich, G., Clarke, L.A., Osterweil, L.J., Dwyer, M.B.: Verification of concurrent software with FLAVERS. In: Proceedings of ICSE, pp. 594\u2013595. ACM Press, New York (1997)"},{"issue":"7","key":"8_CR37","doi-asserted-by":"publisher","first-page":"761","DOI":"10.1016\/0169-7552(93)90047-8","volume":"25","author":"R. Nicola De","year":"1993","unstructured":"De Nicola, R., Fantechi, A., Gnesi, S., Ristori, G.: An action-based framework for verifying logical and behavioural properties of concurrent systems. Computer Networks and ISDN Systems\u00a025(7), 761\u2013778 (1993)","journal-title":"Computer Networks and ISDN Systems"},{"issue":"2","key":"8_CR38","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1145\/201019.201032","volume":"42","author":"R. Nicola De","year":"1995","unstructured":"De Nicola, R., Vaandrager, F.: Three logics for branching bisimulation. Journal of the ACM (JACM)\u00a042(2), 458\u2013487 (1995)","journal-title":"Journal of the ACM (JACM)"},{"key":"8_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-45319-9_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C.S. P\u0103s\u0103reanu","year":"2001","unstructured":"P\u0103s\u0103reanu, C.S., Dwyer, M.B., Visser, W.: Finding feasible counterexamples when model checking abstracted Java programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 284\u2013298. Springer, Heidelberg (2001)"},{"key":"8_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"510","DOI":"10.1007\/BFb0027047","volume-title":"Current Trends in Concurrency","author":"A. Pnueli","year":"1986","unstructured":"Pnueli, A.: Application of temporal logic to the specification and verification of reactive systems: A survey of current trends. In: Rozenberg, G., de Bakker, J.W., de Roever, W.-P. (eds.) Current Trends in Concurrency. LNCS, vol.\u00a0224, pp. 510\u2013584. Springer, Heidelberg (1986)"},{"key":"8_CR41","doi-asserted-by":"crossref","unstructured":"Quielle, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: proceedings of Fifth Intern. Symposium on Programming, pp. 337\u2013350 (1981)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"8_CR42","volume-title":"The Theory and Practice of Concurrency","author":"A.W. Roscoe","year":"1997","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall International, London (1997)"},{"key":"8_CR43","doi-asserted-by":"crossref","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. Computer-Aided Verification, 248\u2013263 (2000)","DOI":"10.1007\/10722167_21"},{"key":"8_CR44","unstructured":"SLAM website, http:\/\/research.microsoft.com\/slam"},{"key":"8_CR45","unstructured":"OpenSSL, http:\/\/wp.netscape.com\/eng\/ssl3\/ssl-toc.html"},{"issue":"1","key":"8_CR46","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/s10009-002-0077-2","volume":"4","author":"S.D. Stoller","year":"2002","unstructured":"Stoller, S.D.: Model-checking multi-threaded distributed Java programs. International Journal on Software Tools for Technology Transfer\u00a04(1), 71\u201391 (2002)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"8_CR47","unstructured":"Wring website, http:\/\/vlsi.colorado.edu\/~rbloem\/wring.html"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24756-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T15:33:34Z","timestamp":1559316814000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24756-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540213772","9783540247562"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24756-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}