{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T23:02:07Z","timestamp":1773615727913,"version":"3.50.1"},"reference-count":23,"publisher":"Allerton Press","issue":"7","license":[{"start":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T00:00:00Z","timestamp":1669852800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T00:00:00Z","timestamp":1669852800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Aut. Control Comp. Sci."],"published-print":{"date-parts":[[2022,12]]},"DOI":"10.3103\/s0146411622070045","type":"journal-article","created":{"date-parts":[[2023,2,19]],"date-time":"2023-02-19T09:03:26Z","timestamp":1676797406000},"page":"634-648","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Autotuning Parallel Programs by Model Checking"],"prefix":"10.3103","volume":"56","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9734-3808","authenticated-orcid":false,"given":"N. O.","family":"Garanina","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3857-9380","authenticated-orcid":false,"given":"S. P.","family":"Gorlatch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1627","published-online":{"date-parts":[[2023,2,19]]},"reference":[{"key":"7520_CR1","doi-asserted-by":"publisher","unstructured":"Ansel, J., Kamil, S., Veeramachaneni, K., Ragan-Kelley, J., Bosboom, J., O\u2019Reilly, U.-M., and Amarasinghe, S., OpenTuner: An extensible framework for program autotuning, PACT \u201914: Proc. 23rd Int. Conf. Parallel Architectures and Compilation, Edmonton, Canada, 2014, New York: Association for Computing Machinery, 2014, pp.\u00a0303\u2013316.\u00a0https:\/\/doi.org\/10.1145\/2628071.2628092","DOI":"10.1145\/2628071.2628092"},{"key":"7520_CR2","doi-asserted-by":"publisher","unstructured":"Beckingsale, D., Pearce, O., Laguna, I., and Gamblin, T., Apollo: Reusable models for fast, dynamic tuning of input-dependent code, IEEE Int. Parallel and Distributed Processing Symp. (IPDPS), Orlando, Fla., 2017, IEEE, 2017, pp. 307\u2013316.\u00a0https:\/\/doi.org\/10.1109\/IPDPS.2017.38","DOI":"10.1109\/IPDPS.2017.38"},{"key":"7520_CR3","unstructured":"Chen, C., Chame, J., and Hall, M., CHiLL: A framework for composing high-level loop transformations, Technical Report 08-897, Los Angeles, 2008, pp. 136\u2013150."},{"key":"7520_CR4","doi-asserted-by":"publisher","unstructured":"Christen, M., Schenk, O., and Burkhart, H., PATUS: A code generation and autotuning framework for parallel iterative stencil computations on modern microarchitectures, IEEE Int. Parallel & Distributed Processing Symp., Anchorage, Alaska, 2011, IEEE, 2011, pp. 676\u2013687.\u00a0https:\/\/doi.org\/10.1109\/IPDPS.2011.70","DOI":"10.1109\/IPDPS.2011.70"},{"key":"7520_CR5","doi-asserted-by":"publisher","unstructured":"Whaley, R.C. and Dongarra, J.J., Automatically tuned linear algebra software, SC \u201998: Proc. 1998 ACM\/IEEE Conf. on Supercomputing, Orlando, Fla., 1998, IEEE, 1998, p. 38.\u00a0https:\/\/doi.org\/10.1109\/SC.1998.10004","DOI":"10.1109\/SC.1998.10004"},{"key":"7520_CR6","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1109\/JPROC.2004.840301","volume":"93","author":"M. Frigo","year":"2005","unstructured":"Frigo, M. and Johnson, S.G., The design and implementation of FFTW3, Proc. IEEE, 2005, vol. 93, no. 2, pp.\u00a0216\u2013231.\u00a0https:\/\/doi.org\/10.1109\/JPROC.2004.840301","journal-title":"Proc. IEEE"},{"key":"7520_CR7","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/s10766-010-0161-2","volume":"39","author":"G. Fursin","year":"2011","unstructured":"Fursin, G., Kashnikov, Yu., Memon, A.W., Chamski, Z., Temam, O., Namolaru, M., Yom-Tov, E., Mendelson, B., Zaks, A., Courtois, E., Bodin, F., Barnard, P., Ashton, E., Bonilla, E., Thomson, J., Williams, C.K.I., and O\u2019Boyle, M., Milepost GCC: Machine learning enabled self-tuning compiler, Int. J. Parallel Programming, 2011, vol. 39, pp. 296\u2013327.\u00a0https:\/\/doi.org\/10.1007\/s10766-010-0161-2","journal-title":"Int. J. Parallel Programming"},{"key":"7520_CR8","doi-asserted-by":"publisher","unstructured":"Nugteren, C. and Codreanu, V., CLTUne: A generic auto-tuner for OpenCL kernels, IEEE 9th Int. Symp. on Embedded Multicore\/Many-Core Systems-on-Chip, Turin, Italy, 2015, IEEE, 2015, pp. 195\u2013202.\u00a0https:\/\/doi.org\/10.1109\/MCSoC.2015.10","DOI":"10.1109\/MCSoC.2015.10"},{"key":"7520_CR9","doi-asserted-by":"publisher","first-page":"e4423","DOI":"10.1002\/cpe.4423","volume":"31","author":"A. Rasch","year":"2018","unstructured":"Rasch, A. and Gorlatch, S., ATF: A generic, directive-based auto-tuning framework, Concurrency Comput.: Pract. Exper., 2018, vol. 31, no. 5, p. e4423.\u00a0https:\/\/doi.org\/10.1002\/cpe.4423","journal-title":"Concurrency Comput.: Pract. Exper."},{"key":"7520_CR10","doi-asserted-by":"publisher","unstructured":"Tapus, C., Chung, I.-H., and Hollingsworth, J.K., Active harmony: Towards automated performance tuning, SC \u201902: Proc. 2002 ACM\/IEEE Conf. on Supercomputing, Baltimore, Md., 2002, IEEE, 2002, p. 44.\u00a0https:\/\/doi.org\/10.1109\/SC.2002.10062","DOI":"10.1109\/SC.2002.10062"},{"key":"7520_CR11","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1088\/1742-6596\/16\/1\/071","volume":"16","author":"R. Vuduc","year":"2005","unstructured":"Vuduc, R., Demmel, J.W., and Yelick, K.A., OSKI: A library of automatically tuned sparse matrix kernels, J.\u00a0Phys.: Conf. Ser., 2005, vol. 16, p. 521. \u00a0https:\/\/doi.org\/10.1088\/1742-6596\/16\/1\/071","journal-title":"J.\u00a0Phys.: Conf. Ser."},{"key":"7520_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_1","volume-title":"Introduction to model checking, Handbook of Model Checking","author":"E.M. Clarke","year":"2018","unstructured":"Clarke, E.M., Henzinger, T.A., and Veith, H., Introduction to model checking, Handbook of Model Checking, Clarke, E.M., Henzinger, T.A., Veith, H., and Bloem, R., Eds., Cham: Springer, 2018, pp. 1\u201326. \u00a0https:\/\/doi.org\/10.1007\/978-3-319-10575-8_1"},{"key":"7520_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054185","volume-title":"Experience with literate programming in the modelling and validation of systems, Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1998","author":"T.C. Ruys","year":"1998","unstructured":"Ruys, T.C. and Brinksma, E., Experience with literate programming in the modelling and validation of systems, Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1998, Steffen, B., Ed., Lecture Notes in Computer Science, vol. 1384, Berlin: Springer, 1998, pp. 393\u2013408. \u00a0https:\/\/doi.org\/10.1007\/BFb0054185"},{"key":"7520_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44829-2_1","volume-title":"Optimal scheduling using branch and bound with SPIN 4.0, Model Checking Software. SPIN 2003","author":"T. Ruys","year":"2003","unstructured":"Ruys, T., Optimal scheduling using branch and bound with SPIN 4.0, Model Checking Software. SPIN 2003, Ball, T. and Rajamani, S.K., Eds., Lecture Notes in Computer Science, vol. 2648, Berlin: Springer, 2003, pp.\u00a01\u201317. \u00a0https:\/\/doi.org\/10.1007\/3-540-44829-2_1"},{"key":"7520_CR15","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., and Fehnker, A., Verification and optimization of a PLC control schedule, Int. J. Software Tools Technol. Transfer, 2002, vol. 4, pp. 21\u201333.\u00a0https:\/\/doi.org\/10.1007\/s10009-002-0079-0","journal-title":"Int. J. Software Tools Technol. Transfer"},{"key":"7520_CR16","doi-asserted-by":"publisher","unstructured":"Wijs, A., van de Pol, J., and Bortnik, E.M., Solving scheduling problems by untimed model checking: The clinical chemical analyser case study, FMICS \u201905: Proc. 10th Int. Workshop on Formal Methods for Industrial Critical Systems, Lisbon, 2005, New York: Association for Computing Machinery, 2005, pp. 54\u201361.\u00a0https:\/\/doi.org\/10.1145\/1081180.1081188","DOI":"10.1145\/1081180.1081188"},{"key":"7520_CR17","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. and Pena, P.N., Optimal task scheduling in a flexible manufacturing system using model checking, IFAC-PapersOnLine, 2018, vol. 51, no. 7, pp. 230\u2013235.https:\/\/doi.org\/10.1016\/j.ifacol.2018.06.306","journal-title":"IFAC-PapersOnLine"},{"key":"7520_CR18","unstructured":"The OpenCL Specification, Khronos OpenCL Working Group, 2021."},{"key":"7520_CR19","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J., The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley Professional, 2003."},{"key":"7520_CR20","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R., Communicating Sequential Processes, Englewood Cliffs, N.J.: Prentice-Hall, 1985."},{"key":"7520_CR21","doi-asserted-by":"publisher","unstructured":"Gaspari, M. and Zavattaro, G., An algebra of actors, Formal Methods for Open Object-Based Distributed Systems. FMOODS 1999, Ciancarini, P., Fantechi, A., and Gorrieri, R., Eds., IFIP\u2014The International Federation for Information Processing, vol. 10, Boston: Springer, 1999, pp. 3\u201318.\u00a0https:\/\/doi.org\/10.1007\/978-0-387-35562-7_2","DOI":"10.1007\/978-0-387-35562-7_2"},{"key":"7520_CR22","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Edelkamp, S., Fox, M., Magazzeni, D., and Plaku, E., Automated planning and model checking, Dagstuhl Seminar 14482, Dagstuhl Reports, vol. 4, Schloss Dagstuhl\u2013Leibniz Zentrum f\u00fcr Informatik, 2015.\u00a0https:\/\/doi.org\/10.4230\/DagRep.4.11.227","DOI":"10.4230\/DagRep.4.11.227"},{"key":"7520_CR23","volume-title":"NVIDIA\u2019s Fermi: The first complete GPU computing architecture.","author":"P.N. Glaskowsky","year":"2009","unstructured":"Glaskowsky, P.N., NVIDIA\u2019s Fermi: The first complete GPU computing architecture. NVIDIA Corporation, 2009."}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411622070045.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S0146411622070045","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411622070045.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T22:03:47Z","timestamp":1773612227000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S0146411622070045"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,12]]},"references-count":23,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2022,12]]}},"alternative-id":["7520"],"URL":"https:\/\/doi.org\/10.3103\/s0146411622070045","relation":{},"ISSN":["0146-4116","1558-108X"],"issn-type":[{"value":"0146-4116","type":"print"},{"value":"1558-108X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,12]]},"assertion":[{"value":"15 November 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 December 2021","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 December 2021","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 February 2023","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}