{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,28]],"date-time":"2025-11-28T17:20:47Z","timestamp":1764350447269,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":11,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,9,3]],"date-time":"2018-09-03T00:00:00Z","timestamp":1535932800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001871","name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","doi-asserted-by":"publisher","award":["POCI-01-0145-FEDER-016826"],"award-info":[{"award-number":["POCI-01-0145-FEDER-016826"]}],"id":[{"id":"10.13039\/501100001871","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100005304","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["FORMEDICIS ANR-16-CE25-0007"],"award-info":[{"award-number":["FORMEDICIS ANR-16-CE25-0007"]}],"id":[{"id":"10.13039\/501100005304","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,9,3]]},"DOI":"10.1145\/3238147.3240475","type":"proceedings-article","created":{"date-parts":[[2018,8,20]],"date-time":"2018-08-20T20:04:36Z","timestamp":1534795476000},"page":"884-887","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":24,"title":["The electrum analyzer: model checking relational first-order temporal specifications"],"prefix":"10.1145","author":[{"given":"Julien","family":"Brunel","sequence":"first","affiliation":[{"name":"ONERA, France \/ University of Toulouse, France"}]},{"given":"David","family":"Chemouil","sequence":"additional","affiliation":[{"name":"ONERA, France \/ University of Toulouse, France"}]},{"given":"Alcino","family":"Cunha","sequence":"additional","affiliation":[{"name":"INESC TEC, Portugal \/ University of Minho, Portugal"}]},{"given":"Nuno","family":"Macedo","sequence":"additional","affiliation":[{"name":"INESC TEC, Portugal \/ University of Minho, Portugal"}]}],"member":"320","published-online":{"date-parts":[[2018,9,3]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"ABZ (LNCS)","volume":"10817","author":"Brunel J.","unstructured":"J. Brunel , D. Chemouil , A. Cunha , T. Hujsa , N. Macedo , and J. Tawa . 2018. Proposition of an Action Layer for Electrum . In ABZ (LNCS) , Vol. 10817 . Springer, 397\u2013402. J. Brunel, D. Chemouil, A. Cunha, T. Hujsa, N. Macedo, and J. Tawa. 2018. Proposition of an Action Layer for Electrum. In ABZ (LNCS), Vol. 10817. Springer, 397\u2013402."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"e_1_3_2_1_3_1","volume-title":"ABZ (LNCS)","volume":"10817","author":"Cunha A.","unstructured":"A. Cunha and N. Macedo . 2018. Validating the Hybrid ERTMS\/ETCS Level 3 Concept with Electrum . In ABZ (LNCS) , Vol. 10817 . Springer, 307\u2013321. A. Cunha and N. Macedo. 2018. Validating the Hybrid ERTMS\/ETCS Level 3 Concept with Electrum. In ABZ (LNCS), Vol. 10817. Springer, 307\u2013321."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54804-8_2"},{"key":"e_1_3_2_1_5_1","volume-title":"Software Abstractions: Logic, Language, and Analysis (revised ed.)","author":"Jackson D.","year":"2012","unstructured":"D. Jackson . 2012 . Software Abstractions: Logic, Language, and Analysis (revised ed.) . MIT Press . D. Jackson. 2012. Software Abstractions: Logic, Language, and Analysis (revised ed.). MIT Press."},{"volume-title":"The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport L.","key":"e_1_3_2_1_6_1","unstructured":"L. Lamport . 2002. Specifying Systems , The TLA+ Language and Tools for Hardware and Software Engineers . Addison-Wesley . L. Lamport. 2002. Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950318"},{"key":"e_1_3_2_1_8_1","volume-title":"Exploring Scenario Exploration. In FASE (LNCS)","volume":"9033","author":"Macedo N.","unstructured":"N. Macedo , A. Cunha , and T. Guimar\u00e3es . 2015 . Exploring Scenario Exploration. In FASE (LNCS) , Vol. 9033 . Springer, 301\u2013315. N. Macedo, A. Cunha, and T. Guimar\u00e3es. 2015. Exploring Scenario Exploration. In FASE (LNCS), Vol. 9033. Springer, 301\u2013315."},{"key":"e_1_3_2_1_9_1","volume-title":"Exploiting Partial Knowledge for Efficient Model Analysis. In ATVA (LNCS)","volume":"10482","author":"Macedo N.","unstructured":"N. Macedo , A. Cunha , and E. Pessoa . 2017 . Exploiting Partial Knowledge for Efficient Model Analysis. In ATVA (LNCS) , Vol. 10482 . Springer, 344\u2013362. N. Macedo, A. Cunha, and E. Pessoa. 2017. Exploiting Partial Knowledge for Efficient Model Analysis. In ATVA (LNCS), Vol. 10482. Springer, 344\u2013362."},{"volume-title":"Symbolic Model Checking","author":"McMillan K. L.","key":"e_1_3_2_1_10_1","unstructured":"K. L. McMillan . 1993. Symbolic Model Checking . Kluwer . K. L. McMillan. 1993. Symbolic Model Checking. Kluwer."},{"key":"e_1_3_2_1_11_1","volume-title":"Kodkod: A Relational Model Finder. In TACAS (LNCS)","author":"Torlak E.","year":"2007","unstructured":"E. Torlak and D. Jackson . 2007 . Kodkod: A Relational Model Finder. In TACAS (LNCS) , Vol. 4424 . Springer , 632\u2013647. Abstract 1 Introduction 2 Electrum Specifications 3 Model Validation 4 Model Verification 5 Evaluation Acknowledgments References E. Torlak and D. Jackson. 2007. Kodkod: A Relational Model Finder. In TACAS (LNCS), Vol. 4424. Springer, 632\u2013647. Abstract 1 Introduction 2 Electrum Specifications 3 Model Validation 4 Model Verification 5 Evaluation Acknowledgments References"}],"event":{"name":"ASE '18: 33rd ACM\/IEEE International Conference on Automated Software Engineering","sponsor":["SIGAI ACM Special Interest Group on Artificial Intelligence","CNRS Centre National De La Rechercue Scientifique","SIGSOFT ACM Special Interest Group on Software Engineering","IEEE-CS Computer Society"],"location":"Montpellier France","acronym":"ASE '18"},"container-title":["Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3238147.3240475","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3238147.3240475","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:39:40Z","timestamp":1750210780000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3238147.3240475"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9,3]]},"references-count":11,"alternative-id":["10.1145\/3238147.3240475","10.1145\/3238147"],"URL":"https:\/\/doi.org\/10.1145\/3238147.3240475","relation":{},"subject":[],"published":{"date-parts":[[2018,9,3]]},"assertion":[{"value":"2018-09-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}