{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,25]],"date-time":"2026-01-25T04:33:46Z","timestamp":1769315626978,"version":"3.49.0"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031167669","type":"print"},{"value":"9783031167676","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-16767-6_4","type":"book-chapter","created":{"date-parts":[[2022,9,10]],"date-time":"2022-09-10T16:02:40Z","timestamp":1662825760000},"page":"63-82","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Model Checking Meets Auto-Tuning of\u00a0High-Performance Programs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9734-3808","authenticated-orcid":false,"given":"Natalia","family":"Garanina","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5183-9736","authenticated-orcid":false,"given":"Sergey","family":"Staroletov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3857-9380","authenticated-orcid":false,"given":"Sergei","family":"Gorlatch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,9,11]]},"reference":[{"key":"4_CR1","unstructured":"Ansel, J., Kamil, S., Veeramachaneni, K., et al.: Opentuner: an extensible framework for program autotuning. In: Proceedings of 2017 IEEE International Parallel and Distributed Processing Symposium (IPDPS), pp. 385\u2013392. IEEE (2017)"},{"key":"4_CR2","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s10009-002-0079-0","volume":"4","author":"E Brinksma","year":"2002","unstructured":"Brinksma, E., Mader, A., Fehnker, A.: Verification and optimization of a PLC control schedule. Int. J. Softw. Tools Technol. Transf. 4, 21\u201333 (2002)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Christen, M., Schenk, O., Burkhart, H.: PATUS: a code generation and autotuning framework for parallel iterative stencil computations on modern microarchitectures. In: Proceedings of 2011 IEEE International Parallel Distributed Processing Symposium, pp. 385\u2013392. IEEE (2011)","DOI":"10.1109\/IPDPS.2011.70"},{"issue":"11","key":"4_CR4","doi-asserted-by":"publisher","first-page":"227","DOI":"10.4230\/DagRep.4.11.227","volume":"4","author":"A Cimatti","year":"2015","unstructured":"Cimatti, A., Edelkamp, S., Fox, M., Magazzeni, D., Plaku, E.: Automated planning and model checking (Seminar 14482). Dagstuhl Rep. 4(11), 227\u2013245 (2015). https:\/\/doi.org\/10.4230\/DagRep.4.11.227","journal-title":"Dagstuhl Rep."},{"key":"4_CR5","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H. (eds.) Handbook of Model Checking. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"4_CR6","unstructured":"Clint, W., Dongarra, J.: Automatically tuned linear algebra software. In: Proceedings of the ACM\/IEEE Conference on Supercomputing, pp. 385\u2013392. IEEE (1998)"},{"issue":"2","key":"4_CR7","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1109\/JPROC.2004.840301","volume":"93","author":"M Frigo","year":"2005","unstructured":"Frigo, M., Johnson, S.G.: The design and implementation of FFTW3. IEEE 93(2), 187\u2013195 (2005)","journal-title":"IEEE"},{"key":"4_CR8","unstructured":"Garanina, N., Staroletov, S.: Discussed models in Promela (2022). https:\/\/github.com\/SergeyStaroletov\/PromelaSamples\/tree\/master\/autotune_opencl"},{"issue":"4","key":"4_CR9","doi-asserted-by":"publisher","first-page":"338","DOI":"10.18255\/1818-1015-2021-4-338-355","volume":"28","author":"NO Garanina","year":"2021","unstructured":"Garanina, N.O., Gorlatch, S.P.: Autotuning parallel programs by model checking. Model. Anal. Inf. Syst. 28(4), 338\u2013355 (2021). in Russian","journal-title":"Model. Anal. Inf. Syst."},{"key":"4_CR10","series-title":"IFIP \u2014 The International Federation for Information Processing","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-0-387-35562-7_2","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"M Gaspari","year":"1999","unstructured":"Gaspari, M., Zavattaro, G.: An Algebra of Actors. In: Ciancarini, P., Fantechi, A., Gorrieri, R. (eds.) FMOODS 1999. ITIFIP, vol. 10, pp. 3\u201318. Springer, Boston (1999). https:\/\/doi.org\/10.1007\/978-0-387-35562-7_2"},{"key":"4_CR11","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Hoboken (1985)"},{"key":"4_CR12","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, Boston (2003)"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-85114-1_11","volume-title":"Model Checking Software","author":"GJ Holzmann","year":"2008","unstructured":"Holzmann, G.J., Joshi, R., Groce, A.: Tackling large verification problems with the swarm tool. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 134\u2013143. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-85114-1_11"},{"issue":"6","key":"4_CR14","doi-asserted-by":"publisher","first-page":"845","DOI":"10.1109\/TSE.2010.110","volume":"37","author":"GJ Holzmann","year":"2010","unstructured":"Holzmann, G.J., Joshi, R., Groce, A.: Swarm verification techniques. IEEE Trans. Softw. Eng. 37(6), 845\u2013857 (2010)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"4_CR15","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-642-21434-9_3","volume-title":"Autonomous Search","author":"HH Hoos","year":"2011","unstructured":"Hoos, H.H.: Automated algorithm configuration and parameter tuning. In: Hamadi, Y., Monfroy, E., Saubion, F. (eds.) Autonomous Search, pp. 37\u201371. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21434-9_3"},{"key":"4_CR16","unstructured":"Khronos: OpenCL specification by Khronos OpenCL working group 2021 (2021). https:\/\/www.khronos.org\/registry\/OpenCL\/specs\/3.0-unified\/html\/OpenCL_API.html"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Lashgar, A., Baniasadi, A., Khonsari, A.: Warp size impact in GPUs: large or small? In: Proceedings of the 6th Workshop on General Purpose Processor Using Graphics Processing Units, pp. 146\u2013152 (2013)","DOI":"10.1145\/2458523.2458538"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Lazreg, S., Cordy, M., Collet, P., Heymans, P., Mosser, S.: Multifaceted automated analyses for variability-intensive embedded systems. In: 2019 IEEE\/ACM 41st International Conference on Software Engineering (ICSE), pp. 854\u2013865. IEEE (2019)","DOI":"10.1109\/ICSE.2019.00092"},{"issue":"7","key":"4_CR19","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1016\/j.ifacol.2018.06.306","volume":"51","author":"R Malik","year":"2018","unstructured":"Malik, R., Pena, P.: Optimal task scheduling in a flexible manufacturing system using model checking. IFAC-PapersOnLine 51(7), 230\u2013235 (2018)","journal-title":"IFAC-PapersOnLine"},{"key":"4_CR20","unstructured":"Nimble-code: Promela language grammar (2021). http:\/\/spinroot.com\/spin\/Man\/grammar.html"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Nugteren, C., Codreanu, V.: Cltune: a generic auto-tuner for OpenCL kernels. In: Proceedings of 9th International Symposium on Embedded Multicore\/Many-core Systems-on-Chip, pp. 385\u2013392. IEEE (2015)","DOI":"10.1109\/MCSoC.2015.10"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Panizo, L., Salmer\u00f3n, A., Gallardo, M.D.M., Merino, P.: Guided test case generation for mobile apps in the TRIANGLE project: work in progress. In: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, pp. 192\u2013195 (2017)","DOI":"10.1145\/3092282.3092298"},{"issue":"5","key":"4_CR23","doi-asserted-by":"publisher","first-page":"e4423","DOI":"10.1002\/cpe.4423","volume":"31","author":"A Rasch","year":"2019","unstructured":"Rasch, A., Gorlatch, S.: ATF: a generic directive-based auto-tuning framework. Concurrency Comput. Pract. Experience 31(5), e4423 (2019). https:\/\/doi.org\/10.1002\/cpe.4423","journal-title":"Concurrency Comput. Pract. Experience"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Ruys, T.C., Brinksma, E.: Experience with literate programming in the modelling and validation of systems. In: Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 1998), pp. 393\u2013408 (1998)","DOI":"10.1007\/BFb0054185"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44829-2_1","volume-title":"Model Checking Software","author":"TC Ruys","year":"2003","unstructured":"Ruys, T.C.: Optimal scheduling using branch and bound with SPIN 4.0. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 1\u201317. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-44829-2_1"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Staroletov, S.: Model checking games and a genome sequence search. In: Journal of Physics: Conference Series, vol. 1679, p. 032020. IOP Publishing (2020)","DOI":"10.1088\/1742-6596\/1679\/3\/032020"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Subhlok, J., Stichnoth, J.M., O\u2019hallaron, D.R., Gross, T.: Exploiting task and data parallelism on a multicomputer. In: Proceedings of the Fourth ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pp. 13\u201322 (1993)","DOI":"10.1145\/173284.155334"},{"issue":"5","key":"4_CR28","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/s10009-009-0110-9","volume":"11","author":"A Wijs","year":"2016","unstructured":"Wijs, A., Pol, J.V.D., Bortnik, E.M.: Solving scheduling problems by untimed model checking: the clinical chemical analyser case study. Int. J. Softw. Tools Technol. Transf. 11(5), 375\u2013392 (2016)","journal-title":"Int. J. Softw. Tools Technol. Transf."}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-16767-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,14]],"date-time":"2022-09-14T23:17:43Z","timestamp":1663197463000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-16767-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031167669","9783031167676"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-16767-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"11 September 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"LOPSTR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Logic-Based Program Synthesis and Transformation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tbilisi","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Georgia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 September 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 September 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"lopstr2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/lopstr2022.webs.upv.es","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"17","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"8","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"47% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}