{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:58:12Z","timestamp":1750309092986,"version":"3.41.0"},"reference-count":7,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[1982,4,1]],"date-time":"1982-04-01T00:00:00Z","timestamp":386467200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGOPS Oper. Syst. Rev."],"published-print":{"date-parts":[[1982,4]]},"abstract":"<jats:p>An inadequacy is pointed out in the original proof rules for monitors and in later extended rules. This inadequacy gives rise to an anomaly in proving the invariant for a monitor simulating a counting semaphore. New proof rules are proposed and used to give a sound proof of the invariant.<\/jats:p>","DOI":"10.1145\/1041474.1041476","type":"journal-article","created":{"date-parts":[[2005,1,26]],"date-time":"2005-01-26T16:49:14Z","timestamp":1106758154000},"page":"18-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["On proof rules for monitors"],"prefix":"10.1145","volume":"16","author":[{"given":"J. M.","family":"Adams","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A. P.","family":"Black","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[1982,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/357103.357110"},{"key":"e_1_2_1_2_1","unstructured":"Brinch-Hansen P. Operating System Principles. Prentice-Hall Englewood Cliffs N.J. 1973.   Brinch-Hansen P. Operating System Principles. Prentice-Hall Englewood Cliffs N.J. 1973."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00571463"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/361268.361277"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/355620.361161"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360079"},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Turski W. M. Computer Programming Methodology Heyden & Sons London. 1978.  Turski W. M. Computer Programming Methodology Heyden & Sons London. 1978.","DOI":"10.1145\/1005888.1005894"}],"container-title":["ACM SIGOPS Operating Systems Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1041474.1041476","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1041474.1041476","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:43:41Z","timestamp":1750286621000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1041474.1041476"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1982,4]]},"references-count":7,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1982,4]]}},"alternative-id":["10.1145\/1041474.1041476"],"URL":"https:\/\/doi.org\/10.1145\/1041474.1041476","relation":{},"ISSN":["0163-5980"],"issn-type":[{"type":"print","value":"0163-5980"}],"subject":[],"published":{"date-parts":[[1982,4]]},"assertion":[{"value":"1982-04-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}