{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T04:44:32Z","timestamp":1748493872678},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540304920"},{"type":"electronic","value":"9783540322405"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11589976_5","type":"book-chapter","created":{"date-parts":[[2005,10,26]],"date-time":"2005-10-26T13:38:16Z","timestamp":1130333896000},"page":"53-69","source":"Crossref","is-referenced-by-count":18,"title":["State\/Event Software Verification for Branching-Time Specifications"],"prefix":"10.1007","author":[{"given":"Sagar","family":"Chaki","sequence":"first","affiliation":[]},{"given":"Edmund","family":"Clarke","sequence":"additional","affiliation":[]},{"given":"Orna","family":"Grumberg","sequence":"additional","affiliation":[]},{"given":"Jo\u00ebl","family":"Ouaknine","sequence":"additional","affiliation":[]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[]},{"given":"Tayssir","family":"Touili","sequence":"additional","affiliation":[]},{"given":"Helmut","family":"Veith","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","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":"5_CR2","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1109\/ICSE.2003.1201217","volume-title":"Proceedings of the 25th International Conference on Software Engineering (ICSE)","author":"S. Chaki","year":"2003","unstructured":"Chaki, S., Clarke, E.M., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: Proceedings of the 25th International Conference on Software Engineering (ICSE), pp. 385\u2013395. IEEE Press, Los Alamitos (2003)"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-540-24756-2_8","volume-title":"Integrated Formal Methods","author":"S. Chaki","year":"2004","unstructured":"Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: State\/event-based software model checking. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol.\u00a02999, pp. 128\u2013147. Springer, Heidelberg (2004)"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: Concurrent software verification with states, events, and deadlocks. Formal Aspects of Computing Journal (2005) (to appear)","DOI":"10.1007\/s00165-005-0071-z"},{"key":"5_CR5","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 the Workshop on Software Model Checking (SoftMC). ENTCS, vol.\u00a089(3) (2003)","DOI":"10.1016\/S1571-0661(05)80004-0"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"issue":"5","key":"5_CR7","doi-asserted-by":"publisher","first-page":"606","DOI":"10.1093\/logcom\/2.5.605","volume":"2","author":"E.M. Clarke","year":"1992","unstructured":"Clarke, E.M., Grumberg, O., Kurshan, R.P.: A synthesis of two approaches for verifying finite state concurrent systems. Journal of Logic and Computation\u00a02(5), 606\u2013618 (1992)","journal-title":"Journal of Logic and Computation"},{"issue":"5","key":"5_CR8","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems\u00a016(5), 1512\u20131542 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"5_CR9","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1109\/LICS.2002.1029814","volume-title":"Proceedings of the 17th Symposium on Logic in Computer Science (LICS)","author":"E.M. Clarke","year":"2002","unstructured":"Clarke, E.M., Jha, S., Lu, Y., Veith, H.: Tree-like counterexamples in model checking. In: Proceedings of the 17th Symposium on Logic in Computer Science (LICS), pp. 19\u201329. IEEE Press, Los Alamitos (2002)"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the SIGPLAN Conference on Programming Languages (1977)","DOI":"10.1145\/512950.512973"},{"key":"5_CR11","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/0304-3975(94)90269-0","volume":"126","author":"M. Dam","year":"1994","unstructured":"Dam, M.: CTL* and ECTL* as fragments of the modal \u03bc-calculus. Theoretical Computer Science\u00a0126, 77\u201396 (1994)","journal-title":"Theoretical Computer Science"},{"key":"5_CR12","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":"5_CR13","unstructured":"Haartsen, J.: Bluetooth Baseband Specification, version 1.0"},{"key":"5_CR14","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1145\/503272.503279","volume-title":"Proceedings of the 29th Annual ACM Symposium on Principles of Programming Languages (POPL)","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of the 29th Annual ACM Symposium on Principles of Programming Languages (POPL), pp. 58\u201370. ACM Press, New York (2002)"},{"key":"5_CR15","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":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","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, pp. 137\u2013154. Springer, Heidelberg (2001)"},{"key":"5_CR17","unstructured":"Ivers, J., Sharygina, N.: Overview of ComFoRT: A model checking reasoning framework. CMU\/SEI-2004-TN-018 (2004)"},{"key":"5_CR18","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, pp. 365\u2013383. Springer, Heidelberg (1998)"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"414","DOI":"10.1007\/3-540-52559-9_74","volume-title":"Stepwise Refinement of Distributed Systems","author":"R.P. Kurshan","year":"1990","unstructured":"Kurshan, R.P.: Analysis of discrete event coordination. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1989. LNCS, vol.\u00a0430, pp. 414\u2013453. Springer, Heidelberg (1990)"},{"key":"5_CR20","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":"5_CR21","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":"5_CR22","unstructured":"MAGIC website, \n                    \n                      http:\/\/www.cs.cmu.edu\/~chaki\/magic"},{"key":"5_CR23","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)"},{"key":"5_CR24","doi-asserted-by":"publisher","first-page":"594","DOI":"10.1145\/253228.253489","volume-title":"Proceedings of the 19th International Conference on Software Engineering (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 the 19th International Conference on Software Engineering (ICSE), pp. 594\u2013595. IEEE Press, Los Alamitos (1997)"},{"issue":"2","key":"5_CR25","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\u00a042(2), 458\u2013487 (1995)","journal-title":"Journal of the ACM"},{"key":"5_CR26","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 counter-examples when model checking abstracted Java programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 284\u2013298. Springer, Heidelberg (2001)"},{"key":"5_CR27","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, Englewood Cliffs (1997)"},{"key":"5_CR28","series-title":"Lecture Notes in Computer Science","first-page":"690","volume-title":"Proceedings of REX Workshop","author":"W. Thomas","year":"1988","unstructured":"Thomas, W.: Computation tree logic and regular \u03c9-languages. In: Proceedings of REX Workshop. LNCS, pp. 690\u2013713. Springer, Heidelberg (1988)"},{"key":"5_CR29","series-title":"Lecture Notes in Computer Science","first-page":"501","volume-title":"Proceedings of Logic of Programs","author":"M.Y. Vardi","year":"1983","unstructured":"Vardi, M.Y., Wolper, P.: Yet another process logic. In: Proceedings of Logic of Programs. LNCS, pp. 501\u2013512. Springer, Heidelberg (1983)"},{"issue":"1","key":"5_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation\u00a0115(1), 1\u201337 (1994)","journal-title":"Information and Computation"},{"key":"5_CR31","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"Wolper, P.: Temporal logic can be more expressive. Information and Control\u00a056, 72\u201399 (1983)","journal-title":"Information and Control"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11589976_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,13]],"date-time":"2019-03-13T06:02:22Z","timestamp":1552456942000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11589976_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540304920","9783540322405"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/11589976_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}