{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T03:33:53Z","timestamp":1769744033086,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":61,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,10,16]],"date-time":"2020-10-16T00:00:00Z","timestamp":1602806400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,10,18]]},"DOI":"10.1145\/3365438.3410936","type":"proceedings-article","created":{"date-parts":[[2021,1,19]],"date-time":"2021-01-19T16:09:22Z","timestamp":1611072562000},"page":"274-284","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Synthesis of state machine models"],"prefix":"10.1145","author":[{"given":"Nafiseh","family":"Kahani","sequence":"first","affiliation":[{"name":"Queen's University, Canada"}]},{"given":"Mojtaba","family":"Bagherzadeh","sequence":"additional","affiliation":[{"name":"University of Ottawa, Canada"}]},{"given":"James R.","family":"Cordy","sequence":"additional","affiliation":[{"name":"Queen's University, Canada"}]}],"member":"320","published-online":{"date-parts":[[2020,10,16]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Classification of model transformation approaches,\" in Proceedings of the 2nd OOPSLA Workshop on Generative Techniques in the Context of the Model Driven Architecture","author":"Czarnecki K.","unstructured":"K. Czarnecki and S. Helsen , \" Classification of model transformation approaches,\" in Proceedings of the 2nd OOPSLA Workshop on Generative Techniques in the Context of the Model Driven Architecture , vol. 45 , no. 3, 2003, pp. 1--17. K. Czarnecki and S. Helsen, \"Classification of model transformation approaches,\" in Proceedings of the 2nd OOPSLA Workshop on Generative Techniques in the Context of the Model Driven Architecture, vol. 45, no. 3, 2003, pp. 1--17."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.10.021"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-018-0665-6"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-012-0261-0"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31847-7_18"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.21"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2005.138"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/381473.381494"},{"key":"e_1_3_2_1_10_1","first-page":"515","volume-title":"a domain-specific language for automatic modeling of real-time embedded systems,\" in 2018 IEEE\/ACM 40th International Conference on Software Engineering: Companion (ICSE-Companion)","author":"Kahani N.","year":"2018","unstructured":"N. Kahani , \"Automodel : a domain-specific language for automatic modeling of real-time embedded systems,\" in 2018 IEEE\/ACM 40th International Conference on Software Engineering: Companion (ICSE-Companion) , 2018 , pp. 515 -- 517 . N. Kahani, \"Automodel: a domain-specific language for automatic modeling of real-time embedded systems,\" in 2018 IEEE\/ACM 40th International Conference on Software Engineering: Companion (ICSE-Companion), 2018, pp. 515--517."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337217"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1656250.1656252"},{"key":"e_1_3_2_1_13_1","volume-title":"dissertation","author":"Rosner R.","year":"1992","unstructured":"R. Rosner , \"Modular synthesis of reactive systems,\" Ph. D. dissertation , 1992 . R. Rosner, \"Modular synthesis of reactive systems,\" Ph.D. dissertation, 1992."},{"key":"e_1_3_2_1_14_1","first-page":"592","volume-title":"Requirements modelling by synthesis of deontic input-output automata,\" in 2013 35th International Conference on Software Engineering (ICSE)","author":"Letier E.","year":"2013","unstructured":"E. Letier and W. Heaven , \" Requirements modelling by synthesis of deontic input-output automata,\" in 2013 35th International Conference on Software Engineering (ICSE) , 2013 , pp. 592 -- 601 . E. Letier and W. Heaven, \"Requirements modelling by synthesis of deontic input-output automata,\" in 2013 35th International Conference on Software Engineering (ICSE), 2013, pp. 592--601."},{"key":"e_1_3_2_1_15_1","first-page":"179","volume-title":"On the synthesis of a reactive module,\" in Proceedings of the 16th Symposium on Principles of Programming Languages","author":"Pnueli A.","year":"1989","unstructured":"A. Pnueli and R. Rosner , \" On the synthesis of a reactive module,\" in Proceedings of the 16th Symposium on Principles of Programming Languages , 1989 , pp. 179 -- 190 . A. Pnueli and R. Rosner, \"On the synthesis of a reactive module,\" in Proceedings of the 16th Symposium on Principles of Programming Languages, 1989, pp. 179--190."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00106"},{"issue":"1","key":"e_1_3_2_1_17_1","first-page":"2","article-title":"Foundations and trends in programming languages","volume":"4","author":"Gulwani S.","year":"2017","unstructured":"S. Gulwani , O. Polozov , and R. Singh , \" Foundations and trends in programming languages ,\" ACM Trans. Comput. Log. , vol. 4 , no. 1 -- 2 , pp. 1--119, 2017 . S. Gulwani, O. Polozov, and R. Singh, \"Foundations and trends in programming languages,\" ACM Trans. Comput. Log., vol. 4, no. 1--2, pp. 1--119, 2017.","journal-title":"ACM Trans. Comput. Log."},{"key":"e_1_3_2_1_18_1","first-page":"215","volume-title":"32nd Intl. Conf. on Software Engineering","author":"Jha S.","year":"2010","unstructured":"S. Jha , S. Gulwani , S. A. Seshia , and A. Tiwari , \" Oracle-guided component-based program synthesis,\" in Proc . 32nd Intl. Conf. on Software Engineering , 2010 , pp. 215 -- 224 . S. Jha, S. Gulwani, S. A. Seshia, and A. Tiwari, \"Oracle-guided component-based program synthesis,\" in Proc. 32nd Intl. Conf. on Software Engineering, 2010, pp. 215--224."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","first-page":"304","DOI":"10.1145\/512529.512566","article-title":"Denali: A goal-directed superoptimizer","author":"Joshi R.","year":"2002","unstructured":"R. Joshi , G. Nelson , and K. Randall , \" Denali: A goal-directed superoptimizer ,\" in PLDI , 2002 , pp. 304 -- 314 . R. Joshi, G. Nelson, and K. Randall, \"Denali: A goal-directed superoptimizer,\" in PLDI, 2002, pp. 304--314.","journal-title":"PLDI"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/1855741.1855754"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"B. Selic \"Using UML for modeling complex real-time systems \" in Languages Compilers and Tools for Embedded Systems 1998 pp. 250--260.  B. Selic \"Using UML for modeling complex real-time systems \" in Languages Compilers and Tools for Embedded Systems 1998 pp. 250--260.","DOI":"10.1007\/BFb0057795"},{"key":"e_1_3_2_1_22_1","volume-title":"retrieved","year":"2019","unstructured":"Eclipse Foundation, \"Eclipse Papyrus for Real Time (Papyrus-RT),\" https:\/\/www.eclipse.org\/papyrus-rt, 2019 , retrieved March 19, 2019 . Eclipse Foundation, \"Eclipse Papyrus for Real Time (Papyrus-RT),\" https:\/\/www.eclipse.org\/papyrus-rt, 2019, retrieved March 19, 2019."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/3104068.3104074"},{"key":"e_1_3_2_1_24_1","volume-title":"UMLRTSynthesizer,\" https:\/\/github.com\/nafisehka\/UMLRTSynthesizer","author":"Kahani N.","year":"2020","unstructured":"N. Kahani , M. Bagherzadeh , and J. Cordy , \" UMLRTSynthesizer,\" https:\/\/github.com\/nafisehka\/UMLRTSynthesizer , 2020 . N. Kahani, M. Bagherzadeh, and J. Cordy, \"UMLRTSynthesizer,\" https:\/\/github.com\/nafisehka\/UMLRTSynthesizer, 2020."},{"key":"e_1_3_2_1_25_1","volume-title":"retrieved","author":"IBM","year":"2019","unstructured":"IBM, \" IBM RSARTE,\" 2016 , retrieved July 19, 2019 . [Online]. Available: https:\/\/www.ibm.com\/developerworks\/downloads\/r\/architect\/index.html IBM, \"IBM RSARTE,\" 2016, retrieved July 19, 2019. [Online]. Available: https:\/\/www.ibm.com\/developerworks\/downloads\/r\/architect\/index.html"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181800"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/2103603"},{"key":"e_1_3_2_1_28_1","volume-title":"Distributed algorithms","author":"Lynch N. A.","year":"1996","unstructured":"N. A. Lynch , Distributed algorithms . Elsevier , 1996 . N. A. Lynch, Distributed algorithms. Elsevier, 1996."},{"key":"e_1_3_2_1_29_1","unstructured":"\"Z3 \" https:\/\/github.com\/Z3Prover\/z3.  \"Z3 \" https:\/\/github.com\/Z3Prover\/z3."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69927-9_4"},{"key":"e_1_3_2_1_31_1","volume-title":"Xtext. [Online]. Available: http:\/\/www.eclipse.org\/Xtext","year":"2017","unstructured":"Xtext. ( 2017 ) Xtext. [Online]. Available: http:\/\/www.eclipse.org\/Xtext . Xtext. (2017) Xtext. [Online]. Available: http:\/\/www.eclipse.org\/Xtext."},{"key":"e_1_3_2_1_32_1","volume-title":"Eclipse Modeling Framework (EMF). [Online]. Available: https:\/\/www.eclipse.org\/modeling\/emf","author":"EMF.","year":"2017","unstructured":"EMF. ( 2017 ) Eclipse Modeling Framework (EMF). [Online]. Available: https:\/\/www.eclipse.org\/modeling\/emf . EMF. (2017) Eclipse Modeling Framework (EMF). [Online]. Available: https:\/\/www.eclipse.org\/modeling\/emf."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1178048"},{"key":"e_1_3_2_1_34_1","first-page":"49","volume-title":"Synthesis of state machines from multiple interrelated scenarios using dependency diagrams,\" in In 8th World Multiconf. on systemics, cybernetics and informatics","author":"Vasilache S.","year":"2004","unstructured":"S. Vasilache and J. Tanaka , \" Synthesis of state machines from multiple interrelated scenarios using dependency diagrams,\" in In 8th World Multiconf. on systemics, cybernetics and informatics , 2004 , pp. 49 -- 54 . S. Vasilache and J. Tanaka, \"Synthesis of state machines from multiple interrelated scenarios using dependency diagrams,\" in In 8th World Multiconf. on systemics, cybernetics and informatics, 2004, pp. 49--54."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71289-3_8"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.14257\/ijseia.2015.9.9.08"},{"key":"e_1_3_2_1_37_1","first-page":"305","volume-title":"7th Joint Meeting on Foundations of Software Engineering","author":"Krka I.","year":"2009","unstructured":"I. Krka , Y. Brun , G. Edwards , and N. Medvidovic , \" Synthesizing partial component-level behavior models from system specifications,\" in Proc . 7th Joint Meeting on Foundations of Software Engineering , 2009 , pp. 305 -- 314 . I. Krka, Y. Brun, G. Edwards, and N. Medvidovic, \"Synthesizing partial component-level behavior models from system specifications,\" in Proc. 7th Joint Meeting on Foundations of Software Engineering, 2009, pp. 305--314."},{"key":"e_1_3_2_1_38_1","volume-title":"dissertation","author":"Kahani N.","year":"2020","unstructured":"N. Kahani , \"Synthesis and verification of models using satisfiability modulo theories,\" Ph. D. dissertation , 2020 . N. Kahani, \"Synthesis and verification of models using satisfiability modulo theories,\" Ph.D. dissertation, 2020."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"e_1_3_2_1_40_1","first-page":"468","volume-title":"36th Intl. Conf. on Software Engineering","author":"Beschastnikh I.","year":"2014","unstructured":"I. Beschastnikh , Y. Brun , M. D. Ernst , and A. Krishnamurthy , \" Inferring models of concurrent systems from logs of their behavior with CSight,\" in Proc . 36th Intl. Conf. on Software Engineering , 2014 , pp. 468 -- 479 . I. Beschastnikh, Y. Brun, M. D. Ernst, and A. Krishnamurthy, \"Inferring models of concurrent systems from logs of their behavior with CSight,\" in Proc. 36th Intl. Conf. on Software Engineering, 2014, pp. 468--479."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2017.2670146"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-015-9367-7"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-35570-2_5"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054102000935"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2967606"},{"key":"e_1_3_2_1_46_1","first-page":"1","article-title":"Trace theory for automatic hierarchical verification of speed independent circuits","volume":"24","author":"Dill D.","year":"1989","unstructured":"D. Dill , \" Trace theory for automatic hierarchical verification of speed independent circuits ,\" MA: MIT press , vol. 24 , pp. 1 -- 180 , 1989 . D. Dill, \"Trace theory for automatic hierarchical verification of speed independent circuits,\" MA: MIT press, vol. 24, pp. 1--180, 1989.","journal-title":"MA: MIT press"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/963927.963928"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/11817963_6","volume-title":"Safraless compositional synthesis,\" in Computer Aided Verification (CAV)","author":"Kupferman N. P. O.","year":"2006","unstructured":"N. P. O. Kupferman and M. Vardi , \" Safraless compositional synthesis,\" in Computer Aided Verification (CAV) , 2006 , pp. 31 -- 44 . N. P. O. Kupferman and M. Vardi, \"Safraless compositional synthesis,\" in Computer Aided Verification (CAV), 2006, pp. 31--44."},{"key":"e_1_3_2_1_49_1","first-page":"221","volume-title":"Correct-by-construction control synthesis for multi-robot mixing,\" in 54th IEEE Conf. on Decision and Control (CDC)","author":"Diaz-Mercado Y.","year":"2015","unstructured":"Y. Diaz-Mercado , A. Jones , C. Belta , and M. Egerstedt , \" Correct-by-construction control synthesis for multi-robot mixing,\" in 54th IEEE Conf. on Decision and Control (CDC) , 2015 , pp. 221 -- 226 . Y. Diaz-Mercado, A. Jones, C. Belta, and M. Egerstedt, \"Correct-by-construction control synthesis for multi-robot mixing,\" in 54th IEEE Conf. on Decision and Control (CDC), 2015, pp. 221--226."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2009.2030225"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2018.02.021"},{"key":"e_1_3_2_1_52_1","first-page":"62","article-title":"Synthesis of loop-free programs","author":"Gulwani S.","year":"2011","unstructured":"S. Gulwani , S. Jha , A. Tiwari , and R. Venkatesan , \" Synthesis of loop-free programs ,\" in PLDI , 2011 , pp. 62 -- 73 . S. Gulwani, S. Jha, A. Tiwari, and R. Venkatesan, \"Synthesis of loop-free programs,\" in PLDI, 2011, pp. 62--73.","journal-title":"PLDI"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168918.1168907"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544173.2509555"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_12"},{"key":"e_1_3_2_1_56_1","first-page":"7434","volume-title":"Controller synthesis with inductive proofs for piecewise linear systems: An SMT-based algorithm,\" in 54th IEEE Conf. on decision and control (CDC)","author":"Huang Z.","year":"2015","unstructured":"Z. Huang , Y. Wang , S. Mitra , G. E. Dullerud , and S. Chaudhuri , \" Controller synthesis with inductive proofs for piecewise linear systems: An SMT-based algorithm,\" in 54th IEEE Conf. on decision and control (CDC) , 2015 , pp. 7434 -- 7439 . Z. Huang, Y. Wang, S. Mitra, G. E. Dullerud, and S. Chaudhuri, \"Controller synthesis with inductive proofs for piecewise linear systems: An SMT-based algorithm,\" in 54th IEEE Conf. on decision and control (CDC), 2015, pp. 7434--7439."},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/1707801.1706337"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1932682.1869463"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_67"},{"key":"e_1_3_2_1_60_1","first-page":"4","article-title":"The sketching approach to program synthesis","author":"Solar-Lezama A.","year":"2009","unstructured":"A. Solar-Lezama , \" The sketching approach to program synthesis ,\" in Asian Symp. on Programming Languages and Systems , 2009 , pp. 4 -- 13 . A. Solar-Lezama, \"The sketching approach to program synthesis,\" in Asian Symp. on Programming Languages and Systems, 2009, pp. 4--13.","journal-title":"Asian Symp. on Programming Languages and Systems"},{"key":"e_1_3_2_1_61_1","first-page":"1178","volume-title":"IEEE","author":"Bagherzadeh M.","year":"2019","unstructured":"M. Bagherzadeh , N. Kahani , J. Karim , and J. Dingel , \" PMExec: An execution engine of partial UML-RT models,\" in 2019 34th IEEE\/ACM International Conference on Automated Software Engineering (ASE) . IEEE , 2019 , pp. 1178 -- 1181 . M. Bagherzadeh, N. Kahani, J. Karim, and J. Dingel, \"PMExec: An execution engine of partial UML-RT models,\" in 2019 34th IEEE\/ACM International Conference on Automated Software Engineering (ASE). IEEE, 2019, pp. 1178--1181."},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2020.3008850"}],"event":{"name":"MODELS '20: ACM\/IEEE 23rd International Conference on Model Driven Engineering Languages and Systems","location":"Virtual Event Canada","acronym":"MODELS '20","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"]},"container-title":["Proceedings of the 23rd ACM\/IEEE International Conference on Model Driven Engineering Languages and Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3365438.3410936","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3365438.3410936","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T17:49:49Z","timestamp":1750268989000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3365438.3410936"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,10,16]]},"references-count":61,"alternative-id":["10.1145\/3365438.3410936","10.1145\/3365438"],"URL":"https:\/\/doi.org\/10.1145\/3365438.3410936","relation":{},"subject":[],"published":{"date-parts":[[2020,10,16]]},"assertion":[{"value":"2020-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}