{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:31:34Z","timestamp":1773192694459,"version":"3.50.1"},"reference-count":62,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T00:00:00Z","timestamp":1133395200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2005,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a framework for model checking concurrent software systems which incorporates both states and events. Contrary to other state\/event approaches, our work also integrates two powerful verification techniques, counterexample-guided abstraction refinement and compositional reasoning. Our specification language is a state\/event extension of linear temporal logic, and allows us to express many properties of software in a concise and intuitive manner. We show how standard automata-theoretic LTL model checking algorithms can be ported to our framework at no extra cost, enabling us to directly benefit from the large body of research on efficient LTL verification.<\/jats:p><jats:p>We also present an algorithm to detect deadlocks in concurrent message-passing programs. Deadlock- freedom is not only an important and desirable property in its own right, but is also a prerequisite for the soundness of our model checking algorithm. Even though deadlock is inherently non-compositional and is not preserved by classical abstractions, our iterative algorithm employs both (non-standard) abstractions and compositional reasoning to alleviate the state-space explosion problem. The resulting framework differs in key respects from other instances of the counterexample-guided abstraction refinement paradigm found in the literature.<\/jats:p><jats:p>We have implemented this work in the magic verification tool for concurrent C programs and performed tests on a broad set of benchmarks. Our experiments show that this new approach not only eases the writing of specifications, but also yields important gains both in space and in time during verification. In certain cases, we even encountered specifications that could not be verified using traditional pure event-based or state-based approaches, but became tractable within our state\/event framework. We also recorded substantial reductions in time and memory consumption when performing deadlock-freedom checks with our new abstractions. Finally, we report two bugs (including a deadlock) in the source code of Micro-C\/OS versions 2.0 and 2.7, which we discovered during our experiments.<\/jats:p>","DOI":"10.1007\/s00165-005-0071-z","type":"journal-article","created":{"date-parts":[[2005,9,21]],"date-time":"2005-09-21T07:54:15Z","timestamp":1127289255000},"page":"461-483","source":"Crossref","is-referenced-by-count":51,"title":["Concurrent software verification with states, events, and deadlocks"],"prefix":"10.1145","volume":"17","author":[{"given":"Sagar","family":"Chaki","sequence":"first","affiliation":[{"name":"Software Engineering Institute, Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edmund","family":"Clarke","sequence":"additional","affiliation":[{"name":"Computer Science Department, Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jo\u00ebl","family":"Ouaknine","sequence":"additional","affiliation":[{"name":"Oxford University Computing Laboratory, Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[{"name":"Software Engineering Institute, Carnegie Mellon University, Pittsburgh, USA"},{"name":"Computer Science Department, Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nishant","family":"Sinha","sequence":"additional","affiliation":[{"name":"Computer Science Department, Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"p_1","unstructured":"[ABB] ABB website. http:\/\/www.abb.com"},{"key":"p_2","first-page":"191","volume-title":"Proceedings of the 12th annual ACM symposium on principles of programming languages (POPL), ACM Press","author":"Anantharaman TS","year":"1985"},{"key":"p_3","first-page":"484","volume-title":"Proceedings of the 16th international conference on computer aided verification (CAV). vol 3114","author":"Andrews T","year":"2004"},{"key":"p_4","unstructured":"[BLAST] BLAST website. http:\/\/www-cad.eecs.berkeley.edu\/\u223crupak\/blast"},{"key":"p_5","first-page":"319","volume-title":"Proceedings of the 10th international conference on computer aided verification (CAV), vol 1427","author":"Bensalem S","year":"1998"},{"key":"p_6","first-page":"203","volume-title":"Proceedings of the SIGPLAN conference on programming language design and implementation (PLDI), ACM Press","author":"Ball T","year":"2001"},{"key":"p_7","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/BF01784721","article-title":"Deadlock analysis of networks of communicating processes","volume":"4","author":"Brookes SD","year":"1991","journal-title":"Distrib Comput"},{"key":"p_8","first-page":"103","volume-title":"Proceedings of the 8th international SPIN workshop, vol","author":"Ball T","year":"2001"},{"key":"p_10","first-page":"293","volume-title":"Modal logics and mu-calculi: an introduction. Handbook of Process Algebra","author":"Bradfield J","year":"2001"},{"key":"p_12","volume-title":"Proceedings of the SIGPLAN conference on programming languages","author":"Cousot P","year":"1977"},{"key":"p_13","first-page":"385","volume-title":"Proceedings of the 25th international conference on software engineering (ICSE), IEEE Press","author":"Chaki S","year":"2003"},{"key":"p_14","volume-title":"Proceedings of the 5th international conference on integrated formal methods (IFM). Lecture notes in computer science. Springer, Berlin Heidelberg New York","author":"Chaki S","year":"2005"},{"key":"p_15","first-page":"33","volume-title":"Proceedings of 4th international conference on formal methods in computer-aided design (FMCAD) vol 2517","author":"Chauhan P","year":"2002"},{"key":"p_16","first-page":"128","volume-title":"Proceedings of the 4th international conference on integrated formal methods (IFM) vol 2999","author":"Chaki S","year":"2004"},{"key":"p_17","volume-title":"Proceedings of the 2nd ACM-IEEE international conference on formal methods and models for codesign (MEMOCODE). IEEE Press","author":"Chaki S","year":"2004"},{"key":"p_18","first-page":"439","volume-title":"Proceedings of the 22nd international conference on software engineering (ICSE), ACM Press","author":"Corbett JC","year":"2000"},{"key":"p_19","first-page":"52","volume-title":"Proceedings of the workshop on logic of programs. vol 131","author":"Clarke EM","year":"1981"},{"issue":"2","key":"p_20","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","article-title":"Automatic verification of finite-state concurrent systems using temporal logic specifications","volume":"8","author":"Clarke EM","year":"1986","journal-title":"ACM Trans Progr Lang Syst"},{"key":"p_21","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Proceedings of the 12th international conference on computer aided verification (CAV). vol","author":"Clarke EM","year":"2000"},{"key":"p_22","first-page":"265","volume-title":"Proceedings of the 14th international conference on computer aided verification (CAV). vol 2404","author":"Clarke EM","year":"2002"},{"issue":"5","key":"p_23","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","article-title":"Model checking and abstraction","volume":"16","author":"Clarke EM","year":"1994","journal-title":"ACM Trans Progr Lang Syst"},{"key":"p_24","volume-title":"Model checking","author":"Clarke EM","year":"1999"},{"key":"p_25","first-page":"331","volume-title":"Proceedings of the 9th international conference on tools and algorithms for the construction and analysis of systems (TACAS). vol 2619","author":"Cobleigh JM","year":"2003"},{"issue":"3","key":"p_26","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1109\/32.489078","article-title":"Evaluating deadlock detection methods for concurrent software","volume":"22","author":"Cor JC","year":"1996","journal-title":"Softw Eng"},{"key":"p_27","volume-title":"Proceedings of the workshop on software model checking (SoftMC). ENTCS 89(3)","author":"Chaki S","year":"2003"},{"issue":"7","key":"p_29","doi-asserted-by":"crossref","first-page":"577","DOI":"10.1002\/(SICI)1097-024X(199906)29:7<577::AID-SPE246>3.0.CO;2-V","article-title":"A deadlock detection tool for concurrent Java programs","volume":"29","author":"Demartini C","year":"1999","journal-title":"Softw Pract Exp"},{"key":"p_30","first-page":"242","volume-title":"Proceedings of the 16th international conference on computer aided verification (CAV). vol 3114","author":"Fournet C","year":"2004"},{"key":"p_31","unstructured":"[FSEL] Formal Systems (Europe) Ltd. website. http:\/\/www.fsel.com"},{"issue":"3","key":"p_32","doi-asserted-by":"crossref","first-page":"843","DOI":"10.1145\/177492.177725","article-title":"Model checking and modular verification","volume":"16","author":"Grumberg O","year":"1994","journal-title":"ACM Trans Progr Lang Syst"},{"key":"p_33","first-page":"257","volume-title":"Proceedings of the 11th ACM SIGSOFT symposium on foundations of software engineering (FSE), ACM Press","author":"Giannakopoulou D","year":"2003"},{"key":"p_34","first-page":"3","volume-title":"Proceedings of the Fifteenth IFIP WG6.1 international symposium on protocol specification, testing and verification, Chapman & Hall","author":"Gerth R","year":"1995"},{"key":"p_35","first-page":"72","volume-title":"Proceedings of the 9th international conference on computer aided verification (CAV). vol 1254","author":"Graf S","year":"1997"},{"key":"p_36","doi-asserted-by":"crossref","first-page":"262","DOI":"10.1007\/978-3-540-45069-6_27","volume-title":"Proceedings of the 15th international conference on computer aided verification (CAV)","volume":"2725","author":"Henzinger TA","year":"2003"},{"key":"p_37","first-page":"58","volume-title":"Proceedings of the 29th annual ACM symposium on principles of programming languages (POPL), ACM Press","author":"Henzinger TA","year":"2002"},{"key":"p_38","first-page":"137","volume-title":"Proceedings of the 10th european symposium on programming (ESOP). vol","author":"Huth M","year":"2001"},{"key":"p_39","volume-title":"Communicating sequential processes","author":"Hoa CAR","year":"1985"},{"key":"p_40","first-page":"245","volume-title":"Proceedings of the international conference on computer-aided design (ICCAD), IEEE Computer Society Press","author":"Henzinger TA","year":"2000"},{"key":"p_41","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","article-title":"Results on the propositional mu-calculus","volume":"27","author":"Koz D","year":"1983","journal-title":"Theoretical Comput Sci"},{"key":"p_42","first-page":"414","volume-title":"Proceedings of the REX workshop. vol 430","author":"Kur RP","year":"1989"},{"key":"p_43","volume-title":"Computer-aided verification of coordinating processes: the automata-theoretic approach","author":"Kur RP","year":"1994"},{"key":"p_44","first-page":"365","volume-title":"Proceedings of the 19th international conference on the application and theory of petri nets (ICATPN). vol 1420","author":"Kindler E","year":"1998"},{"key":"p_45","first-page":"98","volume-title":"Proceedings of the 7th international conference on tools and algorithms for the construction and analysis of systems (TACAS). vol","author":"Lakhnech Y","year":"2001"},{"key":"p_46","first-page":"97","volume-title":"Proceedings of the 12th annual ACM symposium on principles of programming languages (POPL), ACM Press","author":"Lichtenstein O","year":"1985"},{"key":"p_47","unstructured":"[LTSA] LTSA website. http:\/\/www-dse.doc.ic.ac.uk\/concurrency\/ltsa\/LTSA.html"},{"key":"p_48","unstructured":"[MAGIC] MAGIC website. http:\/\/www.cs.cmu.edu\/\u223cchaki\/magic"},{"key":"p_49","first-page":"24","volume-title":"Proceedings of the 9th international conference on computer aided verification (CAV). vol 1254","author":"Mc KL","year":"1997"},{"key":"p_50","volume-title":"Proceedings of Comm. Process Architectures","author":"Martin JMR","year":"2000"},{"key":"p_51","volume-title":"Communication and Concurrency","author":"Mil R","year":"1989"},{"key":"p_52","volume-title":"Proceedings of the 20th world occam and transputer user group technical meeting","author":"Martin JMR","year":"1997"},{"key":"p_53","doi-asserted-by":"crossref","first-page":"594","DOI":"10.1145\/253228.253489","volume-title":"Proceedings of the 19th international conference on software engineering (ICSE), ACM Press","author":"Naumovich G","year":"1997"},{"issue":"7","key":"p_54","doi-asserted-by":"crossref","first-page":"761","DOI":"10.1016\/0169-7552(93)90047-8","article-title":"An action-based framework for verifying logical and behavioural properties of concurrent systems","volume":"25","author":"De Nicola R","year":"1993","journal-title":"Comput Netw ISDN Syst"},{"issue":"2","key":"p_55","doi-asserted-by":"crossref","first-page":"458","DOI":"10.1145\/201019.201032","article-title":"Three logics for branching bisimulation","volume":"42","author":"De Nicola R","year":"1995","journal-title":"J ACM"},{"key":"p_56","first-page":"284","volume-title":"Proceedings of the 7th international conference on tools and algorithms for the construction and analysis of systems (TACAS). vol","author":"Psreanu CS","year":"2001"},{"key":"p_57","first-page":"510","volume-title":"Lecture notes in computer science","author":"Pnu A","year":"1986"},{"key":"p_58","first-page":"337","volume-title":"Selected papers from the first and the second european workshop on application and theory of petri nets","author":"Quielle JP","year":"1981"},{"issue":"3","key":"p_59","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1016\/0890-5401(87)90004-6","article-title":"The pursuit of deadlock freedom","volume":"75","author":"Roscoe AW","year":"1987","journal-title":"Information Comput"},{"key":"p_60","volume-title":"The theory and practice of concurrency","author":"Ros AW","year":"1997"},{"key":"p_61","doi-asserted-by":"crossref","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"Proceedings of the 12th international conference on computer aided verification (CAV). vol","author":"Somenzi F","year":"2000"},{"key":"p_62","unstructured":"[SLAM] SLAM website. http:\/\/research.microsoft.com\/slam"},{"key":"p_63","unstructured":"[SSL] OpenSSL. http:\/\/wp.netscape.com\/eng\/ssl3\/ssl-toc.html"},{"issue":"1","key":"p_64","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1007\/s10009-002-0077-2","article-title":"Model-checking multi-threaded distributed Java programs","volume":"4","author":"Sto SD","year":"2002","journal-title":"Int J Softw Tools Technol Transf"},{"key":"p_65","unstructured":"[WRING] Wring website. http:\/\/vlsi.colorado.edu\/\u223crbloem\/wring.html"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-005-0071-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-005-0071-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-005-0071-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,4]],"date-time":"2025-01-04T12:30:12Z","timestamp":1735993812000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-005-0071-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,12]]},"references-count":62,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2005,12]]}},"alternative-id":["10.1007\/s00165-005-0071-z"],"URL":"https:\/\/doi.org\/10.1007\/s00165-005-0071-z","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,12]]}}}