{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T08:58:16Z","timestamp":1780563496046,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":46,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,10,22]],"date-time":"2019-10-22T00:00:00Z","timestamp":1571702400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,10,22]]},"DOI":"10.1145\/3358499.3361221","type":"proceedings-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T15:16:45Z","timestamp":1570807005000},"page":"11-20","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Modal assertions for actor correctness"],"prefix":"10.1145","author":[{"given":"Colin S.","family":"Gordon","sequence":"first","affiliation":[{"name":"Drexel University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,10,22]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"crossref","unstructured":"Wolfgang Ahrendt Bernhard Beckert Richard Bubel Reiner H\u00e4hnle Peter H Schmitt and Mattias Ulbrich. 2016. Deductive Software Verification\u2013The KeY Book. Springer.  Wolfgang Ahrendt Bernhard Beckert Richard Bubel Reiner H\u00e4hnle Peter H Schmitt and Mattias Ulbrich. 2016. Deductive Software Verification\u2013The KeY Book. Springer.","DOI":"10.1007\/978-3-319-49812-6"},{"key":"e_1_3_2_1_2_1","volume-title":"Panini: A Concurrent Programming Model for Solving Pervasive and Oblivious Interference. In MODULARITY","author":"Bagherzadeh Mehdi","year":"2015"},{"key":"e_1_3_2_1_3_1","volume-title":"Order Types: Static Reasoning About Message Races in Asynchronous Message Passing Concurrency. In AGERE.","author":"Bagherzadeh Mehdi","year":"2017"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_22"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1020083231504"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01049415"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Torben Bra\u00fcner. 2010. Hybrid logic and its proof-theory. Springer.  Torben Bra\u00fcner. 2010. Hybrid logic and its proof-theory. Springer.","DOI":"10.1007\/978-94-007-0002-4"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Sylvan Clebsch Sophia Drossopoulou Sebastian Blessing and Andy McNeil. 2015. Deny capabilities for safe fast actors. In AGERE.  Sylvan Clebsch Sophia Drossopoulou Sebastian Blessing and Andy McNeil. 2015. Deny capabilities for safe fast actors. In AGERE.","DOI":"10.1145\/2824815.2824816"},{"key":"e_1_3_2_1_9_1","volume-title":"Formal Methods for Open Objectbased Distributed Systems","author":"Cola\u00e7o Jean-Louis"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276529"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Thomas Dinsdale-Young Mike Dodds Philippa Gardner Matthew Parkinson and Viktor Vafeiadis. 2010. Concurrent Abstract Predicates. In ECOOP.  Thomas Dinsdale-Young Mike Dodds Philippa Gardner Matthew Parkinson and Viktor Vafeiadis. 2010. Concurrent Abstract Predicates. In ECOOP.","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Mike Dodds Xinyu Feng Matthew Parkinson and Viktor Vafeiadis. 2009. Deny-Guarantee Reasoning. In ESOP.  Mike Dodds Xinyu Feng Matthew Parkinson and Viktor Vafeiadis. 2009. Deny-Guarantee Reasoning. In ESOP.","DOI":"10.1007\/978-3-642-00590-9_26"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Emanuele D\u2019Osualdo Jonathan Kochems and C-H Luke Ong. 2013. Automatic verification of Erlang-style concurrency. In SAS.  Emanuele D\u2019Osualdo Jonathan Kochems and C-H Luke Ong. 2013. Automatic verification of Erlang-style concurrency. In SAS.","DOI":"10.1007\/978-3-642-38856-9_24"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Xinyu Feng. 2009. Local Rely-Guarantee Reasoning. In POPL.  Xinyu Feng. 2009. Local Rely-Guarantee Reasoning. In POPL.","DOI":"10.1145\/1480881.1480922"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90046-1"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01054038"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00215625"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Colin S. Gordon Michael D. Ernst and Dan Grossman. 2013. RelyGuarantee References for Refinement Types Over Aliased Mutable Data. In PLDI.  Colin S. Gordon Michael D. Ernst and Dan Grossman. 2013. RelyGuarantee References for Refinement Types Over Aliased Mutable Data. In PLDI.","DOI":"10.1145\/2491956.2462160"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3064850"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Colin S. Gordon Matthew J. Parkinson Jared Parsons Aleks Bromfield and Joe Duffy. 2012. Uniqueness and Reference Immutability for Safe Parallelism. In OOPSLA.  Colin S. Gordon Matthew J. Parkinson Jared Parsons Aleks Bromfield and Joe Duffy. 2012. Uniqueness and Reference Immutability for Safe Parallelism. In OOPSLA.","DOI":"10.1145\/2384616.2384619"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"David Harel. 1979. First-order dynamic logic.  David Harel. 1979. First-order dynamic logic.","DOI":"10.1007\/3-540-09237-4"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Carl Hewitt Peter Bishop Irene Greif Brian Smith Todd Matson and Richard Steiger. 1973. Actor Induction and Meta-Evaluation. In POPL.  Carl Hewitt Peter Bishop Irene Greif Brian Smith Todd Matson and Richard Steiger. 1973. Actor Induction and Meta-Evaluation. In POPL.","DOI":"10.1145\/512927.512942"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_25_1","volume-title":"International Workshop on Types for Proofs and Programs. Springer, 165\u2013182","author":"Honsell Furio","year":"1995"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ale\u0161 Bizjak Lars Birkedal and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming 28 (2018).  Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ale\u0161 Bizjak Lars Birkedal and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming 28 (2018).","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_1_28_1","volume-title":"Dafny: An automatic program verifier for functional correctness. In Logic for Programming, Artificial Intelligence, and Reasoning","author":"Leino K Rustan M","year":"2010"},{"key":"e_1_3_2_1_29_1","unstructured":"K. Rustan M. Leino and Wolfram Schulte. 2007. Using History Invariants to Verify Observers. In ESOP.  K. Rustan M. Leino and Wolfram Schulte. 2007. Using History Invariants to Verify Observers. In ESOP."},{"key":"e_1_3_2_1_30_1","unstructured":"Inc. Lightbend. 2019. Akka Actors. https:\/\/akka.io  Inc. Lightbend. 2019. Akka Actors. https:\/\/akka.io"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"crossref","unstructured":"Nancy A. Lynch and Mark R. Tuttle. 1987. Hierarchical Correctness Proofs for Distributed Algorithms. In PODC.  Nancy A. Lynch and Mark R. Tuttle. 1987. Hierarchical Correctness Proofs for Distributed Algorithms. In PODC.","DOI":"10.1145\/41840.41852"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Maarten Marx and Yde Venema. 1997. Multi-dimensional modal logic. Vol. 4. Springer Science & Business Media.  Maarten Marx and Yde Venema. 1997. Multi-dimensional modal logic. Vol. 4. Springer Science & Business Media.","DOI":"10.1007\/978-94-011-5694-3"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"crossref","unstructured":"Filipe Milit\u00e3o Jonathan Aldrich and Lu\u00eds Caires. 2014. Rely-Guarantee Protocols. In ECOOP.  Filipe Milit\u00e3o Jonathan Aldrich and Lu\u00eds Caires. 2014. Rely-Guarantee Protocols. In ECOOP.","DOI":"10.21236\/ADA605817"},{"key":"e_1_3_2_1_34_1","unstructured":"Filipe Milit\u00e3o Jonathan Aldrich and Lu\u00eds Caires. 2016. Composing Interfering Abstract Protocols. In ECOOP.  Filipe Milit\u00e3o Jonathan Aldrich and Lu\u00eds Caires. 2016. Composing Interfering Abstract Protocols. In ECOOP."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"crossref","unstructured":"Aleksandar Nanevski Ruy Ley-Wild Ilya Sergey and Germ\u00c3\u0105n Andr\u00c3\u013es Delbianco. 2014. Communicating State Transition Systems for Fine-Grained Concurrent Resources. In ESOP.  Aleksandar Nanevski Ruy Ley-Wild Ilya Sergey and Germ\u00c3\u0105n Andr\u00c3\u013es Delbianco. 2014. Communicating State Transition Systems for Fine-Grained Concurrent Resources. In ESOP.","DOI":"10.1007\/978-3-642-54833-8_16"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"crossref","unstructured":"Susan Owicki and David Gries. 1976. An Axiomatic Proof Technique for Parallel Programs I. Acta Informatica (1976) 319\u2013340. Issue 6.  Susan Owicki and David Gries. 1976. An Axiomatic Proof Technique for Parallel Programs I. Acta Informatica (1976) 319\u2013340. Issue 6.","DOI":"10.1007\/BF00268134"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"crossref","unstructured":"Amir Pnueli. 1977. The Temporal Logic of Programs. In FOCS. IEEE.  Amir Pnueli. 1977. The Temporal Logic of Programs. In FOCS. IEEE.","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"crossref","unstructured":"Vaughan R Pratt. 1976. Semantical consideration on Floyd-Hoare logic. In FOCS.  Vaughan R Pratt. 1976. Semantical consideration on Floyd-Hoare logic. In FOCS.","DOI":"10.1109\/SFCS.1976.27"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"crossref","unstructured":"Azalea Raad Jules Villard and Philippa Gardner. 2015. CoLoSL: Concurrent Local Subjective Logic. In ESOP.  Azalea Raad Jules Villard and Philippa Gardner. 2015. CoLoSL: Concurrent Local Subjective Logic. In ESOP.","DOI":"10.1007\/978-3-662-46669-8_29"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02115610"},{"key":"e_1_3_2_1_41_1","unstructured":"Quentin Sti\u00e9venart Jens Nicolay Wolfgang De Meuter and Coen De Roover. 2017. Mailbox Abstractions for Static Analysis of Actor Programs. In ECOOP.  Quentin Sti\u00e9venart Jens Nicolay Wolfgang De Meuter and Coen De Roover. 2017. Mailbox Abstractions for Static Analysis of Actor Programs. In ECOOP."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"crossref","unstructured":"Aaron Turon Derek Dreyer and Lars Birkedal. 2013. Unifying Refinement and Hoare-Style Reasoning in a Logic for Higher-Order Concurrency. In ICFP.  Aaron Turon Derek Dreyer and Lars Birkedal. 2013. Unifying Refinement and Hoare-Style Reasoning in a Logic for Higher-Order Concurrency. In ICFP.","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_3_2_1_43_1","unstructured":"Viktor Vafeiadis. 2007. Modular Fine-Grained Concurrency Verification. PhD Thesis. University of Cambridge.  Viktor Vafeiadis. 2007. Modular Fine-Grained Concurrency Verification. PhD Thesis. University of Cambridge."},{"key":"e_1_3_2_1_44_1","unstructured":"Viktor Vafeiadis and Matthew Parkinson. 2007. A Marriage of Rely\/Guarantee and Separation Logic. In Concurrency Theory (CONCUR).  Viktor Vafeiadis and Matthew Parkinson. 2007. A Marriage of Rely\/Guarantee and Separation Logic. In Concurrency Theory (CONCUR)."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"crossref","unstructured":"Hans Van Ditmarsch Wiebe van Der Hoek and Barteld Kooi. 2007. Dynamic epistemic logic. Vol. 337. Springer Science & Business Media.  Hans Van Ditmarsch Wiebe van Der Hoek and Barteld Kooi. 2007. Dynamic epistemic logic. Vol. 337. Springer Science & Business Media.","DOI":"10.1007\/978-1-4020-5839-4"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"crossref","unstructured":"Niki Vazou Alexander Bakst and Ranjit Jhala. 2015. Bounded Refinement Types. In ICFP.  Niki Vazou Alexander Bakst and Ranjit Jhala. 2015. Bounded Refinement Types. In ICFP.","DOI":"10.1145\/2784731.2784745"}],"event":{"name":"SPLASH '19: 2019 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity","location":"Athens Greece","acronym":"SPLASH '19","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 9th ACM SIGPLAN International Workshop on Programming Based on Actors, Agents, and Decentralized Control"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3358499.3361221","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3358499.3361221","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:23:12Z","timestamp":1750202592000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3358499.3361221"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,22]]},"references-count":46,"alternative-id":["10.1145\/3358499.3361221","10.1145\/3358499"],"URL":"https:\/\/doi.org\/10.1145\/3358499.3361221","relation":{},"subject":[],"published":{"date-parts":[[2019,10,22]]},"assertion":[{"value":"2019-10-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}