{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:15:50Z","timestamp":1750220150211,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,11,29]],"date-time":"2022-11-29T00:00:00Z","timestamp":1669680000000},"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,11,29]]},"DOI":"10.1145\/3563822.3568014","type":"proceedings-article","created":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T21:17:50Z","timestamp":1669929470000},"page":"16-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Q: A Sound Verification Framework for Statecharts and Their Implementations"],"prefix":"10.1145","author":[{"given":"Samuel D.","family":"Pollard","sequence":"first","affiliation":[{"name":"Sandia National Laboratories, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert C.","family":"Armstrong","sequence":"additional","affiliation":[{"name":"Sandia National Laboratories, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Bender","sequence":"additional","affiliation":[{"name":"Sandia National Laboratories, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Geoffrey C.","family":"Hulette","sequence":"additional","affiliation":[{"name":"Sandia National Laboratories, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Raheel S.","family":"Mahmood","sequence":"additional","affiliation":[{"name":"Sandia National Laboratories, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Karla","family":"Morris","sequence":"additional","affiliation":[{"name":"Sandia National Laboratories, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Blake C.","family":"Rawlings","sequence":"additional","affiliation":[{"name":"Sandia National Laboratories, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jon M.","family":"Aytac","sequence":"additional","affiliation":[{"name":"Sandia National Laboratories, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,12]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0145-y"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542452.1542475"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_1"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.2016.0331"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/b96106"},{"key":"e_1_3_2_1_6_1","unstructured":"Jim Barnett Rahul Akolkar R. J. Auburn Michael Bodell Daniel C. Burnett Jerry Carter Scott McGlashan Torbj\u00f6rn Lager Mark Helbing Rafah Hosn T. V. Raman Klaus Reifenrath No\u2019am Rosenthal and Johan Roxendal. 2015. State Chart XML (SCXML): State Machine Notation for Control Abstraction. WC3: The World Wide Web Consortium. Available at https:\/\/www.w3.org\/TR\/scxml\/ \t\t\t\t  Jim Barnett Rahul Akolkar R. J. Auburn Michael Bodell Daniel C. Burnett Jerry Carter Scott McGlashan Torbj\u00f6rn Lager Mark Helbing Rafah Hosn T. V. Raman Klaus Reifenrath No\u2019am Rosenthal and Johan Roxendal. 2015. State Chart XML (SCXML): State Machine Notation for Control Abstraction. WC3: The World Wide Web Consortium. Available at https:\/\/www.w3.org\/TR\/scxml\/"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9148-3"},{"key":"e_1_3_2_1_8_1","unstructured":"Fran\u00e7ois Bobot Jean-Christophe Filli\u00e2tre Claude March\u00e9 and Andrei Paskevich. 2011. Why3: Shepherd Your Herd of Provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages. Wroc\u0142 aw Poland. 53\u201364.  https:\/\/hal.inria.fr\/hal-00790310 \t\t\t\t  Fran\u00e7ois Bobot Jean-Christophe Filli\u00e2tre Claude March\u00e9 and Andrei Paskevich. 2011. Why3: Shepherd Your Herd of Provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages. Wroc\u0142 aw Poland. 53\u201364.  https:\/\/hal.inria.fr\/hal-00790310"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90098-9"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14808-8_3"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_29"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_1"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39190"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19249-9_3"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69850-0_2"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_10"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_3_2_1_22_1","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","year":"2002","unstructured":"Leslie Lamport . 2002 . Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers . Addison-Wesley Longman Publishing Co., Inc. , Boston, MA, USA . isbn:032114306X Leslie Lamport. 2002. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA. isbn:032114306X"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.1993.274940"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"e_1_3_2_1_28_1","volume-title":"Stateflow: Model and Simulate Decision Logic Using State Machines and Flow Charts.","author":"MathWorks The","year":"2022","unstructured":"The MathWorks , Inc .. 2022 . Stateflow: Model and Simulate Decision Logic Using State Machines and Flow Charts. Available at https:\/\/www.mathworks.com\/products\/stateflow.html The MathWorks, Inc.. 2022. Stateflow: Model and Simulate Decision Logic Using State Machines and Flow Charts. Available at https:\/\/www.mathworks.com\/products\/stateflow.html"},{"key":"e_1_3_2_1_29_1","volume-title":"L\u00e9o Stefanesco, L\u00e9on Gondelman, Abel Nieto, and Lars Birkedal.","author":"Timany Amin","year":"2021","unstructured":"Amin Timany , Simon Oddershede Gregersen , L\u00e9o Stefanesco, L\u00e9on Gondelman, Abel Nieto, and Lars Birkedal. 2021 . Trillium : Unifying Refinement and Higher-Order Distributed Separation Logic . arXiv. Available at arxiv:2109.07863 Amin Timany, Simon Oddershede Gregersen, L\u00e9o Stefanesco, L\u00e9on Gondelman, Abel Nieto, and Lars Birkedal. 2021. Trillium: Unifying Refinement and Higher-Order Distributed Separation Logic. arXiv. Available at arxiv:2109.07863"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.32"}],"event":{"name":"FTSCS '22: 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Auckland New Zealand","acronym":"FTSCS '22"},"container-title":["Proceedings of the 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563822.3568014","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563822.3568014","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:00:07Z","timestamp":1750186807000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563822.3568014"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,11,29]]},"references-count":30,"alternative-id":["10.1145\/3563822.3568014","10.1145\/3563822"],"URL":"https:\/\/doi.org\/10.1145\/3563822.3568014","relation":{},"subject":[],"published":{"date-parts":[[2022,11,29]]},"assertion":[{"value":"2022-12-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}