{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T11:41:20Z","timestamp":1762429280202,"version":"3.41.0"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2017,2,3]],"date-time":"2017-02-03T00:00:00Z","timestamp":1486080000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100002341","name":"Suomen Akatemia","doi-asserted-by":"publisher","award":["277522"],"award-info":[{"award-number":["277522"]}],"id":[{"id":"10.13039\/501100002341","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2017,5,31]]},"abstract":"<jats:p>This article focuses on computing minimal test suites for multithreaded programs. Based on previous work on test case generation for multithreaded programs using unfoldings, this article shows how this unfolding can be used to generate minimal test suites covering all local states of the program. Generating such minimal test suites is shown to be NP-complete in the size of the unfolding. We propose an SMT encoding for this problem and two methods based on heuristics which only approximate the solution, but scale better in practice. Finally, we apply our methods to compute the minimal test suites for several benchmarks.<\/jats:p>","DOI":"10.1145\/3012281","type":"journal-article","created":{"date-parts":[[2017,2,10]],"date-time":"2017-02-10T13:28:54Z","timestamp":1486733334000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Minimizing Test Suites with Unfoldings of Multithreaded Programs"],"prefix":"10.1145","volume":"16","author":[{"given":"Olli","family":"Saarikivi","sequence":"first","affiliation":[{"name":"Aalto University and Helsinki Institute for Information Technology HIIT, Aalto, Finland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hern\u00e1n","family":"Ponce-De-Le\u00f3n","sequence":"additional","affiliation":[{"name":"Aalto University and Helsinki Institute for Information Technology HIIT, Aalto, Finland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kari","family":"K\u00e4hk\u00f6nen","sequence":"additional","affiliation":[{"name":"Aalto University and Helsinki Institute for Information Technology HIIT, Aalto, Finland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Keijo","family":"Heljanko","sequence":"additional","affiliation":[{"name":"Aalto University and Helsinki Institute for Information Technology HIIT, Aalto, Finland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Javier","family":"Esparza","sequence":"additional","affiliation":[{"name":"Fakult\u00e4t f\u00fcr informatik, Technische Universit\u00e4t M\u00fcnchen, M\u00fcnchen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,2,3]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_28"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535845"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_8"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.3060"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/646486.694625"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Volker Diekert and Grzegorz Rozenberg (Eds.). 1995. The Book of Traces. World Scientific Publishing Co. Inc.   Volker Diekert and Grzegorz Rozenberg (Eds.). 1995. The Book of Traces. World Scientific Publishing Co. Inc.","DOI":"10.1142\/2563"},{"volume-title":"Unfoldings\u2014Partial-Order Approach to Model Checking","author":"Esparza Javier","key":"e_1_2_1_8_1","unstructured":"Javier Esparza and Keijo Heljanko . 2008. Unfoldings\u2014Partial-Order Approach to Model Checking . Springer . Javier Esparza and Keijo Heljanko. 2008. Unfoldings\u2014Partial-Order Approach to Model Checking. Springer."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491453"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_30"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/547238"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-09099-3_15"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2014.20"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2351676.2351698"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-006-0023-y"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01384314"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01178907"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/646736.701774"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90112-2"},{"key":"e_1_2_1_23_1","unstructured":"Sampo Niskanen and Patric \u00d6sterg\u00e5rd. 2002. Cliquer - routines for clique searching. Retrieved from http:\/\/users.aalto.fi\/&sim;pat\/cliquer.html.  Sampo Niskanen and Patric \u00d6sterg\u00e5rd. 2002. Cliquer - routines for clique searching. Retrieved from http:\/\/users.aalto.fi\/&sim;pat\/cliquer.html."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0166-218X(01)00290-6"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-15579-1_11"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2015.12"},{"key":"e_1_2_1_27_1","unstructured":"C\u00e9sar Rodr\u00edguez. 2013. Verification Based on Unfoldings of Petri Nets with Read Arcs. Th\u00e8se de doctorat. Laboratoire Sp\u00e9cification et V\u00e9rification ENS Cachan France.  C\u00e9sar Rodr\u00edguez. 2013. Verification Based on Unfoldings of Petri Nets with Read Arcs. Th\u00e8se de doctorat. Laboratoire Sp\u00e9cification et V\u00e9rification ENS Cachan France."},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the 26th International Conference on Concurrency Theory (CONCUR\u201915)","author":"Rodr\u00edguez C\u00e9sar","year":"2015","unstructured":"C\u00e9sar Rodr\u00edguez , Marcelo Sousa , Subodh Sharma , and Daniel Kroening . 2015 . Unfolding-based partial order reduction . In Proceedings of the 26th International Conference on Concurrency Theory (CONCUR\u201915) . 456--469. C\u00e9sar Rodr\u00edguez, Marcelo Sousa, Subodh Sharma, and Daniel Kroening. 2015. Unfolding-based partial order reduction. In Proceedings of the 26th International Conference on Concurrency Theory (CONCUR\u201915). 456--469."},{"key":"e_1_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Antti Valmari. 1996. The state explosion problem. In Lectures on Petri Nets I: Basic Models Advances in Petri Nets the Volumes Are Based on the Advanced Course on Petri Nets. 429--528.   Antti Valmari. 1996. The state explosion problem. In Lectures on Petri Nets I: Basic Models Advances in Petri Nets the Volumes Are Based on the Advanced Course on Petri Nets. 429--528.","DOI":"10.1007\/3-540-65306-6_21"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3012281","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3012281","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:54:47Z","timestamp":1750222487000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3012281"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,2,3]]},"references-count":28,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,5,31]]}},"alternative-id":["10.1145\/3012281"],"URL":"https:\/\/doi.org\/10.1145\/3012281","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2017,2,3]]},"assertion":[{"value":"2016-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-02-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}