{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T05:55:28Z","timestamp":1725602128538},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642244308"},{"type":"electronic","value":"9783642244315"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-24431-5_3","type":"book-chapter","created":{"date-parts":[[2011,8,23]],"date-time":"2011-08-23T22:29:46Z","timestamp":1314138586000},"page":"6-20","source":"Crossref","is-referenced-by-count":3,"title":["Lightweight Verification of a Multi-Task Threaded Server: A Case Study With The Plural Tool"],"prefix":"10.1007","author":[{"given":"N\u00e9stor","family":"Cata\u00f1o","sequence":"first","affiliation":[]},{"given":"Ijaz","family":"Ahmed","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"Ahmed, I., Cata\u00f1o, N.: Architecture of Novabase\u2019 MTTS application. Technical report, The University of Madeira (2010), http:\/\/www3.uma.pt\/ncatano\/aeminium\/Documents_files\/mtts.pdf"},{"key":"3_CR2","doi-asserted-by":"publisher","first-page":"2004","DOI":"10.5381\/jot.2004.3.6.a2","volume":"3","author":"M. Barnett","year":"2004","unstructured":"Barnett, M., DeLine, R., Fhndrich, M., Rustan, K., Leino, M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology\u00a03 (2004)","journal-title":"Journal of Object Technology"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Bierhoff, K., Aldrich, J.: Modular typestate checking of aliased objects. In: Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming Systems and Applications, OOPSLA, pp. 301\u2013320 (2007)","DOI":"10.1145\/1297027.1297050"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-642-03013-0_10","volume-title":"ECOOP 2009 \u2013 Object-Oriented Programming","author":"K. Bierhoff","year":"2009","unstructured":"Bierhoff, K., Beckman, N.E., Aldrich, J.: Practical API protocol checking with access permissions. In: Drossopoulou, S. (ed.) ECOOP 2009. LNCS, vol.\u00a05653, pp. 195\u2013219. Springer, Heidelberg (2009)"},{"key":"3_CR5","unstructured":"Bierhoff, N.B.K., Aldrich, J.: Verifying correct usage of atomic blocks and typestate. In: OOPSLA (2008)"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Boyland, J.: Checking interference with fractional permissions. In: Proceedings of the 10th International Conference on Static Analysis, SAS, pp. 55\u201372 (2003)","DOI":"10.1007\/3-540-44898-5_4"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Burdy, L., Cheon, Y., Cok, D., Ernst, M.D., Kiniry, J., Leavens, G.T., Rustan, K., Leino, M., Poll, E.: An overview of JML tools and applications (2003)","DOI":"10.1016\/S1571-0661(04)80810-7"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Cata\u00f1o, N., Wahls, T.: Executing JML specifications of java card applications: A case study. In: 24th ACM Symposium on Applied Computing, Software Engineering Track (SAC-SE), Honolulu, Hawaii, March 8-12, pp. 404\u2013408 (2009)","DOI":"10.1145\/1529282.1529373"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"DeLine, R., F\u00e4hndrich, M.: Enforcing high-level protocols in low-level software. In: Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation, PLDI, pp. 59\u201369 (2001)","DOI":"10.1145\/381694.378811"},{"key":"3_CR10","unstructured":"DeLine, R., F\u00e4hndrich, M.: The Fugue protocol checker: Is your software baroque (2003)"},{"key":"3_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear logic. Theoretical Computer Science\u00a050, 1\u2013102 (1987)","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"3_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"G.T. Leavens","year":"2006","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. ACM SIGSOFT (Software Engineering Symposium)\u00a031(3), 1\u201338 (2006)","journal-title":"ACM SIGSOFT (Software Engineering Symposium)"},{"key":"3_CR13","unstructured":"Novabase, http:\/\/www.novabase.pt"},{"key":"3_CR14","unstructured":"The Plural Tool, http:\/\/code.google.com\/p\/pluralism\/"},{"key":"3_CR15","first-page":"222","volume-title":"NASA Formal Methods Symposium (NFM), NASA\/CP-2010-216215","author":"P. Roux","year":"2010","unstructured":"Roux, P., Siminiceanu, R.: Model checking with edge-valued decision diagrams. In: NASA Formal Methods Symposium (NFM), NASA\/CP-2010-216215, pp. 222\u2013226. Langley Research Center, NASA (April 2010)"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Stork, S., Marques, P., Aldrich, J.: Concurrency by default: using permissions to express dataflow in stateful programs. In: Conference on Object-Oriented Programming Systems and Applications, OOPSLA, pp. 933\u2013940 (2009)","DOI":"10.1145\/1639950.1640060"},{"key":"3_CR17","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1109\/TSE.1986.6312929","volume":"12","author":"R.E. Strom","year":"1986","unstructured":"Strom, R.E., Yemini, S.: Typestate: A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering\u00a012, 157\u2013171 (1986)","journal-title":"IEEE Transactions on Software Engineering"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24431-5_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,14]],"date-time":"2019-06-14T05:34:09Z","timestamp":1560490449000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24431-5_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642244308","9783642244315"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24431-5_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}