{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,20]],"date-time":"2023-02-20T11:31:29Z","timestamp":1676892689128},"reference-count":5,"publisher":"World Scientific Pub Co Pte Lt","issue":"04","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Found. Comput. Sci."],"published-print":{"date-parts":[[2011,6]]},"abstract":"<jats:p> We propose a symbolic verification method for directory-based consistency protocols working for an arbitrary number of controlled resources and competing processes. We use a graph-based language to specify in a uniform way both client\/server interaction schemes and manipulation of directories that contain the access rights of individual clients. Graph transformations model the dynamics of a given protocol. Universally quantified conditions defined on the labels of edges incident to a given node are used to model inspection of directories, invalidation loops and integrity conditions. Our verification procedure computes an approximated backward reachability analysis by using a symbolic representation of sets of configurations. Termination is ensured by using the theory of well-quasi orderings. <\/jats:p>","DOI":"10.1142\/s0129054111008416","type":"journal-article","created":{"date-parts":[[2011,6,10]],"date-time":"2011-06-10T08:52:34Z","timestamp":1307695954000},"page":"761-782","source":"Crossref","is-referenced-by-count":4,"title":["AUTOMATIC VERIFICATION OF DIRECTORY-BASED CONSISTENCY PROTOCOLS WITH GRAPH CONSTRAINTS"],"prefix":"10.1142","volume":"22","author":[{"given":"PAROSH AZIZ","family":"ABDULLA","sequence":"first","affiliation":[{"name":"Uppsla University, Department of Information Technology, Box 337, 751 05 Uppsala, Sweden"}]},{"given":"GIORGIO","family":"DELZANNO","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Genova, via Dodecaneso 35, 16146 Genov, Italy"}]},{"given":"AHMED","family":"REZINE","sequence":"additional","affiliation":[{"name":"University of Uppsala, Department of Information Technology, Box 337, 751 05 Uppsala, Sweden"}]}],"member":"219","published-online":{"date-parts":[[2011,11,20]]},"reference":[{"key":"rf11","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.11.007"},{"key":"rf13","first-page":"257","volume":"23","author":"Delzanno G.","journal-title":"FMSD"},{"key":"rf16","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"rf18","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00103-1"},{"key":"rf23","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-002-0091-4"}],"container-title":["International Journal of Foundations of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0129054111008416","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,6]],"date-time":"2019-08-06T20:33:15Z","timestamp":1565123595000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0129054111008416"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,6]]},"references-count":5,"journal-issue":{"issue":"04","published-online":{"date-parts":[[2011,11,20]]},"published-print":{"date-parts":[[2011,6]]}},"alternative-id":["10.1142\/S0129054111008416"],"URL":"https:\/\/doi.org\/10.1142\/s0129054111008416","relation":{},"ISSN":["0129-0541","1793-6373"],"issn-type":[{"value":"0129-0541","type":"print"},{"value":"1793-6373","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,6]]}}}