{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,12,24]],"date-time":"2024-12-24T04:40:21Z","timestamp":1735015221632,"version":"3.32.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[1997,7,1]],"date-time":"1997-07-01T00:00:00Z","timestamp":867715200000},"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":[[1997,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We propose a methodology for designing sound and complete proof systems for proving progress properties of parallel programs under various fairness assumptions. Our methodology begins with a branching time temporal logic formula (CTL<jats:sup>*<\/jats:sup>) formula that expresses progress under a fairness assumption. The next step obtains an equivalent fixpoint characterization of this CTL<jats:sup>*<\/jats:sup>formula in the<jats:italic>\u03bc<\/jats:italic>-calculus. The final step uses the fixpoint characterizations to extract proof systems for proving progress under the fairness constraint. The methodology guarantees that the proof rules so obtained are sound and relatively complete in the sense of Cook.<\/jats:p>","DOI":"10.1007\/bf01211296","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T22:18:43Z","timestamp":1109369923000},"page":"359-378","source":"Crossref","is-referenced-by-count":1,"title":["A methodology for designing proof rules for fair parallel programs"],"prefix":"10.1145","volume":"9","author":[{"given":"Charanjit S.","family":"Jutla","sequence":"first","affiliation":[{"name":"IBM Thomas J. Watson Research Center, PO Box 704, 10598, Yorktown Heights, NY, USA"}]},{"given":"Josyula R.","family":"Rao","sequence":"additional","affiliation":[{"name":"IBM Thomas J. Watson Research Center, PO Box 704, 10598, Yorktown Heights, NY, USA"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1145\/6490.6494"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90103-8"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/357146.357150"},{"issue":"4","key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","article-title":"Defining liveness","volume":"24","author":"Alpern B.","year":"1985","journal-title":"Inf. Process. Lett."},{"volume-title":"Parallel Program Design: A Foundation","year":"1988","author":"Mani Chandy K.","key":"e_1_2_1_2_5_2"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1137\/0207005"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.5555\/77545"},{"volume-title":"Lecture Notes in Computer Science 85: Proceedings of the Seventh ICALP","year":"1981","author":"Allen Emerson E.","key":"e_1_2_1_2_9_2"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Allen Emerson E. and Lei D. L.: Modalities for model checking: Branching time strikes back. In Proceedings of the 12th Annual ACM Symposium on the Principles of Programming Languages New Orleans LA January 1985.","DOI":"10.1145\/318593.318620"},{"key":"e_1_2_1_2_11_2","unstructured":"Allen Emerson E. and Lei D. L.: Model-checking in the propositional \u03bc -calculus. In Proceedings of the Fist Annual IEEE Symposium on Logic in Computer Science 1986."},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4886-6","volume-title":"Fairness","author":"Francez N.","year":"1986"},{"key":"e_1_2_1_2_14_2","unstructured":"Grumberg O. Francez N. Makowsky J. A. and De Roever W-P.: A proof rule for the fair termination of guarded commands. In Proceedings of the International Symposium on Algorithmic Languages Amsterdam The Netherlands October 1981."},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Gabbay D. Pnueli A. Shelah S. and Stavi J.: On the temporal analysis of fairness. In Proceedings of the Seventh Annual ACM Symposium on the Principles of Programming Languages Las Vegas Nevada January 1980.","DOI":"10.1145\/567446.567462"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_2_17_2","unstructured":"Hopcroft J. E. and Ullman J. D.: Intoduction to Automata Theory Languages and Computation. Addison-Wesley 1979."},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Jutla C. S. Knapp E. and Rao J. R.: A predicate transformer approach to the semantics of parallel programs. In Proceedings of the Eighth Annual ACM Symposium on the Principles of Distributed Computing pages 249\u2013263 1989.","DOI":"10.1145\/72981.72999"},{"volume-title":"Technical Report TR-92-23","year":"1992","author":"Jutla C. S.","key":"e_1_2_1_2_19_2"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360251"},{"volume-title":"Technical Report TR-88-35","year":"1988","author":"Knapp E.","key":"e_1_2_1_2_21_2"},{"key":"e_1_2_1_2_22_2","first-page":"348","volume-title":"Lecture Notes in Computer Science 140: Proceedings of the Ninth ICALP","author":"Kozen D.","year":"1982"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.229904"},{"volume-title":"Lecture Notes in Computer Science 115: Proceedings of the Eighth ICALP","year":"1981","author":"Lehmann D.","key":"e_1_2_1_2_24_2"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Manna Z. and Pnueli A.: How to cook a temporal proof system for your pet language. In Proceedings of the Tenth Annual ACM Symposium on the Principles of Programming Languages pages 141\u2013154 1983.","DOI":"10.1145\/567067.567082"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(84)90003-0"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Niwinski D.: Fixed points versus infinite generation. In Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science pages 402\u2013409 1988.","DOI":"10.1109\/LICS.1988.5137"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BF00268134","article-title":"An axiomatic proof technique for parallel programs","volume":"5","author":"Owicki S.","year":"1976","journal-title":"Acta Informatica"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357178"},{"key":"e_1_2_1_2_31_2","unstructured":"Pachl J.: Three definitions of leads-to for unity. Notes on UNITY 23-90 1990."},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Park D.: On the semantics of fair parallelism. In D. Biorner editor Lecture Notes in Computer Science 86: Proceedings of the Winter School on Formal Software Specification. Springer-Verlag 1980.","DOI":"10.1007\/3-540-10007-5_47"},{"volume-title":"Proceedings of the Sixth IBM Symposium on Mathematical Foundations of Computer Science (Hakone)","year":"1981","author":"Park D.","key":"e_1_2_1_2_33_2"},{"key":"e_1_2_1_2_34_2","first-page":"278","volume-title":"On the extremely fair treatment of probabilistic algorithms","author":"Pnueli A.","year":"1983"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00265555"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Rao J. R.: Extensions of the UNITY Methodology: Compositionality Fairness And Probability In Parallelism volume 908 of Lecture Notes in Computer Science . Springer-Verlag 1995.","DOI":"10.1007\/3-540-59173-7"},{"key":"e_1_2_1_2_37_2","unstructured":"Rosenstein J. G.: Linear Orderings . Academic Press 1982."},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(89)90004-7"},{"key":"e_1_2_1_2_39_2","unstructured":"Walukiewicz I.: On completeness of the \u03bc -calculus. In Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science 1993."},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/322047.322062"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01211296.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01211296\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01211296","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,24]],"date-time":"2024-12-24T03:52:56Z","timestamp":1735012376000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01211296"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,7]]},"references-count":40,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1997,7]]}},"alternative-id":["10.1007\/BF01211296"],"URL":"https:\/\/doi.org\/10.1007\/bf01211296","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[1997,7]]}}}