[{"date_updated":"2023-09-06T08:27:33Z","oa":1,"volume":13964,"article_processing_charge":"Yes (in subscription journal)","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","acknowledgement":"This research was funded in part by the German Research Foundation (DFG) project 427755713 Group-By Objectives in Probabilistic Verification (GOPro).","quality_controlled":"1","oa_version":"Published Version","_id":"14259","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031377051"],"issn":["0302-9743"]},"publication_status":"published","citation":{"ieee":"J. Kretinsky, T. Meggendorfer, M. Prokop, and S. Rieder, “Guessing winning policies in LTL synthesis by semantic learning,” in <i>35th International Conference on Computer Aided Verification </i>, Paris, France, 2023, vol. 13964, pp. 390–414.","apa":"Kretinsky, J., Meggendorfer, T., Prokop, M., &#38; Rieder, S. (2023). Guessing winning policies in LTL synthesis by semantic learning. In <i>35th International Conference on Computer Aided Verification </i> (Vol. 13964, pp. 390–414). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-37706-8_20\">https://doi.org/10.1007/978-3-031-37706-8_20</a>","chicago":"Kretinsky, Jan, Tobias Meggendorfer, Maximilian Prokop, and Sabine Rieder. “Guessing Winning Policies in LTL Synthesis by Semantic Learning.” In <i>35th International Conference on Computer Aided Verification </i>, 13964:390–414. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-37706-8_20\">https://doi.org/10.1007/978-3-031-37706-8_20</a>.","ama":"Kretinsky J, Meggendorfer T, Prokop M, Rieder S. Guessing winning policies in LTL synthesis by semantic learning. In: <i>35th International Conference on Computer Aided Verification </i>. Vol 13964. Springer Nature; 2023:390-414. doi:<a href=\"https://doi.org/10.1007/978-3-031-37706-8_20\">10.1007/978-3-031-37706-8_20</a>","mla":"Kretinsky, Jan, et al. “Guessing Winning Policies in LTL Synthesis by Semantic Learning.” <i>35th International Conference on Computer Aided Verification </i>, vol. 13964, Springer Nature, 2023, pp. 390–414, doi:<a href=\"https://doi.org/10.1007/978-3-031-37706-8_20\">10.1007/978-3-031-37706-8_20</a>.","ista":"Kretinsky J, Meggendorfer T, Prokop M, Rieder S. 2023. Guessing winning policies in LTL synthesis by semantic learning. 35th International Conference on Computer Aided Verification . CAV: Computer Aided Verification, LNCS, vol. 13964, 390–414.","short":"J. Kretinsky, T. Meggendorfer, M. Prokop, S. Rieder, in:, 35th International Conference on Computer Aided Verification , Springer Nature, 2023, pp. 390–414."},"author":[{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky","full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","first_name":"Jan"},{"last_name":"Meggendorfer","full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165","first_name":"Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1"},{"last_name":"Prokop","full_name":"Prokop, Maximilian","first_name":"Maximilian"},{"first_name":"Sabine","full_name":"Rieder, Sabine","last_name":"Rieder"}],"abstract":[{"text":"We provide a learning-based technique for guessing a winning strategy in a parity game originating from an LTL synthesis problem. A cheaply obtained guess can be useful in several applications. Not only can the guessed strategy be applied as best-effort in cases where the game’s huge size prohibits rigorous approaches, but it can also increase the scalability of rigorous LTL synthesis in several ways. Firstly, checking whether a guessed strategy is winning is easier than constructing one. Secondly, even if the guess is wrong in some places, it can be fixed by strategy iteration faster than constructing one from scratch. Thirdly, the guess can be used in on-the-fly approaches to prioritize exploration in the most fruitful directions.\r\nIn contrast to previous works, we (i) reflect the highly structured logical information in game’s states, the so-called semantic labelling, coming from the recent LTL-to-automata translations, and (ii) learn to reflect it properly by learning from previously solved games, bringing the solving process closer to human-like reasoning.","lang":"eng"}],"alternative_title":["LNCS"],"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"ddc":["000"],"doi":"10.1007/978-3-031-37706-8_20","year":"2023","title":"Guessing winning policies in LTL synthesis by semantic learning","page":"390-414","file_date_updated":"2023-09-06T08:25:50Z","publication":"35th International Conference on Computer Aided Verification ","type":"conference","day":"17","status":"public","intvolume":"     13964","department":[{"_id":"KrCh"}],"license":"https://creativecommons.org/licenses/by/4.0/","has_accepted_license":"1","file":[{"access_level":"open_access","date_updated":"2023-09-06T08:25:50Z","checksum":"ed66278b61bb869e1baba3d9b9081271","date_created":"2023-09-06T08:25:50Z","file_size":428354,"file_name":"2023_LNCS_CAV_Kretinsky.pdf","creator":"dernst","file_id":"14276","relation":"main_file","content_type":"application/pdf","success":1}],"date_created":"2023-09-03T22:01:16Z","conference":{"start_date":"2023-07-17","name":"CAV: Computer Aided Verification","end_date":"2023-07-22","location":"Paris, France"},"date_published":"2023-07-17T00:00:00Z","month":"07","language":[{"iso":"eng"}],"publisher":"Springer Nature","scopus_import":"1"},{"alternative_title":["LNCS"],"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"related_material":{"record":[{"relation":"research_data","id":"14995","status":"public"}]},"ddc":["000"],"year":"2023","doi":"10.1007/978-3-031-37706-8_8","title":"Lincheck: A practical framework for testing concurrent data structures on JVM","oa":1,"date_updated":"2024-02-27T07:46:52Z","volume":13964,"article_processing_charge":"Yes (in subscription journal)","_id":"14260","publication_identifier":{"isbn":["9783031377051"],"issn":["0302-9743"],"eissn":["1611-3349"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Published Version","quality_controlled":"1","publication_status":"published","citation":{"ieee":"N. Koval, A. Fedorov, M. Sokolova, D. Tsitelov, and D.-A. Alistarh, “Lincheck: A practical framework for testing concurrent data structures on JVM,” in <i>35th International Conference on Computer Aided Verification </i>, Paris, France, 2023, vol. 13964, pp. 156–169.","apa":"Koval, N., Fedorov, A., Sokolova, M., Tsitelov, D., &#38; Alistarh, D.-A. (2023). Lincheck: A practical framework for testing concurrent data structures on JVM. In <i>35th International Conference on Computer Aided Verification </i> (Vol. 13964, pp. 156–169). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-37706-8_8\">https://doi.org/10.1007/978-3-031-37706-8_8</a>","chicago":"Koval, Nikita, Alexander Fedorov, Maria Sokolova, Dmitry Tsitelov, and Dan-Adrian Alistarh. “Lincheck: A Practical Framework for Testing Concurrent Data Structures on JVM.” In <i>35th International Conference on Computer Aided Verification </i>, 13964:156–69. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-37706-8_8\">https://doi.org/10.1007/978-3-031-37706-8_8</a>.","mla":"Koval, Nikita, et al. “Lincheck: A Practical Framework for Testing Concurrent Data Structures on JVM.” <i>35th International Conference on Computer Aided Verification </i>, vol. 13964, Springer Nature, 2023, pp. 156–69, doi:<a href=\"https://doi.org/10.1007/978-3-031-37706-8_8\">10.1007/978-3-031-37706-8_8</a>.","ama":"Koval N, Fedorov A, Sokolova M, Tsitelov D, Alistarh D-A. Lincheck: A practical framework for testing concurrent data structures on JVM. In: <i>35th International Conference on Computer Aided Verification </i>. Vol 13964. Springer Nature; 2023:156-169. doi:<a href=\"https://doi.org/10.1007/978-3-031-37706-8_8\">10.1007/978-3-031-37706-8_8</a>","short":"N. Koval, A. Fedorov, M. Sokolova, D. Tsitelov, D.-A. Alistarh, in:, 35th International Conference on Computer Aided Verification , Springer Nature, 2023, pp. 156–169.","ista":"Koval N, Fedorov A, Sokolova M, Tsitelov D, Alistarh D-A. 2023. Lincheck: A practical framework for testing concurrent data structures on JVM. 35th International Conference on Computer Aided Verification . CAV: Computer Aided Verification, LNCS, vol. 13964, 156–169."},"abstract":[{"lang":"eng","text":"This paper presents Lincheck, a new practical and user-friendly framework for testing concurrent algorithms on the Java Virtual Machine (JVM). Lincheck provides a simple and declarative way to write concurrent tests: instead of describing how to perform the test, users specify what to test by declaring all the operations to examine; the framework automatically handles the rest. As a result, tests written with Lincheck are concise and easy to understand. The framework automatically generates a set of concurrent scenarios, examines them using stress-testing or bounded model checking, and verifies that the results of each invocation are correct. Notably, if an error is detected via model checking, Lincheck provides an easy-to-follow trace to reproduce it, significantly simplifying the bug investigation.\r\n\r\nTo the best of our knowledge, Lincheck is the first production-ready tool on the JVM that offers such a simple way of writing concurrent tests, without requiring special skills or expertise. We successfully integrated Lincheck in the development process of several large projects, such as Kotlin Coroutines, and identified new bugs in popular concurrency libraries, such as a race in Java’s standard ConcurrentLinkedDeque and a liveliness bug in Java’s AbstractQueuedSynchronizer framework, which is used in most of the synchronization primitives. We believe that Lincheck can significantly improve the quality and productivity of concurrent algorithms research and development and become the state-of-the-art tool for checking their correctness."}],"author":[{"id":"2F4DB10C-F248-11E8-B48F-1D18A9856A87","first_name":"Nikita","full_name":"Koval, Nikita","last_name":"Koval"},{"id":"2e711909-896a-11ed-bdf8-eb0f5a2984c6","first_name":"Alexander","last_name":"Fedorov","full_name":"Fedorov, Alexander"},{"first_name":"Maria","full_name":"Sokolova, Maria","last_name":"Sokolova"},{"full_name":"Tsitelov, Dmitry","last_name":"Tsitelov","first_name":"Dmitry"},{"id":"4A899BFC-F248-11E8-B48F-1D18A9856A87","first_name":"Dan-Adrian","last_name":"Alistarh","full_name":"Alistarh, Dan-Adrian","orcid":"0000-0003-3650-940X"}],"has_accepted_license":"1","department":[{"_id":"DaAl"},{"_id":"GradSch"}],"conference":{"start_date":"2023-07-17","name":"CAV: Computer Aided Verification","end_date":"2023-07-22","location":"Paris, France"},"file":[{"success":1,"relation":"main_file","content_type":"application/pdf","file_id":"14275","creator":"dernst","file_size":421408,"file_name":"2023_LNCS_Koval.pdf","checksum":"c346016393123a0a2338ad4d976f61bc","date_created":"2023-09-06T08:16:25Z","access_level":"open_access","date_updated":"2023-09-06T08:16:25Z"}],"date_created":"2023-09-03T22:01:16Z","month":"07","date_published":"2023-07-17T00:00:00Z","publisher":"Springer Nature","scopus_import":"1","language":[{"iso":"eng"}],"publication":"35th International Conference on Computer Aided Verification ","file_date_updated":"2023-09-06T08:16:25Z","page":"156-169","day":"17","type":"conference","intvolume":"     13964","status":"public"}]