{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T12:35:32Z","timestamp":1649075732433},"reference-count":14,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3619,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,9]]},"DOI":"10.1016\/s1571-0661(05)80007-6","type":"journal-article","created":{"date-parts":[[2005,5,20]],"date-time":"2005-05-20T13:21:17Z","timestamp":1116595277000},"page":"464-479","source":"Crossref","is-referenced-by-count":4,"title":["Interface-Based Specification and Verification of Concurrency Controllers"],"prefix":"10.1016","volume":"89","author":[{"given":"Aysu","family":"Betin-Can","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tevfik","family":"Bultan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(05)80007-6_BIBBCB03","article-title":"Interface-based specification and verification of concurrency controllers","author":"Betin-Can","year":"2003","journal-title":"Technical Report 2003-13, Computer Science Department, University of California, Santa Barbara"},{"key":"10.1016\/S1571-0661(05)80007-6_BIBBHPVOO","series-title":"Proc. Workshop on Advances in Verification","article-title":"Java pathfinder: Second generation of a Java model checker","author":"Brat","year":"2000"},{"key":"10.1016\/S1571-0661(05)80007-6_BIBBUL00","series-title":"Proc. 22nd International Conference on Software Engineering","first-page":"335","article-title":"Action Language: A specification language for model checking reactive systems","author":"Bultan","year":"2000"},{"key":"10.1016\/S1571-0661(05)80007-6_BIBBYK01","series-title":"Proc. 16th IEEE International Conference on Automated Software Engineering","first-page":"382","article-title":"Action language verifier","author":"Bultan","year":"2001"},{"key":"10.1016\/S1571-0661(05)80007-6_BIBCAR96","series-title":"Proc. 3rd Conference on Pattern Languages of Programs","article-title":"Specific notification for Java thread synchronization","author":"Cargill","year":"1996"},{"key":"10.1016\/S1571-0661(05)80007-6_BIBCH74","series-title":"Operating Systems, volume 16 of LNCS","first-page":"89","article-title":"The specification of process synchronization by path expressions","author":"Campbell","year":"1974"},{"key":"10.1016\/S1571-0661(05)80007-6_BIBDAH01","series-title":"Proc. 9th Annual Symposium on Foundations of Software Engineering","first-page":"109","article-title":"Interface automata","author":"de Alfaro","year":"2001"},{"key":"10.1016\/S1571-0661(05)80007-6_BIBDDHM02","series-title":"Proc. 24th International Conference on Software Engineering","article-title":"Invariant-based specification, synthesis, and verification of synchronization in concurrent programs","author":"Deng","year":"2002"},{"key":"10.1016\/S1571-0661(05)80007-6_BIBDEL00","series-title":"Proc. 12th International Conference on Computer Aided Verification, volume 1855 of LNCS","first-page":"53","article-title":"Automatic verification of parameterized cache coherence protocols","author":"Delzanno","year":"2000"},{"key":"10.1016\/S1571-0661(05)80007-6_BIBLEA99","series-title":"Concurrent Programming in Java","author":"Lea","year":"1999"},{"key":"10.1016\/S1571-0661(05)80007-6_BIBPDH99","series-title":"Theoretical and Practical Aspects of SPIN Model Checking, volume 1680 of LNCS","article-title":"Assume guarantee model checking of software: A comparative case study","author":"Pasareanu","year":"1999"},{"key":"10.1016\/S1571-0661(05)80007-6_BIBYKB02","series-title":"Proc. 2002 ACM\/SIGSOFT International Symposium on Software Testing and Analysis","first-page":"169","article-title":"Specification, verification, and synthesis of concurrency control components","author":"Yavuz-Kahveci","year":"2002"},{"key":"10.1016\/S1571-0661(05)80007-6_BIBYKTB01","series-title":"Proc. 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 2031 of LNCS","first-page":"335","article-title":"A library for composite symbolic representations","author":"Yavuz-Kahveci","year":"2001"},{"key":"10.1016\/S1571-0661(05)80007-6_BIBZHO97","series-title":"Modeling of Airport Operations Using An Object-Oriented Approach","author":"Zhong","year":"1997"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105800076?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105800076?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,1,26]],"date-time":"2019-01-26T10:50:26Z","timestamp":1548499826000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105800076"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,9]]},"references-count":14,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,9]]}},"alternative-id":["S1571066105800076"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(05)80007-6","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,9]]}}}