{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,2]],"date-time":"2026-01-02T07:44:10Z","timestamp":1767339850343,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":43,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,10,23]],"date-time":"2022-10-23T00:00:00Z","timestamp":1666483200000},"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":[[2022,10,23]]},"DOI":"10.1145\/3550355.3552449","type":"proceedings-article","created":{"date-parts":[[2022,10,24]],"date-time":"2022-10-24T22:44:57Z","timestamp":1666651497000},"page":"278-288","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Model-checking legal contracts with SymboleoPC"],"prefix":"10.1145","author":[{"given":"Alireza","family":"Parvizimosaed","sequence":"first","affiliation":[{"name":"University of Ottawa, Ottawa, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Roveri","sequence":"additional","affiliation":[{"name":"University of Trento, Trento, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aidin","family":"Rasti","sequence":"additional","affiliation":[{"name":"University of Ottawa, Ottawa, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Amyot","sequence":"additional","affiliation":[{"name":"University of Ottawa, Ottawa, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luigi","family":"Logrippo","sequence":"additional","affiliation":[{"name":"Universit\u00e9 du Qu\u00e9bec en Outaouais, Gatineau, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Mylopoulos","sequence":"additional","affiliation":[{"name":"University of Ottawa, Ottawa, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,10,24]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"5th GI\/ITG KuVS Fachgespr\u00e4ch \"Drahtlose Sensornetze\".","author":"Aberer Karl","year":"2006","unstructured":"Karl Aberer , Manfred Hauswirth , and A\u00ed Salehi . 2006. Middleware support for the \"Internet of Things \". In 5th GI\/ITG KuVS Fachgespr\u00e4ch \"Drahtlose Sensornetze\". Universit\u00e4t Stuttgart , Germany , 15--20. https:\/\/elib.uni-stuttgart.de\/bitstream\/11682\/2604\/1\/TR_ 2006 _07.pdf Karl Aberer, Manfred Hauswirth, and A\u00ed Salehi. 2006. Middleware support for the \"Internet of Things\". In 5th GI\/ITG KuVS Fachgespr\u00e4ch \"Drahtlose Sensornetze\". Universit\u00e4t Stuttgart, Germany, 15--20. https:\/\/elib.uni-stuttgart.de\/bitstream\/11682\/2604\/1\/TR_2006_07.pdf"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.2753\/JEC1086-4415120401"},{"key":"e_1_3_2_1_3_1","unstructured":"Alireza Parvizimosaid. 2022. Supplementary online material. https:\/\/bit.ly\/MODELS22 See also https:\/\/github.com\/Smart-Contract-Modelling-uOttawa\/Symboleo-Compliance-Checker.  Alireza Parvizimosaid. 2022. Supplementary online material. https:\/\/bit.ly\/MODELS22 See also https:\/\/github.com\/Smart-Contract-Modelling-uOttawa\/Symboleo-Compliance-Checker."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.24251\/HICSS.2020.650"},{"key":"e_1_3_2_1_5_1","unstructured":"Pedro Antonino and A. W. Roscoe. 2020. Formalising and verifying smart contracts with Solidifier: a bounded model checker for Solidity. CoRR abs\/2002.02710 (2020) 24 pages. arXiv:2002.02710 https:\/\/arxiv.org\/abs\/2002.02710  Pedro Antonino and A. W. Roscoe. 2020. Formalising and verifying smart contracts with Solidifier: a bounded model checker for Solidity. CoRR abs\/2002.02710 (2020) 24 pages. arXiv:2002.02710 https:\/\/arxiv.org\/abs\/2002.02710"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-58603-929-5-825"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Roberto Cavada Alessandro Cimatti Andrea Micheli Marco Roveri Angelo Susi and Stefano Tonetta. 2011. OthelloPlay: a plug-in based tool for requirement formalization and validation. In TOPI@ICSE. ACM 59.  Roberto Cavada Alessandro Cimatti Andrea Micheli Marco Roveri Angelo Susi and Stefano Tonetta. 2011. OthelloPlay: a plug-in based tool for requirement formalization and validation. In TOPI@ICSE. ACM 59.","DOI":"10.1145\/1984708.1984728"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10458-012-9202-0"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_29"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2377656.2377659"},{"key":"e_1_3_2_1_12_1","volume-title":"Peled","author":"Clarke Edmund M.","year":"2001","unstructured":"Edmund M. Clarke , Orna Grumberg , and Doron A . Peled . 2001 . Model checking. MIT Press . http:\/\/books.google.de\/books?id=Nmc4wEaLXFEC Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 2001. Model checking. MIT Press. http:\/\/books.google.de\/books?id=Nmc4wEaLXFEC"},{"volume-title":"Logic-based tools for the analysis and representation of legal contracts. Ph. D. Dissertation","author":"Daskalopulu Aspassia-Kaliopi","key":"e_1_3_2_1_13_1","unstructured":"Aspassia-Kaliopi Daskalopulu . 1999. Logic-based tools for the analysis and representation of legal contracts. Ph. D. Dissertation . Imperial College London , UK. Aspassia-Kaliopi Daskalopulu. 1999. Logic-based tools for the analysis and representation of legal contracts. Ph. D. Dissertation. Imperial College London, UK."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/302405.302672"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(83)90017-5"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1613\/jair.1129"},{"key":"e_1_3_2_1_17_1","volume-title":"ETHBMC: A Bounded Model Checker for Smart Contracts. In 29th USENIX Security Symposium. USENIX Association, 2757--2774","author":"Frank Joel","year":"2020","unstructured":"Joel Frank , Cornelius Aschermann , and Thorsten Holz . 2020 . ETHBMC: A Bounded Model Checker for Smart Contracts. In 29th USENIX Security Symposium. USENIX Association, 2757--2774 . https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/frank Joel Frank, Cornelius Aschermann, and Thorsten Holz. 2020. ETHBMC: A Bounded Model Checker for Smart Contracts. In 29th USENIX Security Symposium. USENIX Association, 2757--2774. https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/frank"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00766-004-0191-7"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11837862_2"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-41600-3_11"},{"key":"e_1_3_2_1_21_1","volume-title":"Detecting Standard Violation Errors in Smart Contracts. CoRR abs\/1812.07702","author":"Li Ao","year":"2018","unstructured":"Ao Li and Fan Long . 2018. Detecting Standard Violation Errors in Smart Contracts. CoRR abs\/1812.07702 ( 2018 ), 17 pages. arXiv:1812.07702 http:\/\/arxiv.org\/abs\/1812.07702 Ao Li and Fan Long. 2018. Detecting Standard Violation Errors in Smart Contracts. CoRR abs\/1812.07702 (2018), 17 pages. arXiv:1812.07702 http:\/\/arxiv.org\/abs\/1812.07702"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2020.103369"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/COMPSAC.2019.10265"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14538-4"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-019-00339-1"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/Cybermatics_2018.2018.00185"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICBC48266.2020.9169428"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75596-8_8"},{"volume-title":"Conceptual Modeling","author":"Parvizimosaed Alireza","key":"e_1_3_2_1_30_1","unstructured":"Alireza Parvizimosaed , Sepehr Sharifi , Daniel Amyot , Luigi Logrippo , and John Mylopoulos . 2020. Subcontracting, Assignment, and Substitution for Legal Contracts in Symboleo . In Conceptual Modeling . Springer , Cham , 271--285. Alireza Parvizimosaed, Sepehr Sharifi, Daniel Amyot, Luigi Logrippo, and John Mylopoulos. 2020. Subcontracting, Assignment, and Substitution for Legal Contracts in Symboleo. In Conceptual Modeling. Springer, Cham, 271--285."},{"key":"e_1_3_2_1_31_1","volume-title":"Specification and Analysis of Legal Contracts with Symboleo. Software and Systems Modeling","author":"Parvizimosaed Alireza","year":"2022","unstructured":"Alireza Parvizimosaed , Sepehr Sharifi , Daniel Amyot , Luigi Logrippo , Marco Roveri , Aidin Rasti , Ali Roudak , and John Mylopoulos . 2022. Specification and Analysis of Legal Contracts with Symboleo. Software and Systems Modeling ( 2022 ). Under revision. Alireza Parvizimosaed, Sepehr Sharifi, Daniel Amyot, Luigi Logrippo, Marco Roveri, Aidin Rasti, Ali Roudak, and John Mylopoulos. 2022. Specification and Analysis of Legal Contracts with Symboleo. Software and Systems Modeling (2022). Under revision."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146909.1147119"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.future.2018.05.046"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0140-3"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-019-00337-w"},{"volume-title":"Artificial intelligence today","author":"Shanahan Murray","key":"e_1_3_2_1_36_1","unstructured":"Murray Shanahan . 1999. The event calculus explained . In Artificial intelligence today . Springer , 409--430. Murray Shanahan. 1999. The event calculus explained. In Artificial intelligence today. Springer, 409--430."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/RE48521.2020.00049"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1134\/S0361768819080164"},{"key":"e_1_3_2_1_39_1","volume-title":"Formalizing and securing relationships on public networks. First Monday 2, 9","author":"Szabo Nick","year":"1997","unstructured":"Nick Szabo . 1997. Formalizing and securing relationships on public networks. First Monday 2, 9 ( 1997 ). Nick Szabo. 1997. Formalizing and securing relationships on public networks. First Monday 2, 9 (1997)."},{"key":"e_1_3_2_1_40_1","unstructured":"The nuXmv team. 2020. The nuXmv symbolic model checker. https:\/\/nuxmv.fbk.eu  The nuXmv team. 2020. The nuXmv symbolic model checker. https:\/\/nuxmv.fbk.eu"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3425898.3426958"},{"key":"e_1_3_2_1_42_1","unstructured":"Palina Tolmach Yi Li Shang-Wei Lin Yang Liu and Zengxiang Li. 2020. A Survey of Smart Contract Formal Specification and Verification. https:\/\/arxiv.org\/abs\/2008.02712 arXiv:2008.02712.  Palina Tolmach Yi Li Shang-Wei Lin Yang Liu and Zengxiang Li. 2020. A Survey of Smart Contract Formal Specification and Verification. https:\/\/arxiv.org\/abs\/2008.02712 arXiv:2008.02712."},{"volume-title":"Practical model-based testing: a tools approach","author":"Utting Mark","key":"e_1_3_2_1_43_1","unstructured":"Mark Utting and Bruno Legeard . 2010. Practical model-based testing: a tools approach . Elsevier . Mark Utting and Bruno Legeard. 2010. Practical model-based testing: a tools approach. Elsevier."}],"event":{"name":"MODELS '22: ACM\/IEEE 25th International Conference on Model Driven Engineering Languages and Systems","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","Univ. of Montreal University of Montreal","IEEE CS"],"location":"Montreal Quebec Canada","acronym":"MODELS '22"},"container-title":["Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3550355.3552449","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3550355.3552449","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:08Z","timestamp":1750183688000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3550355.3552449"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,23]]},"references-count":43,"alternative-id":["10.1145\/3550355.3552449","10.1145\/3550355"],"URL":"https:\/\/doi.org\/10.1145\/3550355.3552449","relation":{},"subject":[],"published":{"date-parts":[[2022,10,23]]},"assertion":[{"value":"2022-10-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}