{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T14:17:02Z","timestamp":1742393822662},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540732297"},{"type":"electronic","value":"9783540732303"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-73230-3_6","type":"book-chapter","created":{"date-parts":[[2007,6,29]],"date-time":"2007-06-29T17:04:42Z","timestamp":1183136682000},"page":"69-83","source":"Crossref","is-referenced-by-count":4,"title":["Static Detection of Livelocks in Ada Multitasking Programs"],"prefix":"10.1007","author":[{"given":"Johann","family":"Blieberger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"Burgstaller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Mittermayr","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/11817949_7","volume-title":"CONCUR 2006 \u2013 Concurrency Theory","author":"P.A. Abdulla","year":"2006","unstructured":"Abdulla, P.A., Jonsson, B., Rezine, A., Saksena, M.: Proving Liveness by Backwards Reachability. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol.\u00a04137, pp. 95\u2013109. Springer, Heidelberg (2006)"},{"key":"6_CR2","unstructured":"Burgstaller, B.: Symbolic Evaluation of Imperative Programming Languages. Technical Report 183\/1-138, Department of Automation, Vienna University of Technology (June 2005), Available at http:\/\/www.auto.tuwien.ac.at\/~bburg\/reports.html"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/11767077_4","volume-title":"Reliable Software Technologies \u2013 Ada-Europe 2006","author":"B. Burgstaller","year":"2006","unstructured":"Burgstaller, B., Blieberger, J., Mittermayr, R.: Static detection of access anomalies in Ada95. In: Pinho, L.M., Gonz\u00e1lez Harbour, M. (eds.) Ada-Europe 2006. LNCS, vol.\u00a04006, pp. 40\u201355. Springer, Heidelberg (2006)"},{"key":"6_CR4","unstructured":"Burgstaller, B., Scholz, B., Blieberger, J.: Tour de Spec \u2014 A Collection of Spec95 Program Paths and Associated Costs for Symbolic Evaluation. Technical Report 183\/1-137, Department of Automation, Vienna University of Technology (June 2004) Available at http:\/\/www.auto.tuwien.ac.at\/~bburg\/reports.html"},{"key":"6_CR5","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/11860990_12","volume-title":"Proceedings of the 7th Joint Modular Languages Conference","author":"B. Burgstaller","year":"2006","unstructured":"Burgstaller, B., Scholz, B., Blieberger, J.: Symbolic Analysis of Imperative Programming Languages. In: Proceedings of the 7th Joint Modular Languages Conference. LNCS, pp. 172\u2013194. Springer, Heidelberg (2006)"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/3-540-49253-4_11","volume-title":"Algebraic Methodology and Software Technology","author":"B. Buth","year":"1998","unstructured":"Buth, B., Peleska, J., Shi, H.: Combining Methods for the Livelock Analysis of a Fault-Tolerant System. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol.\u00a01548, pp. 124\u2013139. Springer, Heidelberg (1998)"},{"key":"6_CR7","unstructured":"Buth, B., Peleska, J., Shi, H.: Deadlock- und Livelock-Analyse f\u00fcr die Internationale Raumstation ISS (August 2006)"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Cassidy, T., Cordy, J., Dean, T., Dingel, J.: Source Transformation for Concurrency Analysis. In: Proc. LDTA 2005, ACM 5th International Workshop on Language Descriptions, Tools and Applications, Edinburgh, Scotland, April 2005, pp. 26\u201343 (2005)","DOI":"10.1016\/j.entcs.2005.05.012"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/BFb0018493","volume-title":"Ada: The Choice for \u201992","author":"J. Cheng","year":"1991","unstructured":"Cheng, J., Ushijima, K.: Analyzing Ada Tasking Deadlocks and Livelocks Using Extended Petri Nets. In: Christodoulakis, D.N. (ed.) Ada: The Choice for \u201992. LNCS, vol.\u00a0499, pp. 125\u2013146. Springer, Heidelberg (1991)"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., P\u0103s\u0103reanu, C.S.: Bandera: Extracting Finite-state Models from Java Source Code. In: Proceedings of the 22nd International Conference on Software Engineering, Limerick, Ireland, June 2000, pp. 439\u2013448 (2000)","DOI":"10.1145\/337180.337234"},{"key":"6_CR11","volume-title":"Introduction to Algorithms","author":"T.H. Cormen","year":"1989","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. MIT Press, Cambridge, MA (1989)"},{"issue":"2","key":"6_CR12","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s10703-005-1489-x","volume":"26","author":"P. Godefroid","year":"2005","unstructured":"Godefroid, P.: Software Model Checking: The VeriSoft Approach. Form. Methods Syst. Des.\u00a026(2), 77\u2013101 (2005)","journal-title":"Form. Methods Syst. Des."},{"key":"6_CR13","unstructured":"Hilderink, G.H., Broenink, J.F., Bakkers, A.W.P.: Communicating Threads for Java. In: Cook, B.M. (ed.) Proceedings of WoTUG-22: Architectures, Languages and Techniques for Concurrent Systems, Keele, UK, March 1999, pp. 243\u2013261 (1999)"},{"key":"6_CR14","unstructured":"Ho, A., Smith, S., Hand, S.: On deadlock, livelock, and forward progress. Technical Report UCAM-CL-TR-633, University of Cambridge, Computer Laboratory (May 2005)"},{"key":"6_CR15","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, London (1985)"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","volume-title":"CONCUR \u201995 Concurrency Theory","author":"G.J. Holzmann","year":"1995","unstructured":"Holzmann, G.J.: Proving Properties of Concurrent Systems with Spin (invited tutorial). In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol.\u00a0962, Springer, Heidelberg (1995)"},{"key":"6_CR17","volume-title":"The Spin Model Checker \u2013 Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The Spin Model Checker \u2013 Primer and Reference Manual. Addison-Wesley, Reading, Massachusetts (2003)"},{"key":"6_CR18","unstructured":"Ouaknine, J.: SLAP tool (Version 0.1): A Static Livelock Analyzer for CSP Processes, http:\/\/web.comlab.ox.ac.uk\/oucl\/work\/joel.ouaknine\/software\/slap.html"},{"issue":"8","key":"6_CR19","doi-asserted-by":"publisher","first-page":"829","DOI":"10.1109\/32.57622","volume":"16","author":"G.M. Karam","year":"1990","unstructured":"Karam, G.M., Buhr, R.J.A.: Starvation and Critical Race Analyzers for Ada. IEEE Transactions on Software Engineering\u00a016(8), 829\u2013843 (1990)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"6_CR20","unstructured":"Kwong, Y.S.: On reductions and livelocks in asynchronous parallel computation. PhD thesis (1978)"},{"key":"6_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/BFb0022469","volume-title":"Proceedings of the International Sympoisum on Semantics of Concurrent Computation","author":"Y.S. Kwong","year":"1979","unstructured":"Kwong, Y.S.: On the Absence of Livelocks in Parallel Programs. In: Kahn, G. (ed.) Semantics of Concurrent Computation. LNCS, vol.\u00a070, pp. 172\u2013190. Springer, Heidelberg (1979)"},{"key":"6_CR22","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":"6_CR23","unstructured":"F.\u00a0S.\u00a0E. Ltd. Failures-Divergence Refinement, FDR 2 User Manual (2005), www.fsel.com"},{"key":"6_CR24","unstructured":"Martin, J.M.R., Huddart, Y.: Parallel Algorithms for Deadlock and Livelock Analysis of Concurrent Systems. In: Welch, P.H., Bakkers, A.W.P. (eds.) Communicating Process Architectures, September 2000, pp. 1\u201314 (2000)"},{"key":"6_CR25","first-page":"1","volume-title":"Proc. WoTUG20: Parallel Programming and Java","author":"J.M.R. Martin","year":"1997","unstructured":"Martin, J.M.R., Jassim, S.A.: A Tool for Proving Deadlock Freedom. In: Proc. WoTUG20: Parallel Programming and Java, April 1997, pp. 1\u201316. IOS Press, Amsterdam (1997)"},{"issue":"3","key":"6_CR26","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/263326.263335","volume":"15","author":"J.C. Mogul","year":"1997","unstructured":"Mogul, J.C., Ramakrishnan, K.K.: Eliminating Receive Livelock in an Interrupt-Driven Kernel. ACM Transactions on Computer Systems\u00a015(3), 217\u2013252 (1997)","journal-title":"ACM Transactions on Computer Systems"},{"issue":"3","key":"6_CR27","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1145\/357172.357178","volume":"4","author":"S. Owicki","year":"1982","unstructured":"Owicki, S., Lamport, L.: Proving Liveness Properties of Concurrent Programs. ACM Trans. Program. Lang. Syst.\u00a04(3), 455\u2013495 (1982)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"6_CR28","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":"6_CR29","volume-title":"Discrete Mathematics and its Applications","author":"K.H. Rosen","year":"1995","unstructured":"Rosen, K.H.: Discrete Mathematics and its Applications, 3rd edn. McGraw-Hill, New York (1995)","edition":"3"},{"key":"6_CR30","series-title":"LNCS","volume-title":"Proc. ETAPS 2007","author":"B. Scholz","year":"2007","unstructured":"Scholz, B., Blieberger, J.: A New Elimination-Based Data Flow Analysis Framework using Annotated Decomposition Trees. In: Proc. ETAPS 2007, Braga, Portugal, March 2007. LNCS, Springer, Heidelberg (2007)"},{"key":"6_CR31","unstructured":"Shi, H.: Java2CSP: A System for Verifying Concurrent Java Programs. In: Schellhorn, G., Reif, W. (eds) FM-TOOLS 2000, number 2000-07 in Ulmer Informatik-Berichte, pp. 111\u2013115 (2000)"},{"key":"6_CR32","volume-title":"Operating Systems: Internals and Design Principles","author":"W. Stallings","year":"2001","unstructured":"Stallings, W.: Operating Systems: Internals and Design Principles. Prentice Hall, Englewood Cliffs, NJ (2001)"},{"key":"6_CR33","doi-asserted-by":"crossref","unstructured":"Tai, K.-C.: Definitions and Detection of Deadlock, Livelock, and Starvation in Concurrent Programs. In: ICPP, August 1994, vol.\u00a02, pp. 69\u201372 (1994)","DOI":"10.1109\/ICPP.1994.84"},{"issue":"3","key":"6_CR34","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1145\/322261.322272","volume":"28","author":"R.E. Tarjan","year":"1981","unstructured":"Tarjan, R.E.: A unified approach to path problems. J. ACM\u00a028(3), 577\u2013593 (1981)","journal-title":"J. ACM"},{"issue":"3","key":"6_CR35","doi-asserted-by":"publisher","first-page":"594","DOI":"10.1145\/322261.322273","volume":"28","author":"R.E. Tarjan","year":"1981","unstructured":"Tarjan, R.E.: Fast algorithms for solving path problems. J. ACM\u00a028(3), 594\u2013614 (1981)","journal-title":"J. ACM"},{"key":"6_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/11817949_9","volume-title":"CONCUR 2006 \u2013 Concurrency Theory","author":"R.J. Glabbeek van","year":"2006","unstructured":"van Glabbeek, R.J., Voorhoeve, M.: Liveness, Fairness and Impossible Futures. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol.\u00a04137, pp. 126\u2013141. Springer, Heidelberg (2006)"},{"key":"6_CR37","volume-title":"ASE","author":"W. Visser","year":"2000","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S.: Model Checking Programs. In: ASE. IEEE International Conference on Automated Software Engineering, Grenoble, France, September 2000, IEEE Computer Society Press, Los Alamitos (2000)"},{"key":"6_CR38","volume-title":"PDSE \u201900","author":"P.H. Welch","year":"2000","unstructured":"Welch, P.H., Martin, J.M.R.: A CSP Model for Java Multithreading. In: PDSE \u201900. Proceedings of the International Symposium on Software Engineering for Parallel and Distributed Systems, Washington, DC, vol.\u00a0114, IEEE Computer Society Press, Los Alamitos (2000)"}],"container-title":["Lecture Notes in Computer Science","Reliable Software Technologies \u2013 Ada Europe 2007"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73230-3_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:12:42Z","timestamp":1605762762000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73230-3_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540732297","9783540732303"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73230-3_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}