{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,31]],"date-time":"2025-12-31T12:22:22Z","timestamp":1767183742361,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":59,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,10,19]],"date-time":"2020-10-19T00:00:00Z","timestamp":1603065600000},"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":[[2020,10,19]]},"DOI":"10.1145\/3419804.3420263","type":"proceedings-article","created":{"date-parts":[[2020,10,18]],"date-time":"2020-10-18T10:23:21Z","timestamp":1603016601000},"page":"23-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Bounded Verification of State Machine Models"],"prefix":"10.1145","author":[{"given":"Nafiseh","family":"Kahani","sequence":"first","affiliation":[{"name":"Queen's University"}]},{"given":"James R.","family":"Cordy","sequence":"additional","affiliation":[{"name":"Queen's University"}]}],"member":"320","published-online":{"date-parts":[[2020,10,19]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-018-0665-6"},{"key":"e_1_3_2_2_2_1","first-page":"250","article-title":"Using UML for Modeling Complex Real-Time Systems,\" in Languages, Compilers, and Tools for Embedded Systems","author":"Selic B.","year":"1998","journal-title":"Springer"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-012-0261-0"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-012-0281-9"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-015-0484-y"},{"key":"e_1_3_2_2_7_1","unstructured":"\"Z3 \" https:\/\/github.com\/Z3Prover\/z3 2019 retrieved October 14 2019.  \"Z3 \" https:\/\/github.com\/Z3Prover\/z3 2019 retrieved October 14 2019."},{"key":"e_1_3_2_2_8_1","first-page":"260","volume-title":"Springer","author":"Ball T.","year":"2001"},{"key":"e_1_3_2_2_9_1","first-page":"168","article-title":"A tool for checking ANSI-C programs","author":"Clarke E.","year":"2004","journal-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"crossref","unstructured":"N. Kahani M. Bagherzadeh and J. R. Cordy \"Synthesis of state machine models \" in Proceedings of the ACM\/IEEE 23rd International Conference on Model Driven Engineering Languages and Systems 2020.  N. Kahani M. Bagherzadeh and J. R. Cordy \"Synthesis of state machine models \" in Proceedings of the ACM\/IEEE 23rd International Conference on Model Driven Engineering Languages and Systems 2020.","DOI":"10.1145\/3365438.3410936"},{"key":"e_1_3_2_2_11_1","first-page":"62","article-title":"Synthesis of loop-free programs","author":"Gulwani S.","year":"2011","journal-title":"PLDI"},{"key":"e_1_3_2_2_12_1","first-page":"31","article-title":"Exploiting hierarchy in the abstraction-based verification of statecharts using SMT solvers","author":"Czip\u00f3 B.","year":"2017","journal-title":"FESCA"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-013-0330-z"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-014-0399-z"},{"key":"e_1_3_2_2_15_1","first-page":"1","article-title":"Model checking and the state explosion problem,\" in LASER","author":"Clarke E. M.","year":"2011","journal-title":"Software Engineering"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_3_2_2_17_1","first-page":"389","volume-title":"Springer","author":"Kroening D.","year":"2014"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2005.138"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36209-6_39"},{"key":"e_1_3_2_2_20_1","unstructured":"IBM \"IBM RSARTE \" https:\/\/www.ibm.com\/developerworks\/downloads-\/r\/architect\/index.html 2019 retrieved October 14 2019.  IBM \"IBM RSARTE \" https:\/\/www.ibm.com\/developerworks\/downloads-\/r\/architect\/index.html 2019 retrieved October 14 2019."},{"key":"e_1_3_2_2_21_1","unstructured":"Eclipse \"Eclipse Papyrus for Real Time (Papyrus-RT) \" https:\/\/www.eclipse.org\/papyrus-rt 2019 retrieved March 19 2019.  Eclipse \"Eclipse Papyrus for Real Time (Papyrus-RT) \" https:\/\/www.eclipse.org\/papyrus-rt 2019 retrieved March 19 2019."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2020.3008850"},{"key":"e_1_3_2_2_23_1","unstructured":"G. D. Plotkin \"A structural approach to operational semantics \" 1981.  G. D. Plotkin \"A structural approach to operational semantics \" 1981."},{"key":"e_1_3_2_2_24_1","first-page":"768","volume-title":"Springer","author":"von der Beeck M.","year":"2006"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"crossref","unstructured":"B. K. Rosen M. N. Wegman and F. K. Zadeck \"Global value numbers and redundant computations \" in Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages 1988 pp. 12--27.  B. K. Rosen M. N. Wegman and F. K. Zadeck \"Global value numbers and redundant computations \" in Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages 1988 pp. 12--27.","DOI":"10.1145\/73560.73562"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:FORM.0000040025.89719.f3"},{"key":"e_1_3_2_2_27_1","first-page":"46","volume-title":"Springer","author":"Kolovos D. S.","year":"2008"},{"key":"e_1_3_2_2_28_1","unstructured":"Xtext \"Xtext \" http:\/\/www.eclipse.org\/Xtext 2019 retrieved October 14 2019.  Xtext \"Xtext \" http:\/\/www.eclipse.org\/Xtext 2019 retrieved October 14 2019."},{"key":"e_1_3_2_2_29_1","unstructured":"N. Kahani \"Synthesis and verification of models using satisfiability modulo theories \" Ph.D. dissertation Queen's University 2020.  N. Kahani \"Synthesis and verification of models using satisfiability modulo theories \" Ph.D. dissertation Queen's University 2020."},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"crossref","unstructured":"M. Bagherzadeh N. Hili and J. Dingel \"Model-level platform-independent debugging in the context of the model-driven development of real-time systems \" in 11th Joint Meeting on Foundations of Software Engineering 2017 pp. 419--430.  M. Bagherzadeh N. Hili and J. Dingel \"Model-level platform-independent debugging in the context of the model-driven development of real-time systems \" in 11th Joint Meeting on Foundations of Software Engineering 2017 pp. 419--430.","DOI":"10.1145\/3106237.3106278"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/358557.358572"},{"volume-title":"Wiley","year":"1999","author":"Magee J.","key":"e_1_3_2_2_32_1"},{"key":"e_1_3_2_2_33_1","unstructured":"M. Bagherzadeh \"Model-level debugging in the context of the model-driven development \" Ph.D. dissertation 2019.  M. Bagherzadeh \"Model-level debugging in the context of the model-driven development \" Ph.D. dissertation 2019."},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"crossref","unstructured":"J. Balasubramanian S. Tambe C. Lu A. Gokhale C. Gill and D. C. Schmidt \"Adaptive failover for real-time middleware with passive replication \" in 15th IEEE Symposium on Real-Time and Embedded Technology and Applications 2009 pp. 118--127.  J. Balasubramanian S. Tambe C. Lu A. Gokhale C. Gill and D. C. Schmidt \"Adaptive failover for real-time middleware with passive replication \" in 15th IEEE Symposium on Real-Time and Embedded Technology and Applications 2009 pp. 118--127.","DOI":"10.1109\/RTAS.2009.36"},{"key":"e_1_3_2_2_35_1","first-page":"12","volume-title":"IEEE Press","author":"Kahani N.","year":"2017"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.585156"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11219-007-9020-9"},{"key":"e_1_3_2_2_39_1","first-page":"180","volume-title":"IEEE","author":"Zhao Y.","year":"2004"},{"key":"e_1_3_2_2_40_1","first-page":"25","article-title":"A semantic model for the state machine in the unified modeling language","author":"Compton K.","year":"2000","journal-title":"Proceeding of Dynamic Behavior in UML Models: Semantic Questions"},{"key":"e_1_3_2_2_41_1","first-page":"320","volume-title":"Springer","author":"Jin Y.","year":"2002"},{"key":"e_1_3_2_2_42_1","first-page":"378","volume-title":"Springer","author":"Varr\u00f3 D.","year":"2002"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2008.06.030"},{"key":"e_1_3_2_2_44_1","first-page":"83","article-title":"Completeness and consistency analysis of UML statechart specifications","author":"Pap Z.","year":"2001","journal-title":"Proceedings IEEE Design and Diagnostics of Electronic Circuits and Systems Workshop"},{"key":"e_1_3_2_2_45_1","unstructured":"J. Lilius and I. P. Paltor \"vUML: A tool for verifying UML models \" in 14th IEEE International Conference on Automated Software Engineering 1999 pp. 255--258.  J. Lilius and I. P. Paltor \"vUML: A tool for verifying UML models \" in 14th IEEE International Conference on Automated Software Engineering 1999 pp. 255--258."},{"key":"e_1_3_2_2_46_1","first-page":"331","volume-title":"Springer","author":"Latella D.","year":"1999"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001659970003"},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-002-0012-8"},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.33"},{"key":"e_1_3_2_2_50_1","first-page":"59","article-title":"Model checking and code generation for UML state machines and collaborations","author":"Knapp A.","year":"2002","journal-title":"Proceedings 5th Wsh. Tools for System Design and Verification"},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.10.024"},{"key":"e_1_3_2_2_52_1","unstructured":"S. Meng Z. Naixiao and B. K. Aichernig \"The formal foundations in RSL for UML statechart diagrams \" 2004.  S. Meng Z. Naixiao and B. K. Aichernig \"The formal foundations in RSL for UML statechart diagrams \" 2004."},{"key":"e_1_3_2_2_53_1","first-page":"497","article-title":"A formal model of the UML metamodel: The UML state machine and its integrity constraints","author":"Kim S.-K.","year":"2002","journal-title":"International Conference of B and Z Users"},{"key":"e_1_3_2_2_54_1","first-page":"304","volume-title":"Springer","author":"Zurowska K.","year":"2013"},{"key":"e_1_3_2_2_56_1","first-page":"238","volume-title":"Models and Patterns. Springer","author":"Leue S.","year":"2008"},{"key":"e_1_3_2_2_57_1","first-page":"99","volume-title":"Springer","author":"Ramos R.","year":"2005"},{"key":"e_1_3_2_2_58_1","first-page":"1","article-title":"Verifying dynamic aspects of UML models,\" in 2011 Design","author":"Soeken M.","year":"2011","journal-title":"Automation & Test in Europe"},{"key":"e_1_3_2_2_59_1","doi-asserted-by":"crossref","unstructured":"N. Przigoda R. Wille and R. Drechsler \"Ground setting properties for an efficient translation of OCL in SMT-based model finding \" in Proceedings of the ACM\/IEEE 19th International Conference on Model Driven Engineering Languages and Systems 2016 pp. 261--271.  N. Przigoda R. Wille and R. Drechsler \"Ground setting properties for an efficient translation of OCL in SMT-based model finding \" in Proceedings of the ACM\/IEEE 19th International Conference on Model Driven Engineering Languages and Systems 2016 pp. 261--271.","DOI":"10.1145\/2976767.2976780"},{"key":"e_1_3_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2017.2777830"},{"key":"e_1_3_2_2_61_1","doi-asserted-by":"crossref","unstructured":"C. Dania and M. Clavel \"OCL2MSFOL: a mapping to many-sorted first-order logic for efficiently checking the satisfiability of OCL constraints \" in Proceedings of the ACM\/IEEE 19th International Conference on Model Driven Engineering Languages and Systems 2016 pp. 65--75.  C. Dania and M. Clavel \"OCL2MSFOL: a mapping to many-sorted first-order logic for efficiently checking the satisfiability of OCL constraints \" in Proceedings of the ACM\/IEEE 19th International Conference on Model Driven Engineering Languages and Systems 2016 pp. 65--75.","DOI":"10.1145\/2976767.2976774"}],"event":{"name":"SAM '20: 12th System Analysis and Modelling Conference","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"],"location":"Virtual Event Canada","acronym":"SAM '20"},"container-title":["Proceedings of the 12th System Analysis and Modelling Conference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3419804.3420263","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3419804.3420263","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:32:03Z","timestamp":1750195923000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3419804.3420263"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,10,19]]},"references-count":59,"alternative-id":["10.1145\/3419804.3420263","10.1145\/3419804"],"URL":"https:\/\/doi.org\/10.1145\/3419804.3420263","relation":{},"subject":[],"published":{"date-parts":[[2020,10,19]]},"assertion":[{"value":"2020-10-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}