{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:13:24Z","timestamp":1725491604797},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540752905"},{"type":"electronic","value":"9783540752929"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75292-9_5","type":"book-chapter","created":{"date-parts":[[2007,9,11]],"date-time":"2007-09-11T10:43:07Z","timestamp":1189507387000},"page":"64-78","source":"Crossref","is-referenced-by-count":0,"title":["Automatic Refinement of Split Binary Semaphore"],"prefix":"10.1007","author":[{"given":"Dami\u00e1n","family":"Barsotti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Javier O.","family":"Blanco","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","unstructured":"Dijkstra, E.W.: A tutorial on the split binary semaphore (March 1979), \n                  \n                    http:\/\/www.cs.utexas.edu\/users\/EWD\/ewd07xx\/EWD703.PDF"},{"key":"5_CR2","series-title":"Graduate texts in computer science","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-1830-2","volume-title":"On Concurrent Programming","author":"F.B. Schneider","year":"1997","unstructured":"Schneider, F.B.: On Concurrent Programming. Graduate texts in computer science. Springer, New York, Inc. (1997)"},{"issue":"1","key":"5_CR3","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/S0304-3975(96)00191-0","volume":"173","author":"N. Bjorner","year":"1997","unstructured":"Bjorner, N., Browne, A., Manna, Z.: Automatic generation of invariants and intermediate assertions. Theor. Comput. Sci.\u00a0173(1), 49\u201387 (1997)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2004","unstructured":"Barrett, C., Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"key":"5_CR5","unstructured":"Paulson, L.C.: The Isabelle reference manual (2004), \n                  \n                    http:\/\/isabelle.in.tum.de\/doc\/ref.pdf"},{"key":"5_CR6","volume-title":"Foundations of Multithreaded, Parallel, and Distributed Programming","author":"G. Andrews","year":"1999","unstructured":"Andrews, G.: Foundations of Multithreaded, Parallel, and Distributed Programming. Addison-Wesley, Reading, Massachusetts, USA (1999)"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Martin, A., van de Snepscheut, J.: Design of synchronization algorithms. Constructive Methods in Computing Science, pp. 445\u2013478 (1989)","DOI":"10.1007\/978-3-642-74884-4_13"},{"key":"5_CR8","unstructured":"Barsotti, D., Blanco, J.O.: (Im)proving split binary semaphores. Tecnical Report (2007), Available at \n                  \n                    http:\/\/www.cs.famaf.unc.edu.ar\/~damian\/publicaciones\/sbdinv\/SBDwip_ext.pdf"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-45319-9_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Tiwari","year":"2001","unstructured":"Tiwari, A., Rue\u00df, H., Sa\u00efdi, H., Shankar, N.: A technique for invariant generation. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, pp. 113\u2013127. Springer, Heidelberg (2001)"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: On the faithfulness of formal models. In: Mathematical Foundations of Computer Science, pp. 28\u201342 (1991)","DOI":"10.1007\/3-540-54345-7_46"},{"key":"5_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate calculus and program semantics","author":"E.W. Dijkstra","year":"1990","unstructured":"Dijkstra, E.W., Scholten, C.S.: Predicate calculus and program semantics. Springer, New York, Inc. (1990)"},{"issue":"7","key":"5_CR12","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1145\/359636.359710","volume":"20","author":"J.L.W. Kessels","year":"1977","unstructured":"Kessels, J.L.W.: An alternative to event queues for synchronization in monitors. Commun. ACM\u00a020(7), 500\u2013503 (1977)","journal-title":"Commun. ACM"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2007"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75292-9_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:59:02Z","timestamp":1619521142000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75292-9_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540752905","9783540752929"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75292-9_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}