{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,9]],"date-time":"2026-04-09T21:15:05Z","timestamp":1775769305816,"version":"3.50.1"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030781415","type":"print"},{"value":"9783030781422","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-78142-2_8","type":"book-chapter","created":{"date-parts":[[2021,6,7]],"date-time":"2021-06-07T23:06:27Z","timestamp":1623107187000},"page":"121-133","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Java Typestate Checker"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3182-2245","authenticated-orcid":false,"given":"Jo\u00e3o","family":"Mota","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7582-0308","authenticated-orcid":false,"given":"Marco","family":"Giunti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8074-0380","authenticated-orcid":false,"given":"Ant\u00f3nio","family":"Ravara","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,6,8]]},"reference":[{"issue":"10","key":"8_CR1","doi-asserted-by":"publisher","first-page":"838","DOI":"10.1145\/3022671.2984004","volume":"51","author":"N Amin","year":"2016","unstructured":"Amin, N., Tate, R.: Java and Scala\u2019s type systems are unsound: the existential crisis of null pointers. ACM SIGPLAN Notices 51(10), 838\u2013848 (2016). https:\/\/doi.org\/10.1145\/3022671.2984004","journal-title":"ACM SIGPLAN Notices"},{"issue":"2\u20133","key":"8_CR2","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1561\/2500000031","volume":"3","author":"D Ancona","year":"2016","unstructured":"Ancona, D., et al.: Behavioral types in programming languages. Found. Trends Program. Lang. 3(2\u20133), 95\u2013230 (2016). https:\/\/doi.org\/10.1561\/2500000031","journal-title":"Found. Trends Program. Lang."},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Bacchiani, L., Bravetti, M., Lange, J., Zavattaro, G.: A session subtyping tool, to appear. In: 23rd International Conference on Coordination Models and Languages (2021)","DOI":"10.1007\/978-3-030-78142-2_6"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-22655-7_2","volume-title":"ECOOP 2011 \u2013 Object-Oriented Programming","author":"NE Beckman","year":"2011","unstructured":"Beckman, N.E., Kim, D., Aldrich, J.: An empirical study of object protocols in the wild. In: Mezini, M. (ed.) ECOOP 2011. LNCS, vol. 6813, pp. 2\u201326. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22655-7_2"},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: The 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 259\u2013270 (2005). https:\/\/doi.org\/10.1145\/1040305.1040327","DOI":"10.1145\/1040305.1040327"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-44898-5_4","volume-title":"Static Analysis","author":"J Boyland","year":"2003","unstructured":"Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55\u201372. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-44898-5_4"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-030-64437-6_6","volume-title":"Programming Languages and Systems","author":"M Bravetti","year":"2020","unstructured":"Bravetti, M., et al.: Behavioural types for memory and method safety in a core object-oriented language. In: Oliveira, B.C.S. (ed.) APLAS 2020. LNCS, vol. 12470, pp. 105\u2013124. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-64437-6_6"},{"issue":"1","key":"8_CR8","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1145\/234313.234418","volume":"28","author":"L Cardelli","year":"1996","unstructured":"Cardelli, L.: Type systems. ACM Comput. Surv. 28(1), 263\u2013264 (1996). https:\/\/doi.org\/10.1145\/234313.234418","journal-title":"ACM Comput. Surv."},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"8_CR10","unstructured":"DeLine, R., F\u00e4hndrich, M.: The fugue protocol checker: Is your software baroque. Technical Report, Technical Report MSR-TR-2004-07, Microsoft Research (2004)"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"Dietl, W., Dietzel, S., Ernst, M.D., Mu\u015flu, K., Schiller, T.W.: Building and using pluggable type-checkers. In: The 33rd International Conference on Software Engineering, pp. 681\u2013690 (2011). https:\/\/doi.org\/10.1145\/1985793.1985889","DOI":"10.1145\/1985793.1985889"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-540-24851-4_7","volume-title":"ECOOP 2004 \u2013 Object-Oriented Programming","author":"T Ekman","year":"2004","unstructured":"Ekman, T., Hedin, G.: Rewritable reference attributed grammars. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 147\u2013171. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24851-4_7"},{"key":"8_CR13","doi-asserted-by":"publisher","unstructured":"Ekman, T., Hedin, G.: The jastadd extensible java compiler. In: The 22nd Annual ACM SIGPLAN Conference on Object-oriented Programming Systems and Applications, pp. 1\u201318 (2007). https:\/\/doi.org\/10.1145\/1297105.1297029","DOI":"10.1145\/1297105.1297029"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-642-27940-9_14","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P Ferrara","year":"2012","unstructured":"Ferrara, P., M\u00fcller, P.: Automatic inference of access permissions. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 202\u2013218. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-27940-9_14"},{"issue":"4","key":"8_CR15","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/2629609","volume":"36","author":"R Garcia","year":"2014","unstructured":"Garcia, R., Tanter, \u00c9., Wolff, R., Aldrich, J.: Foundations of typestate-oriented programming. ACM Trans. Program. Lang. Syst. (TOPLAS) 36(4), 12 (2014). https:\/\/doi.org\/10.1145\/2629609","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"issue":"1","key":"8_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"JY Girard","year":"1987","unstructured":"Girard, J.Y.: Linear logic. Theoretical Comput. Sci. 50(1), 1\u2013101 (1987). https:\/\/doi.org\/10.1016\/0304-3975(87)90045-4","journal-title":"Theoretical Comput. Sci."},{"key":"8_CR17","unstructured":"Group, T.P.: The plaid programming language - introduction. https:\/\/www.cs.cmu.edu\/aldrich\/plaid\/plaid-intro.pdf. Accessed 10 Apr 2021"},{"key":"8_CR18","unstructured":"Hoare, T.: Null references: The billion dollar mistake, Presentation at QCon London (2009). https:\/\/tinyurl.com\/eyipowm4"},{"issue":"1","key":"8_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2873052","volume":"49","author":"H H\u00fcttel","year":"2016","unstructured":"H\u00fcttel, H., et al.: Foundations of session types and behavioural contracts. ACM Comput. Surv. (CSUR) 49(1), 1\u201336 (2016). https:\/\/doi.org\/10.1145\/2873052","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"8_CR20","doi-asserted-by":"publisher","unstructured":"Ishtiaq, S.S., O\u2019hearn, P.W.: Bi as an assertion language for mutable data structures. In: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 14\u201326 (2001). https:\/\/doi.org\/10.1145\/1988042.1988050","DOI":"10.1145\/1988042.1988050"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41\u201355. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_4"},{"key":"8_CR22","volume-title":"Kotlin in Action","author":"D Jemerov","year":"2017","unstructured":"Jemerov, D., Isakova, S.: Kotlin in Action. Manning Publications Company, New York (2017)"},{"key":"8_CR23","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In: Mason, R.E.A. (ed.) The IFIP 9th World Computer Congress Information Processing, Paris, vol. 83, pp. 321\u2013332 (1983). North-Holland\/IFIP (1983)"},{"key":"8_CR24","doi-asserted-by":"publisher","unstructured":"Kouzapas, D., Dardha, O., Perera, R., Gay, S.J.: Typechecking protocols with mungo and stmungo. In: The 18th International Symposium on Principles and Practice of Declarative Programming, pp. 146\u2013159. ACM (2016). https:\/\/doi.org\/10.1145\/2967973.2968595","DOI":"10.1145\/2967973.2968595"},{"key":"8_CR25","unstructured":"Mota, J.: Coping with the reality: adding crucial features to a typestate-oriented language. Master\u2019s thesis, NOVA School of Science and Technology (2021). https:\/\/github.com\/jdmota\/java-typestate-checker\/blob\/master\/docs\/msc-thesis.pdf"},{"issue":"1","key":"8_CR26","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1145\/2103621.2103722","volume":"47","author":"K Naden","year":"2012","unstructured":"Naden, K., Bocchino, R., Aldrich, J., Bierhoff, K.: A type system for borrowing permissions. ACM SIGPLAN Notices 47(1), 557\u2013570 (2012). https:\/\/doi.org\/10.1145\/2103621.2103722","journal-title":"ACM SIGPLAN Notices"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1\u201319. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44802-0_1"},{"key":"8_CR28","doi-asserted-by":"publisher","unstructured":"Papi, M.M., Ali, M., Correa Jr, T.L., Perkins, J.H., Ernst, M.D.: Practical pluggable types for java. In: The 2008 International Symposium on Software Testing and Analysis, pp. 201\u2013212 (2008). https:\/\/doi.org\/10.1145\/1390630.1390656","DOI":"10.1145\/1390630.1390656"},{"key":"8_CR29","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pp. 55\u201374. IEEE (2002). https:\/\/doi.org\/10.1109\/lics.2002.1029817","DOI":"10.1109\/lics.2002.1029817"},{"key":"8_CR30","doi-asserted-by":"publisher","first-page":"110150","DOI":"10.1016\/j.jss.2019.110450","volume":"159","author":"A Sadiq","year":"2020","unstructured":"Sadiq, A., Li, Y.F., Ling, S.: A survey on the use of access permission-based specifications for program verification. J. Syst. Softw. 159, 110150 (2020). https:\/\/doi.org\/10.1016\/j.jss.2019.110450","journal-title":"J. Syst. Softw."},{"key":"8_CR31","unstructured":"Sunshine, J.: Protocol programmability. Ph.D. thesis, Carnegie Mellon University, Pittsburgh (2013)"},{"issue":"10","key":"8_CR32","doi-asserted-by":"publisher","first-page":"713","DOI":"10.1145\/2076021.2048122","volume":"46","author":"J Sunshine","year":"2011","unstructured":"Sunshine, J., Naden, K., Stork, S., Aldrich, J., Tanter, \u00c9.: First-class state change in plaid. ACM SIGPLAN Notices 46(10), 713\u2013732 (2011). https:\/\/doi.org\/10.1145\/2076021.2048122","journal-title":"ACM SIGPLAN Notices"},{"key":"8_CR33","unstructured":"Wetsman, N.: Contact tracing app for England and wales failed to flag people exposed to Covid-19. The Verge (2020). https:\/\/www.theverge.com\/2020\/11\/2\/21546618\/uk-coronavirus-contact-tracing-app-error-alert-isolation"}],"container-title":["Lecture Notes in Computer Science","Coordination Models and Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-78142-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T22:02:48Z","timestamp":1749333768000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-78142-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030781415","9783030781422"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-78142-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"8 June 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"COORDINATION","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Coordination Languages and Models","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Valletta","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Malta","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 June 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 June 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"coordination2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.discotec.org\/2021\/coordination.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"15","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"48% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Due to the Corona pandemic this event was held virutally.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}