{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:49Z","timestamp":1761611149817},"reference-count":22,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2005,5,1]],"date-time":"2005-05-01T00:00:00Z","timestamp":1114905600000},"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,5]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>\n            The paper reports on experiences of mechanizing various proposals for compositional reasoning in concurrent systems. The work uses the UNITY formalism and the Isabelle proof tool. The proposals investigated include existential\/universal properties,\n            <jats:bold>guarantees<\/jats:bold>\n            properties and progress sets. The results also apply to related proposals such as traditional assumption-commitment guarantees and Misra\u2019s closure properties. Findings that have been published in detail elsewhere are summarised and consolidated here. One conclusion is that UNITY and related formalisms leave some important issues implicit, such as their concept of the program state, which means that great care must be exercised when implementing tool support. Another conclusion is that many compositional reasoning methods can be mechanized, provided that the issues mentioned above are correctly addressed.\n          <\/jats:p>","DOI":"10.1007\/s00165-004-0053-6","type":"journal-article","created":{"date-parts":[[2005,2,9]],"date-time":"2005-02-09T09:21:37Z","timestamp":1107940897000},"page":"58-68","source":"Crossref","is-referenced-by-count":3,"title":["Mechanizing compositional reasoning for concurrent systems: some lessons"],"prefix":"10.1145","volume":"17","author":[{"given":"Sidi O.","family":"Ehmety","sequence":"first","affiliation":[{"name":"Facult\u00e9 des Sciences et Techniques, Universit\u00e9 de Nouakchott, BP. 5026, Nouakchott, Mauritania"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[{"name":"Computer Laboratory, University of Cambridge, CB3 0FD, Cambridge, England"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"p_1","first-page":"1","volume-title":"Jimmi S. Pettersson (1994) Program verification using HOL-UNITY. In: Joyce J, Seger C (eds) Higher order logic theorem proving and its applications: HUG '93, LNCS 780","author":"Andersen Flemming"},{"key":"p_2","first-page":"1215","volume-title":"Workshop on formal methods for parallel programming: theory and applications","author":"Charpentier Michel","year":"1999"},{"key":"p_3","first-page":"167","volume-title":"MPC 2000","author":"Charpentier Michel","year":"2000"},{"key":"p_4","volume-title":"An experiment in program composition and proof. Formal methods syst. des. 20(1):7-21","author":"Mani Chandy","year":"2002"},{"issue":"3","key":"p_5","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/s00236-003-0130-y","article-title":"Specification transformers: a predicate transformer approach to composition","volume":"40","author":"Charpentier Michel","year":"2004","journal-title":"Acta Informatica"},{"key":"p_6","volume-title":"Parallel program design: a foundation","author":"Mani Chandy","year":"1988"},{"key":"p_7","volume-title":"Annabelle McIver, Carroll Morgan (eds) Programming methodology","author":"Cohen Ernie","year":"2002"},{"key":"p_9","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate calculus and program semantics","author":"Dijkstra Edsger W.","year":"1990"},{"key":"p_10","series-title":"number EDI-INF-RR-0046 in Informatics Report Series","first-page":"151","volume-title":"Richard J. Boulton, Paul B. Jackson (eds) TPHOLs 2001: supplemental proceedings","author":"Ehmety Sidi O.","year":"2001"},{"key":"p_11","volume-title":"IEEE Workshop on formal methods for parallel programming: theory and applications; text on CD-ROM","author":"Ehmety Sidi O.","year":"2002"},{"key":"p_12","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/BFb0105409","volume-title":"Grundy J, Harrison J (eds) Theorem proving in higher order logics: TPHOLs '96, vol 1125","author":"Heyd Barbara","year":"1996"},{"issue":"3","key":"p_13","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","article-title":"The temporal logic of actions","volume":"16","author":"Lamport Leslie","year":"1994","journal-title":"ACM Trans Programming Languages Syst"},{"key":"p_14","first-page":"402","volume-title":"Willem-Paul de Roever, Hans Langmaack, Amir Pnueli (eds) Compositionality: the significant difference (Proceedings of the COMPOS'97 Symposium), vol 1536","author":"Lamport Leslie","year":"1998"},{"key":"p_16","volume-title":"Yet another encoding of TLA in Isabelle. On the Internet at http:\/\/www.loria.fr\/~merz\/projects\/ isabelle-tla\/doc\/design.ps.gz","author":"Merz Stephan","year":"1999"},{"key":"p_17","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-8528-6","volume-title":"A discipline of multiprogramming","author":"Misra Jayadev","year":"2001"},{"key":"p_18","volume-title":"Programming from specifications","author":"Morgan Carroll","year":"1994","edition":"2"},{"issue":"1","key":"p_19","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1016\/S0304-3975(98)00233-3","article-title":"Composing leads-to properties","volume":"243","author":"Meier David","year":"2000","journal-title":"Theor Comput Sci"},{"key":"p_20","volume-title":"Berlin Heidelberg New York","author":"Nipkow Tobias","year":"2002"},{"issue":"1","key":"p_21","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1145\/343369.343370","article-title":"Mechanizing UNITY in Isabelle","volume":"1","author":"Paulson Lawrence C.","year":"2000","journal-title":"ACM Trans Comput Logic"},{"issue":"5","key":"p_22","doi-asserted-by":"crossref","first-page":"626","DOI":"10.1145\/504709.504711","article-title":"Mechanizing a theory of program composition for UNITY","volume":"25","author":"Paulson Lawrence C.","year":"2001","journal-title":"ACM Trans Programming Languages Syst"},{"issue":"3","key":"p_23","first-page":"291","article-title":"Mechanizing set theory: cardinal arithmetic and the axiom of choice","volume":"17","author":"Paulson Lawrence C.","year":"1990","journal-title":"J Automated Reasoning"},{"issue":"2","key":"p_24","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/BF01898402","article-title":"Eliminating the substitution axiom from UNITY logic","volume":"3","author":"Sanders Beverly","year":"1991","journal-title":"Formal Aspects Comput"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-004-0053-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-004-0053-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-004-0053-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:43:53Z","timestamp":1641483833000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-004-0053-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,5]]},"references-count":22,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2005,5]]}},"alternative-id":["10.1007\/s00165-004-0053-6"],"URL":"https:\/\/doi.org\/10.1007\/s00165-004-0053-6","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,5]]}}}