{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,23]],"date-time":"2026-10-23T03:27:53Z","timestamp":1792726073133,"version":"4.5.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030290252","type":"print"},{"value":"9783030290269","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-29026-9_22","type":"book-chapter","created":{"date-parts":[[2019,8,21]],"date-time":"2019-08-21T19:10:06Z","timestamp":1566414606000},"page":"391-408","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Behavioral Program Logic"],"prefix":"10.1007","author":[{"given":"Eduard","family":"Kamburjan","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,8,14]]},"reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6","volume-title":"Deductive Software Verification - The KeY Book - From Theory to Practice","year":"2016","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice. LNCS, vol. 10001. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-49812-6"},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/3-540-45165-X_2","volume-title":"Java on Smart Cards:Programming and Security","author":"B Beckert","year":"2001","unstructured":"Beckert, B.: A dynamic logic for the formal verification of Java Card programs. In: Attali, I., Jensen, T. (eds.) JavaCard 2000. LNCS, vol. 2041, pp. 6\u201324. Springer, Heidelberg (2001). \n                      https:\/\/doi.org\/10.1007\/3-540-45165-X_2"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-642-38574-2_22","volume-title":"Automated Deduction \u2013 CADE-24","author":"B Beckert","year":"2013","unstructured":"Beckert, B., Bruns, D.: Dynamic logic with trace semantics. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 315\u2013329. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-38574-2_22"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-540-70583-3_9","volume-title":"Automata, Languages and Programming","author":"M Berger","year":"2008","unstructured":"Berger, M., Honda, K., Yoshida, N.: Completeness and logical full abstraction in modal logics for typed mobile processes. In: Aceto, L., Damg\u00e5rd, I., Goldberg, L.A., Halld\u00f3rsson, M.M., Ing\u00f3lfsd\u00f3ttir, A., Walukiewicz, I. (eds.) ICALP 2008. LNCS, vol. 5126, pp. 99\u2013111. Springer, Heidelberg (2008). \n                      https:\/\/doi.org\/10.1007\/978-3-540-70583-3_9"},{"issue":"1","key":"22_CR5","first-page":"61","volume":"22","author":"L Bocchi","year":"2012","unstructured":"Bocchi, L., Lange, J., Tuosto, E.: Three algorithms and a methodology for amending contracts for choreographies. Sci. Ann. Comput. Sci. 22(1), 61\u2013104 (2012)","journal-title":"Sci. Ann. Comput. Sci."},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-319-46508-1_8","volume-title":"Transactions on Foundations for Mastering Change I","author":"R Bubel","year":"2016","unstructured":"Bubel, R., et al.: Proof repositories for compositional verification of evolving software systems - managing change when proving software correct. In: Steffen, B. (ed.) Transactions on Foundations for Mastering Change I. LNCS, vol. 9960, pp. 130\u2013156. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-46508-1_8"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-319-24312-2_21","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R Bubel","year":"2015","unstructured":"Bubel, R., Din, C.C., H\u00e4hnle, R., Nakata, K.: A dynamic logic with traces and coinduction. In: De Nivelle, H. (ed.) TABLEAUX 2015. LNCS (LNAI), vol. 9323, pp. 307\u2013322. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-24312-2_21"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-642-15375-4_16","volume-title":"CONCUR 2010 - Concurrency Theory","author":"L Caires","year":"2010","unstructured":"Caires, L., Pfenning, F.: Session types as intuitionistic linear propositions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 222\u2013236. Springer, Heidelberg (2010). \n                      https:\/\/doi.org\/10.1007\/978-3-642-15375-4_16"},{"issue":"5","key":"22_CR9","doi-asserted-by":"publisher","first-page":"76:1","DOI":"10.1145\/3122848","volume":"50","author":"FS Boer de","year":"2017","unstructured":"de Boer, F.S., et al.: A survey of active object languages. ACM Comput. Surv. 50(5), 76:1\u201376:39 (2017)","journal-title":"ACM Comput. Surv."},{"key":"22_CR10","unstructured":"Dezani-Ciancaglini, M.: Personal Communication, 19 October 2018"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-319-66902-1_2","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"CC Din","year":"2017","unstructured":"Din, C.C., H\u00e4hnle, R., Johnsen, E.B., Pun, K.I., Tapia Tarifa, S.L.: Locally abstract, globally concrete semantics of concurrent programming languages. In: Schmidt, R.A., Nalon, C. (eds.) TABLEAUX 2017. LNCS (LNAI), vol. 10501, pp. 22\u201343. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-66902-1_2"},{"issue":"5\u20136","key":"22_CR12","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1016\/j.jlamp.2014.03.003","volume":"83","author":"CC Din","year":"2014","unstructured":"Din, C.C., Owe, O.: A sound and complete reasoning system for asynchronous communication with shared futures. J. Log. Algebraic Methods Program. 83(5\u20136), 360\u2013383 (2014)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"22_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-319-25423-4_14","volume-title":"Formal Methods and Software Engineering","author":"CC Din","year":"2015","unstructured":"Din, C.C., Tapia Tarifa, S.L., H\u00e4hnle, R., Johnsen, E.B.: History-based specification and verification of scalable concurrent and distributed systems. In: Butler, M., Conchon, S., Za\u00efdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 217\u2013233. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-25423-4_14"},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-642-38592-6_19","volume-title":"Formal Techniques for Distributed Systems","author":"AE Flores-Montoya","year":"2013","unstructured":"Flores-Montoya, A.E., Albert, E., Genaim, S.: May-happen-in-parallel based deadlock analysis for concurrent objects. In: Beyer, D., Boreale, M. (eds.) FMOODS\/FORTE -2013. LNCS, vol. 7892, pp. 273\u2013288. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-38592-6_19"},{"key":"22_CR15","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/3-7643-7304-0_2","volume-title":"Logica Universalis","author":"M Garc\u00eda-Matos","year":"2005","unstructured":"Garc\u00eda-Matos, M., V\u00e4\u00e4n\u00e4nen, J.: Abstract model theory as a framework for universal logic. In: Beziau, J.-Y. (ed.) Logica Universalis, pp. 19\u201333. Basel, Birkh\u00e4user Basel (2005)"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-319-28934-2_11","volume-title":"Formal Aspects of Component Software","author":"E Giachino","year":"2016","unstructured":"Giachino, E., Johnsen, E.B., Laneve, C., Pun, K.I.: Time complexity of concurrent programs. In: Braga, C., \u00d6lveczky, P.C. (eds.) FACS 2015. LNCS, vol. 9539, pp. 199\u2013216. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-28934-2_11"},{"key":"22_CR17","first-page":"88","volume":"20","author":"L Henkin","year":"1968","unstructured":"Henkin, L.: Relativization with respect to formulas and its use in proofs of independence. Compositio Mathematica 20, 88\u2013106 (1968)","journal-title":"Compositio Mathematica"},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-319-66845-1_13","volume-title":"Integrated Formal Methods","author":"L Henrio","year":"2017","unstructured":"Henrio, L., Laneve, C., Mastandrea, V.: Analysis of synchronisations in stateful active objects. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 195\u2013210. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-66845-1_13"},{"key":"22_CR19","doi-asserted-by":"publisher","first-page":"9:1","DOI":"10.1145\/2827695","volume":"63","author":"K Honda","year":"2016","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. JACM 63, 9:1\u20139:67 (2016)","journal-title":"JACM"},{"issue":"1","key":"22_CR20","doi-asserted-by":"publisher","first-page":"3: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. 49(1), 3:1\u20133:36 (2016)","journal-title":"ACM Comput. Surv."},{"key":"22_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-25271-6_8","volume-title":"Formal Methods for Components and Objects","author":"EB Johnsen","year":"2011","unstructured":"Johnsen, E.B., H\u00e4hnle, R., Sch\u00e4fer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 142\u2013164. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-25271-6_8"},{"key":"22_CR22","unstructured":"Kamburjan, E. Behavioral program logic and LAGC semantics without continuations (technical report). CoRR abs\/1904.13338 (2019)"},{"key":"22_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-319-98938-9_13","volume-title":"Integrated Formal Methods","author":"E Kamburjan","year":"2018","unstructured":"Kamburjan, E., Chen, T.-C.: Stateful behavioral types for active objects. In: Furia, C.A., Winter, K. (eds.) IFM 2018. LNCS, vol. 11023, pp. 214\u2013235. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-98938-9_13"},{"key":"22_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/978-3-319-47846-3_19","volume-title":"Formal Methods and Software Engineering","author":"E Kamburjan","year":"2016","unstructured":"Kamburjan, E., Din, C.C., Chen, T.-C.: Session-based compositional analysis for actor-based languages using futures. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016. LNCS, vol. 10009, pp. 296\u2013312. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-47846-3_19"},{"key":"22_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-319-68499-4_9","volume-title":"RSSRail 2017: Reliability, Safety, and Security of Railway Systems","author":"E Kamburjan","year":"2017","unstructured":"Kamburjan, E., H\u00e4hnle, R.: Deductive verification of railway operations. In: Fantechi, A., Lecomte, T., Romanovsky, A.B. (eds.) RSSRail 2017. LNCS, vol. 10598, pp. 131\u2013147. Springer, Uk (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-68499-4_9"},{"key":"22_CR26","first-page":"1","volume":"13","author":"R Neykova","year":"2017","unstructured":"Neykova, R., Yoshida, N.: Multiparty session actors. Log. Methods Comput. Sci. 13, 1 (2017)","journal-title":"Log. Methods Comput. Sci."},{"issue":"12","key":"22_CR27","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1145\/2699407","volume":"58","author":"P Wadler","year":"2015","unstructured":"Wadler, P.: Propositions as types. Commun. ACM 58(12), 75\u201384 (2015)","journal-title":"Commun. ACM"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-29026-9_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,21]],"date-time":"2019-08-21T19:15:42Z","timestamp":1566414942000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-29026-9_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030290252","9783030290269"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-29026-9_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"14 August 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TABLEAUX","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Reasoning with Analytic Tableaux and Related Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"London","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 September 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 September 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tableaux2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/tableaux2019.org\/","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":"43","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":"25","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":"0","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":"58% - 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.2","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":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}