{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:25:33Z","timestamp":1750220733649,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":48,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,10,5]],"date-time":"2020-10-05T00:00:00Z","timestamp":1601856000000},"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,5]]},"DOI":"10.1145\/3382494.3410674","type":"proceedings-article","created":{"date-parts":[[2020,10,23]],"date-time":"2020-10-23T16:59:24Z","timestamp":1603472364000},"page":"1-11","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Understanding The Impact of Solver Choice in Model-Based Test Generation"],"prefix":"10.1145","author":[{"given":"Ying","family":"Meng","sequence":"first","affiliation":[{"name":"University of South Carolina, Columbia, SC, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gregory","family":"Gay","sequence":"additional","affiliation":[{"name":"Chalmers and the University of Gothenburg, Gothenburg, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,10,23]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Optimization of machining techniques --- A retrospective and literature review. Sadhana 30, 6 (01","author":"Aggarwal Aman","year":"2005","unstructured":"Aman Aggarwal and Hari Singh . 2005. Optimization of machining techniques --- A retrospective and literature review. Sadhana 30, 6 (01 Dec 2005 ), 699--711. https:\/\/doi.org\/10.1007\/BF02716704 10.1007\/BF02716704 Aman Aggarwal and Hari Singh. 2005. Optimization of machining techniques --- A retrospective and literature review. Sadhana 30, 6 (01 Dec 2005), 699--711. https:\/\/doi.org\/10.1007\/BF02716704"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/AICCSA.2010.5586985"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST46399.2020.00017"},{"volume-title":"Proceedings of the Sixth Int'l Conf. on the Theory and Applications of Satisfiability Testing.","author":"Alsinet T.","key":"e_1_3_2_1_4_1","unstructured":"T. Alsinet , F. Manya , and J. Planes . 2003. Improved Branch and Bound Algorithms for MAX-SAT . In Proceedings of the Sixth Int'l Conf. on the Theory and Applications of Satisfiability Testing. T. Alsinet, F. Manya, and J. Planes. 2003. Improved Branch and Bound Algorithms for MAX-SAT. In Proceedings of the Sixth Int'l Conf. on the Theory and Applications of Satisfiability Testing."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.83"},{"volume-title":"Search Based Software Engineering, Myra B. Cohen and Mel \u00d3 Cinn\u00e9ide (Eds.)","author":"Arcuri Andrea","key":"e_1_3_2_1_6_1","unstructured":"Andrea Arcuri and Gordon Fraser . 2011. On Parameter Tuning in Search Based Software Engineering . In Search Based Software Engineering, Myra B. Cohen and Mel \u00d3 Cinn\u00e9ide (Eds.) . Springer Berlin Heidelberg , Berlin, Heidelberg , 33--47. Andrea Arcuri and Gordon Fraser. 2011. On Parameter Tuning in Search Based Software Engineering. In Search Based Software Engineering, Myra B. Cohen and Mel \u00d3 Cinn\u00e9ide (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 33--47."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032319"},{"key":"e_1_3_2_1_8_1","unstructured":"A. Biere M. Heule H. van Maaren and T. Walsh. 2009. Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications. IOS Press Amsterdam The Netherlands The Netherlands.  A. Biere M. Heule H. van Maaren and T. Walsh. 2009. Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications. IOS Press Amsterdam The Netherlands The Netherlands."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"e_1_3_2_1_11_1","volume-title":"STG: A Symbolic Test Generation Tool. In Tools and Algorithms for the Construction and Analysis of Systems, Joost-Pieter Katoen and Perdita Stevens (Eds.)","author":"Clarke Duncan","year":"2002","unstructured":"Duncan Clarke , Thierry J\u00e9ron , Vlad Rusu , and Elena Zinovieva . 2002 . STG: A Symbolic Test Generation Tool. In Tools and Algorithms for the Construction and Analysis of Systems, Joost-Pieter Katoen and Perdita Stevens (Eds.) . Springer Berlin Heidelberg, Berlin , Heidelberg , 470--475. Duncan Clarke, Thierry J\u00e9ron, Vlad Rusu, and Elena Zinovieva. 2002. STG: A Symbolic Test Generation Tool. In Tools and Algorithms for the Construction and Analysis of Systems, Joost-Pieter Katoen and Perdita Stevens (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 470--475."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1077288.1077289"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Moura Leonardo De","key":"e_1_3_2_1_14_1","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner . 2008. Z3: An efficient SMT solver . In Tools and Algorithms for the Construction and Analysis of Systems . Springer , 337--340. Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems. Springer, 337--340."},{"volume-title":"Computer-Aided Verification (CAV'2014) (Lecture Notes in Computer Science)","author":"Dutertre Bruno","key":"e_1_3_2_1_15_1","unstructured":"Bruno Dutertre . 2014. Yices 2.2. In Computer-Aided Verification (CAV'2014) (Lecture Notes in Computer Science) , Armin Biere and Roderick Bloem (Eds.), Vol. 8559 . Springer , 737--744. Bruno Dutertre. 2014. Yices 2.2. In Computer-Aided Verification (CAV'2014) (Lecture Notes in Computer Science), Armin Biere and Roderick Bloem (Eds.), Vol. 8559. Springer, 737--744."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.swevo.2011.02.001"},{"key":"e_1_3_2_1_17_1","unstructured":"Esterel-Technologies. 2004. SCADE Suite Product Description. http:\/\/www.esterel-technologies.com\/v2\/ scadeSuiteForSafetyCriticalSoft-wareDevelopment\/index.html.  Esterel-Technologies. 2004. SCADE Suite Product Description. http:\/\/www.esterel-technologies.com\/v2\/ scadeSuiteForSafetyCriticalSoft-wareDevelopment\/index.html."},{"key":"e_1_3_2_1_18_1","volume-title":"An Empirical Analysis of the Mutation Operator for Run-Time Adaptive Testing in Self-Adaptive Systems. In 2018 IEEE\/ACM 11th International Workshop on Search-Based Software Testing (SBST). 59--66","author":"Fredericks E. M.","year":"2018","unstructured":"E. M. Fredericks . 2018 . An Empirical Analysis of the Mutation Operator for Run-Time Adaptive Testing in Self-Adaptive Systems. In 2018 IEEE\/ACM 11th International Workshop on Search-Based Software Testing (SBST). 59--66 . E. M. Fredericks. 2018. An Empirical Analysis of the Mutation Operator for Run-Time Adaptive Testing in Self-Adaptive Systems. In 2018 IEEE\/ACM 11th International Workshop on Search-Based Software Testing (SBST). 59--66."},{"key":"e_1_3_2_1_19_1","unstructured":"Andrew Gacek. 2015. JKind - a Java implementation of the KIND model checker. https:\/\/github.com\/agacek.  Andrew Gacek. 2015. JKind - a Java implementation of the KIND model checker. https:\/\/github.com\/agacek."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/318774.318939"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934672"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2016.2615311"},{"key":"e_1_3_2_1_23_1","first-page":"1","article-title":"Automated Oracle Data Selection Support. Software Engineering","volume":"99","author":"Gay G.","year":"2015","unstructured":"G. Gay , M. Staats , M. Whalen , and M. Heimdahl . 2015 . Automated Oracle Data Selection Support. Software Engineering , IEEE Transactions on PP , 99 (2015), 1 -- 1 . https:\/\/doi.org\/10.1109\/TSE.2015.2436920 10.1109\/TSE.2015.2436920 G. Gay, M. Staats, M. Whalen, and M. Heimdahl. 2015. Automated Oracle Data Selection Support. Software Engineering, IEEE Transactions on PP, 99 (2015), 1--1. https:\/\/doi.org\/10.1109\/TSE.2015.2436920","journal-title":"IEEE Transactions on PP"},{"key":"e_1_3_2_1_24_1","volume-title":"The Risks of Coverage-Directed Test Case Generation. Software Engineering","author":"Gay G.","year":"2015","unstructured":"G. Gay , M. Staats , M. Whalen , and M.P.E. Heimdahl . 2015. The Risks of Coverage-Directed Test Case Generation. Software Engineering , IEEE Transactions on PP , 99 ( 2015 ). https:\/\/doi.org\/10.1109\/TSE.2015.2421011 10.1109\/TSE.2015.2421011 G. Gay, M. Staats, M. Whalen, and M.P.E. Heimdahl. 2015. The Risks of Coverage-Directed Test Case Generation. Software Engineering, IEEE Transactions on PP, 99 (2015). https:\/\/doi.org\/10.1109\/TSE.2015.2421011"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3239372.3239409"},{"volume-title":"Synchronous Programming of Reactive Systems","author":"Halbwachs N.","key":"e_1_3_2_1_27_1","unstructured":"N. Halbwachs . 1993. Synchronous Programming of Reactive Systems . Klower Academic Press . N. Halbwachs. 1993. Synchronous Programming of Reactive Systems. Klower Academic Press."},{"key":"e_1_3_2_1_28_1","volume-title":"Proceedings of the 18th International Software Product Line Conference -","volume":"1","author":"Harman M.","unstructured":"M. Harman , Y. Jia , J. Krinke , W. B. Langdon , J. Petke , and Y. Zhang . 2014. Search Based Software Engineering for Software Product Line Engineering: A Survey and Directions for Future Work . In Proceedings of the 18th International Software Product Line Conference - Volume 1 (SPLC '14). ACM, New York, NY, USA, 5--18. https:\/\/doi.org\/10.1145\/2648511.2648513 10.1145\/2648511.2648513 M. Harman, Y. Jia, J. Krinke, W. B. Langdon, J. Petke, and Y. Zhang. 2014. Search Based Software Engineering for Software Product Line Engineering: A Survey and Directions for Future Work. In Proceedings of the 18th International Software Product Line Conference - Volume 1 (SPLC '14). ACM, New York, NY, USA, 5--18. https:\/\/doi.org\/10.1145\/2648511.2648513"},{"volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, Joost-Pieter Katoen and Perdita Stevens (Eds.)","author":"Hong Hyoung Seok","key":"e_1_3_2_1_29_1","unstructured":"Hyoung Seok Hong , Insup Lee , Oleg Sokolsky , and Hasan Ural . 2002. A Temporal Logic Based Theory of Test Coverage and Generation . In Tools and Algorithms for the Construction and Analysis of Systems, Joost-Pieter Katoen and Perdita Stevens (Eds.) . Springer Berlin Heidelberg, Berlin , Heidelberg , 327--341. Hyoung Seok Hong, Insup Lee, Oleg Sokolsky, and Hasan Ural. 2002. A Temporal Logic Based Theory of Test Coverage and Generation. In Tools and Algorithms for the Construction and Analysis of Systems, Joost-Pieter Katoen and Perdita Stevens (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 327--341."},{"key":"e_1_3_2_1_30_1","volume-title":"Computer Science: Modeling and Reasoning about Systems","author":"Huth M.","year":"2006","unstructured":"M. Huth and M. Ryan . 2006 . Logic in Computer Science: Modeling and Reasoning about Systems , Second Edition. Cambridge Press . M. Huth and M. Ryan. 2006. Logic in Computer Science: Modeling and Reasoning about Systems, Second Edition. Cambridge Press."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568271"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2015.71"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2635868.2635929"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2012.08.024"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1072997.1072998"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.533956"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/1077276.1077279"},{"key":"#cr-split#-e_1_3_2_1_38_1.1","unstructured":"Y. Meng G. Gay and M. Whalen. 2018. Ensuring the Observability of Structural Test Obligations. IEEE Transactions on Software Engineering (2018) 1--1. https:\/\/doi.org\/10.1109\/TSE.2018.2869146 Available at http:\/\/greggay.com\/pdf\/18omcdc.pdf. 10.1109\/TSE.2018.2869146"},{"key":"#cr-split#-e_1_3_2_1_38_1.2","doi-asserted-by":"crossref","unstructured":"Y. Meng G. Gay and M. Whalen. 2018. Ensuring the Observability of Structural Test Obligations. IEEE Transactions on Software Engineering (2018) 1--1. https:\/\/doi.org\/10.1109\/TSE.2018.2869146 Available at http:\/\/greggay.com\/pdf\/18omcdc.pdf.","DOI":"10.1109\/TSE.2018.2869146"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCPS.2014.6843718"},{"key":"e_1_3_2_1_40_1","unstructured":"Jeff Offutt Shaoying Liu Aynur Abdurazik and Paul Ammann. [n.d.]. Generating test data from state-based specifications. Software Testing Verification and Reliability 13 1 ([n.d.]) 25--53. https:\/\/doi.org\/10.1002\/stvr.264 arXiv:https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/stvr.264    10.1002\/stvr.264\nJeff Offutt Shaoying Liu Aynur Abdurazik and Paul Ammann. [n.d.]. Generating test data from state-based specifications. Software Testing Verification and Reliability 13 1 ([n.d.]) 25--53. https:\/\/doi.org\/10.1002\/stvr.264 arXiv:https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/stvr.264"},{"key":"e_1_3_2_1_41_1","unstructured":"M. Qasem. [n.d.]. SAT and MAX-SAT for the Lay-Researcher. ([n.d.]). Available at http:\/\/www.mqasem.net\/sat\/sat\/index.php.  M. Qasem. [n.d.]. SAT and MAX-SAT for the Lay-Researcher. ([n.d.]). Available at http:\/\/www.mqasem.net\/sat\/sat\/index.php."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"crossref","unstructured":"A. Rajan M. Whalen M. Staats and M.P. Heimdahl. 2008. Requirements Coverage as an Adequacy Measure for Conformance Testing. (2008) 86--104.  A. Rajan M. Whalen M. Staats and M.P. Heimdahl. 2008. Requirements Coverage as an Adequacy Measure for Conformance Testing. (2008) 86--104.","DOI":"10.1007\/978-3-540-88194-0_8"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/ECBS.2001.922409"},{"key":"e_1_3_2_1_44_1","unstructured":"RTCA\/DO-178C. [n.d.]. Software Considerations in Airborne Systems and Equipment Certification.  RTCA\/DO-178C. [n.d.]. Software Considerations in Airborne Systems and Equipment Certification."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.456"},{"volume-title":"Proceedings of the 2013 Int'l Conf. on Software Engineering. ACM.","author":"Whalen M.","key":"e_1_3_2_1_46_1","unstructured":"M. Whalen , G. Gay , D. You , M.P.E. Heimdahl , and M. Staats . 2013. Observable Modified Condition\/Decision Coverage . In Proceedings of the 2013 Int'l Conf. on Software Engineering. ACM. M. Whalen, G. Gay, D. You, M.P.E. Heimdahl, and M. Staats. 2013. Observable Modified Condition\/Decision Coverage. In Proceedings of the 2013 Int'l Conf. on Software Engineering. ACM."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.2307\/3001968"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/603095.603153"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491456"}],"event":{"name":"ESEM '20: ACM \/ IEEE International Symposium on Empirical Software Engineering and Measurement","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"],"location":"Bari Italy","acronym":"ESEM '20"},"container-title":["Proceedings of the 14th ACM \/ IEEE International Symposium on Empirical Software Engineering and Measurement (ESEM)"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3382494.3410674","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3382494.3410674","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:38:26Z","timestamp":1750199906000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3382494.3410674"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,10,5]]},"references-count":48,"alternative-id":["10.1145\/3382494.3410674","10.1145\/3382494"],"URL":"https:\/\/doi.org\/10.1145\/3382494.3410674","relation":{},"subject":[],"published":{"date-parts":[[2020,10,5]]},"assertion":[{"value":"2020-10-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}