{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T11:22:23Z","timestamp":1742383343737,"version":"3.35.0"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540851134"},{"type":"electronic","value":"9783540851141"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-85114-1_14","type":"book-chapter","created":{"date-parts":[[2008,8,13]],"date-time":"2008-08-13T03:22:48Z","timestamp":1218597768000},"page":"176-195","source":"Crossref","is-referenced-by-count":5,"title":["Dependency Analysis for Control Flow Cycles in Reactive Communicating Processes"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Leue","sequence":"first","affiliation":[]},{"given":"Alin","family":"\u015etef\u0103nescu","sequence":"additional","affiliation":[]},{"given":"Wei","family":"Wei","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/978-3-540-30579-8_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: Termination of polynomial programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 113\u2013129. Springer, Heidelberg (2005)"},{"issue":"2","key":"14_CR2","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1145\/322374.322380","volume":"30","author":"D. Brand","year":"1983","unstructured":"Brand, D., Zafiropulo, P.: On communicating finite-state machines. Journal of the ACM\u00a030(2), 323\u2013342 (1983)","journal-title":"Journal of the ACM"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/11547662_8","volume-title":"Static Analysis","author":"B. Cook","year":"2005","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Abstraction refinement for termination. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 87\u2013101. Springer, Heidelberg (2005)"},{"issue":"1","key":"14_CR4","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/BF01384316","volume":"6","author":"J.C. Corbett","year":"1995","unstructured":"Corbett, J.C., Avrunin, G.S.: Using integer programming to verify general safety and liveness properties. Formal Methods in System Design\u00a06(1), 97\u2013123 (1995)","journal-title":"Formal Methods in System Design"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/b105073","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Cousot","year":"2005","unstructured":"Cousot, P.: Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 1\u201324. Springer, Heidelberg (2005)"},{"issue":"4","key":"14_CR6","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-002-0092-3","volume":"4","author":"Y. Dong","year":"2003","unstructured":"Dong, Y., Du, X., Holzmann, G.J., Smolka, S.A.: Fighting livelock in the GNU i-Protocol: a case study in explicit-state model checking. Int. Journal on Software Tools for Technology Transfer (STTT)\u00a04(4), 505\u2013528 (2003)","journal-title":"Int. Journal on Software Tools for Technology Transfer (STTT)"},{"key":"14_CR7","unstructured":"Dwyer, M.B., Hatcliff, J.: Slicing software for model construction. In: Proc. of PEPM 1999, pp. 105\u2013118 (1999)"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Graham, T.C.N., Urnes, T., Nejabi, R.: Efficient distributed implementation of semi-replicated synchronous groupware. In: ACM Symposium on User Interface Software and Technology, pp. 1\u201310 (1996)","DOI":"10.1145\/237091.237092"},{"key":"14_CR9","volume-title":"The SPIN model checker: Primer and reference manual","author":"G.J. Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The SPIN model checker: Primer and reference manual. Addison Wesley, Reading (2004)"},{"issue":"4","key":"14_CR10","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/s100090050045","volume":"2","author":"M. Kamel","year":"2000","unstructured":"Kamel, M., Leue, S.: Formalization and validation of the general Inter-ORB protocol (GIOP) using PROMELA and SPIN. Int. Journal on Software Tools for Technology Transfer (STTT)\u00a02(4), 394\u2013409 (2000)","journal-title":"Int. Journal on Software Tools for Technology Transfer (STTT)"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Kumar, R., Tullsen, D.: Compiling for instruction cache performance on a multithreaded architecture. In: Proc. of MICRO 2002, pp. 419\u2013429. ACM\/IEEE (2002)","DOI":"10.1109\/MICRO.2002.1176269"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/11817949_6","volume-title":"CONCUR 2006 \u2013 Concurrency Theory","author":"S. Leue","year":"2006","unstructured":"Leue, S., \u015etef\u0103nescu, A., Wei, W.: A livelock freedom analysis for infinite state asynchronous reactive systems. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol.\u00a04137, pp. 79\u201394. Springer, Heidelberg (2006)"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1007\/978-3-540-24730-2_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Leue","year":"2004","unstructured":"Leue, S., Mayr, R., Wei, W.: A scalable incomplete test for the boundedness of UML RT models. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 327\u2013341. Springer, Heidelberg (2004)"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1007\/11537328_8","volume-title":"Model Checking Software","author":"S. Leue","year":"2005","unstructured":"Leue, S., Wei, W.: Counterexample-based refinement for a boundedness test for CFSM languages. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol.\u00a03639, pp. 58\u201374. Springer, Heidelberg (2005)"},{"key":"14_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems \u2013 Specification","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems \u2013 Specification. Springer, Heidelberg (1992)"},{"key":"14_CR16","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1145\/155332.155346","volume-title":"PPOPP 1993","author":"S.P. Masticola","year":"1993","unstructured":"Masticola, S.P., Ryder, B.G.: Non-concurrency analysis. In: PPOPP 1993, pp. 129\u2013138. ACM Press, New York (1993)"},{"key":"14_CR17","unstructured":"Merino, P., Troya, J.M.: Modeling and verification of the ITU-T multipoint communication service with SPIN. In: Proc. of SPIN 1996 (1996)"},{"issue":"4","key":"14_CR18","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/s100090050041","volume":"2","author":"L.I. Millett","year":"2000","unstructured":"Millett, L.I., Teitelbaum, T.: Issues in slicing Promela and its applications to model checking, protocol understanding, and simulation. STTT\u00a02(4), 343\u2013349 (2000)","journal-title":"STTT"},{"key":"14_CR19","first-page":"24","volume-title":"SIGSOFT FSE 1998","author":"G. Naumovich","year":"1998","unstructured":"Naumovich, G., Avrunin, G.S.: A conservative data flow algorithm for detecting all pairs of statements that may happen in parallel. In: SIGSOFT FSE 1998, pp. 24\u201334. ACM Press, New York (1998)"},{"key":"14_CR20","volume-title":"Principles of program analysis","author":"F. Nielson","year":"2005","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of program analysis, 2nd edn. Springer, Heidelberg (2005)","edition":"2"},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-540-73370-6_17","volume-title":"Model Checking Software","author":"R. Pel\u00e1nek","year":"2007","unstructured":"Pel\u00e1nek, R.: BEEM: Benchmarks for explicit model checkers. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 263\u2013267. Springer, Heidelberg (2007)"},{"key":"14_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 239\u2013251. Springer, Heidelberg (2004)"},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Ranganath, V.P., Amtoft, T., Banerjee, A., Hatcliff, J., Dwyer, M.B.: A new foundation for control dependence and slicing for modern program structures. ACM Trans. Program. Lang. Syst.\u00a029(5) (2007)","DOI":"10.1145\/1275497.1275502"},{"issue":"2","key":"14_CR24","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1109\/32.988494","volume":"28","author":"S.F. Siegel","year":"2002","unstructured":"Siegel, S.F., Avrunin, G.S.: Improving the precision of INCA by eliminating solutions with spurious cycles. IEEE Trans. Software Eng.\u00a028(2), 115\u2013128 (2002)","journal-title":"IEEE Trans. Software Eng."},{"issue":"3","key":"14_CR25","first-page":"121","volume":"3","author":"F. Tip","year":"1995","unstructured":"Tip, F.: A survey of program slicing techniques. Journal of Programming Languages\u00a03(3), 121\u2013189 (1995)","journal-title":"Journal of Programming Languages"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-85114-1_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,31]],"date-time":"2025-01-31T12:37:54Z","timestamp":1738327074000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-85114-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540851134","9783540851141"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-85114-1_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}