[{"month":"04","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031308284"],"issn":["0302-9743"]},"conference":{"name":"FOSSACS: Foundations of Software Science and Computation Structures","location":"Paris, France","start_date":"2023-04-22","end_date":"2023-04-27"},"doi":"10.1007/978-3-031-30829-1_17","language":[{"iso":"eng"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"oa":1,"external_id":{"arxiv":["2301.11175"]},"quality_controlled":"1","project":[{"call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"file_date_updated":"2023-06-19T10:28:09Z","ec_funded":1,"license":"https://creativecommons.org/licenses/by/4.0/","author":[{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Mazzocchi, Nicolas Adrien","id":"b26baa86-3308-11ec-87b0-8990f34baa85","first_name":"Nicolas Adrien","last_name":"Mazzocchi"},{"id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","first_name":"Naci E","last_name":"Sarac","full_name":"Sarac, Naci E"}],"date_updated":"2023-07-14T11:20:27Z","date_created":"2023-01-31T07:23:56Z","volume":13992,"year":"2023","acknowledgement":"We thank the anonymous reviewers for their helpful comments. This work was supported in part by the ERC-2020-AdG 101020093.","publication_status":"published","publisher":"Springer Nature","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"day":"21","has_accepted_license":"1","article_processing_charge":"No","scopus_import":"1","date_published":"2023-04-21T00:00:00Z","publication":"26th International Conference Foundations of Software Science and Computation Structures","citation":{"ama":"Henzinger TA, Mazzocchi NA, Sarac NE. Quantitative safety and liveness. In: 26th International Conference Foundations of Software Science and Computation Structures. Vol 13992. Springer Nature; 2023:349-370. doi:10.1007/978-3-031-30829-1_17","apa":"Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2023). Quantitative safety and liveness. In 26th International Conference Foundations of Software Science and Computation Structures (Vol. 13992, pp. 349–370). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30829-1_17","ieee":"T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Quantitative safety and liveness,” in 26th International Conference Foundations of Software Science and Computation Structures, Paris, France, 2023, vol. 13992, pp. 349–370.","ista":"Henzinger TA, Mazzocchi NA, Sarac NE. 2023. Quantitative safety and liveness. 26th International Conference Foundations of Software Science and Computation Structures. FOSSACS: Foundations of Software Science and Computation Structures, LNCS, vol. 13992, 349–370.","short":"T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 26th International Conference Foundations of Software Science and Computation Structures, Springer Nature, 2023, pp. 349–370.","mla":"Henzinger, Thomas A., et al. “Quantitative Safety and Liveness.” 26th International Conference Foundations of Software Science and Computation Structures, vol. 13992, Springer Nature, 2023, pp. 349–70, doi:10.1007/978-3-031-30829-1_17.","chicago":"Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Quantitative Safety and Liveness.” In 26th International Conference Foundations of Software Science and Computation Structures, 13992:349–70. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30829-1_17."},"page":"349-370","abstract":[{"lang":"eng","text":"Safety and liveness are elementary concepts of computation, and the foundation of many verification paradigms. The safety-liveness classification of boolean properties characterizes whether a given property can be falsified by observing a finite prefix of an infinite computation trace (always for safety, never for liveness). In quantitative specification and verification, properties assign not truth values, but quantitative values to infinite traces (e.g., a cost, or the distance to a boolean property). We introduce quantitative safety and liveness, and we prove that our definitions induce conservative quantitative generalizations of both (1)~the safety-progress hierarchy of boolean properties and (2)~the safety-liveness decomposition of boolean properties. In particular, we show that every quantitative property can be written as the pointwise minimum of a quantitative safety property and a quantitative liveness property. Consequently, like boolean properties, also quantitative properties can be min-decomposed into safety and liveness parts, or alternatively, max-decomposed into co-safety and co-liveness parts. Moreover, quantitative properties can be approximated naturally. We prove that every quantitative property that has both safe and co-safe approximations can be monitored arbitrarily precisely by a monitor that uses only a finite number of states."}],"type":"conference","alternative_title":["LNCS"],"file":[{"date_updated":"2023-01-31T07:22:21Z","date_created":"2023-01-31T07:22:21Z","success":1,"checksum":"981025aed580b6b27c426cb8856cf63e","file_id":"12468","relation":"main_file","creator":"esarac","content_type":"application/pdf","file_size":449027,"file_name":"qsl.pdf","access_level":"open_access"},{"creator":"dernst","file_size":1048171,"content_type":"application/pdf","access_level":"open_access","file_name":"2023_LNCS_HenzingerT.pdf","success":1,"checksum":"f16e2af1e0eb243158ab0f0fe74e7d5a","date_updated":"2023-06-19T10:28:09Z","date_created":"2023-06-19T10:28:09Z","file_id":"13153","relation":"main_file"}],"oa_version":"Published Version","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","_id":"12467","ddc":["000"],"title":"Quantitative safety and liveness","status":"public","intvolume":" 13992"},{"publication_identifier":{"eissn":["2475-1421"]},"month":"06","language":[{"iso":"eng"}],"doi":"10.1145/3591230","quality_controlled":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"oa":1,"file_date_updated":"2023-07-03T13:09:39Z","article_number":"116","volume":7,"date_updated":"2023-07-17T08:43:19Z","date_created":"2023-07-02T22:00:43Z","author":[{"last_name":"Koval","first_name":"Nikita","id":"2F4DB10C-F248-11E8-B48F-1D18A9856A87","full_name":"Koval, Nikita"},{"full_name":"Khalanskiy, Dmitry","last_name":"Khalanskiy","first_name":"Dmitry"},{"last_name":"Alistarh","first_name":"Dan-Adrian","orcid":"0000-0003-3650-940X","id":"4A899BFC-F248-11E8-B48F-1D18A9856A87","full_name":"Alistarh, Dan-Adrian"}],"department":[{"_id":"DaAl"}],"publisher":"Association for Computing Machinery ","publication_status":"published","year":"2023","has_accepted_license":"1","article_processing_charge":"No","day":"06","scopus_import":"1","date_published":"2023-06-06T00:00:00Z","article_type":"original","citation":{"ama":"Koval N, Khalanskiy D, Alistarh D-A. CQS: A formally-verified framework for fair and abortable synchronization. Proceedings of the ACM on Programming Languages. 2023;7. doi:10.1145/3591230","ista":"Koval N, Khalanskiy D, Alistarh D-A. 2023. CQS: A formally-verified framework for fair and abortable synchronization. Proceedings of the ACM on Programming Languages. 7, 116.","ieee":"N. Koval, D. Khalanskiy, and D.-A. Alistarh, “CQS: A formally-verified framework for fair and abortable synchronization,” Proceedings of the ACM on Programming Languages, vol. 7. Association for Computing Machinery , 2023.","apa":"Koval, N., Khalanskiy, D., & Alistarh, D.-A. (2023). CQS: A formally-verified framework for fair and abortable synchronization. Proceedings of the ACM on Programming Languages. Association for Computing Machinery . https://doi.org/10.1145/3591230","mla":"Koval, Nikita, et al. “CQS: A Formally-Verified Framework for Fair and Abortable Synchronization.” Proceedings of the ACM on Programming Languages, vol. 7, 116, Association for Computing Machinery , 2023, doi:10.1145/3591230.","short":"N. Koval, D. Khalanskiy, D.-A. Alistarh, Proceedings of the ACM on Programming Languages 7 (2023).","chicago":"Koval, Nikita, Dmitry Khalanskiy, and Dan-Adrian Alistarh. “CQS: A Formally-Verified Framework for Fair and Abortable Synchronization.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery , 2023. https://doi.org/10.1145/3591230."},"publication":"Proceedings of the ACM on Programming Languages","abstract":[{"text":"Writing concurrent code that is both correct and efficient is notoriously difficult. Thus, programmers often prefer to use synchronization abstractions, which render code simpler and easier to reason about. Despite a wealth of work on this topic, there is still a gap between the rich semantics provided by synchronization abstractions in modern programming languages—specifically, fair FIFO ordering of synchronization requests and support for abortable operations—and frameworks for implementing it correctly and efficiently. Supporting such semantics is critical given the rising popularity of constructs for asynchronous programming, such as coroutines, which abort frequently and are cheaper to suspend and resume compared to native threads.\r\n\r\nThis paper introduces a new framework called CancellableQueueSynchronizer (CQS), which enables simple yet efficient implementations of a wide range of fair and abortable synchronization primitives: mutexes, semaphores, barriers, count-down latches, and blocking pools. Our main contribution is algorithmic, as implementing both fairness and abortability efficiently at this level of generality is non-trivial. Importantly, all our algorithms, including the CQS framework and the primitives built on top of it, come with formal proofs in the Iris framework for Coq for many of their properties. These proofs are modular, so it is easy to show correctness for new primitives implemented on top of CQS. From a practical perspective, implementation of CQS for native threads on the JVM improves throughput by up to two orders of magnitude over Java’s AbstractQueuedSynchronizer, the only practical abstraction offering similar semantics. Further, we successfully integrated CQS as a core component of the popular Kotlin Coroutines library, validating the framework’s practical impact and expressiveness in a real-world environment. In sum, CancellableQueueSynchronizer is the first framework to combine expressiveness with formal guarantees and solid practical performance. Our approach should be extensible to other languages and families of synchronization primitives.","lang":"eng"}],"type":"journal_article","file":[{"creator":"alisjak","content_type":"application/pdf","file_size":1266773,"access_level":"open_access","file_name":"2023_ACMProgram.Lang._Koval.pdf","success":1,"checksum":"5dba6e73f0ed79adbdae14d165bc2f68","date_updated":"2023-07-03T13:09:39Z","date_created":"2023-07-03T13:09:39Z","file_id":"13187","relation":"main_file"}],"oa_version":"Published Version","intvolume":" 7","ddc":["000"],"status":"public","title":"CQS: A formally-verified framework for fair and abortable synchronization","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"13179"},{"publisher":"Mathematical Sciences Publishers","department":[{"_id":"TiBr"}],"publication_status":"published","year":"2023","volume":16,"date_updated":"2023-07-17T08:39:19Z","date_created":"2023-07-02T22:00:43Z","author":[{"full_name":"Browning, Timothy D","id":"35827D50-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8314-0177","first_name":"Timothy D","last_name":"Browning"},{"full_name":"Lyczak, Julian","id":"3572849A-F248-11E8-B48F-1D18A9856A87","first_name":"Julian","last_name":"Lyczak"},{"full_name":"Sarapin, Roman","last_name":"Sarapin","first_name":"Roman"}],"publication_identifier":{"issn":["1944-4176"],"eissn":["1944-4184"]},"month":"05","quality_controlled":"1","oa":1,"external_id":{"arxiv":["2203.06881"]},"main_file_link":[{"url":"https://arxiv.org/abs/2203.06881","open_access":"1"}],"language":[{"iso":"eng"}],"doi":"10.2140/involve.2023.16.331","type":"journal_article","issue":"2","abstract":[{"text":"We study the density of everywhere locally soluble diagonal quadric surfaces, parameterised by rational points that lie on a split quadric surface","lang":"eng"}],"intvolume":" 16","title":"Local solubility for a family of quadrics over a split quadric surface","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"13180","oa_version":"Preprint","scopus_import":"1","article_processing_charge":"No","day":"26","page":"331-342","article_type":"original","citation":{"chicago":"Browning, Timothy D, Julian Lyczak, and Roman Sarapin. “Local Solubility for a Family of Quadrics over a Split Quadric Surface.” Involve. Mathematical Sciences Publishers, 2023. https://doi.org/10.2140/involve.2023.16.331.","short":"T.D. Browning, J. Lyczak, R. Sarapin, Involve 16 (2023) 331–342.","mla":"Browning, Timothy D., et al. “Local Solubility for a Family of Quadrics over a Split Quadric Surface.” Involve, vol. 16, no. 2, Mathematical Sciences Publishers, 2023, pp. 331–42, doi:10.2140/involve.2023.16.331.","ieee":"T. D. Browning, J. Lyczak, and R. Sarapin, “Local solubility for a family of quadrics over a split quadric surface,” Involve, vol. 16, no. 2. Mathematical Sciences Publishers, pp. 331–342, 2023.","apa":"Browning, T. D., Lyczak, J., & Sarapin, R. (2023). Local solubility for a family of quadrics over a split quadric surface. Involve. Mathematical Sciences Publishers. https://doi.org/10.2140/involve.2023.16.331","ista":"Browning TD, Lyczak J, Sarapin R. 2023. Local solubility for a family of quadrics over a split quadric surface. Involve. 16(2), 331–342.","ama":"Browning TD, Lyczak J, Sarapin R. Local solubility for a family of quadrics over a split quadric surface. Involve. 2023;16(2):331-342. doi:10.2140/involve.2023.16.331"},"publication":"Involve","date_published":"2023-05-26T00:00:00Z"},{"publisher":"EuroCC","department":[{"_id":"ScienComp"}],"publication_status":"accepted","status":"public","ddc":["000"],"title":"Cryo-EM software packages: A sys-admins point of view","_id":"13162","year":"2023","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"file_name":"2023_ASHPC_Elefante.pdf","access_level":"open_access","creator":"dernst","content_type":"application/pdf","file_size":380354,"file_id":"13250","relation":"main_file","date_created":"2023-07-18T09:28:30Z","date_updated":"2023-07-18T09:28:30Z","success":1,"checksum":"0ab6173cd5c5634ed773cd37ff012681"}],"oa_version":"Submitted Version","date_created":"2023-06-23T11:03:18Z","date_updated":"2023-07-18T09:32:16Z","author":[{"last_name":"Elefante","first_name":"Stefano","id":"490F40CE-F248-11E8-B48F-1D18A9856A87","full_name":"Elefante, Stefano"},{"id":"4D0BC184-F248-11E8-B48F-1D18A9856A87","first_name":"Stephan","last_name":"Stadlbauer","full_name":"Stadlbauer, Stephan"},{"last_name":"Alexander","first_name":"Michael F","id":"3A02A8FA-F248-11E8-B48F-1D18A9856A87","full_name":"Alexander, Michael F"},{"id":"45BF87EE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-5621-8100","first_name":"Alois","last_name":"Schlögl","full_name":"Schlögl, Alois"}],"type":"conference_abstract","file_date_updated":"2023-07-18T09:28:30Z","page":"42-42","quality_controlled":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"oa":1,"citation":{"ista":"Elefante S, Stadlbauer S, Alexander MF, Schlögl A. Cryo-EM software packages: A sys-admins point of view. ASHPC23 - Austrian-Slovenian HPC Meeting 2023. ASHPC: Austrian-Slovenian HPC Meeting, 42–42.","apa":"Elefante, S., Stadlbauer, S., Alexander, M. F., & Schlögl, A. (n.d.). Cryo-EM software packages: A sys-admins point of view. In ASHPC23 - Austrian-Slovenian HPC Meeting 2023 (pp. 42–42). Maribor, Slovenia: EuroCC.","ieee":"S. Elefante, S. Stadlbauer, M. F. Alexander, and A. Schlögl, “Cryo-EM software packages: A sys-admins point of view,” in ASHPC23 - Austrian-Slovenian HPC Meeting 2023, Maribor, Slovenia, pp. 42–42.","ama":"Elefante S, Stadlbauer S, Alexander MF, Schlögl A. Cryo-EM software packages: A sys-admins point of view. In: ASHPC23 - Austrian-Slovenian HPC Meeting 2023. EuroCC; :42-42.","chicago":"Elefante, Stefano, Stephan Stadlbauer, Michael F Alexander, and Alois Schlögl. “Cryo-EM Software Packages: A Sys-Admins Point of View.” In ASHPC23 - Austrian-Slovenian HPC Meeting 2023, 42–42. EuroCC, n.d.","mla":"Elefante, Stefano, et al. “Cryo-EM Software Packages: A Sys-Admins Point of View.” ASHPC23 - Austrian-Slovenian HPC Meeting 2023, EuroCC, pp. 42–42.","short":"S. Elefante, S. Stadlbauer, M.F. Alexander, A. Schlögl, in:, ASHPC23 - Austrian-Slovenian HPC Meeting 2023, EuroCC, n.d., pp. 42–42."},"publication":"ASHPC23 - Austrian-Slovenian HPC Meeting 2023","language":[{"iso":"eng"}],"date_published":"2023-07-01T00:00:00Z","conference":{"location":"Maribor, Slovenia","start_date":"2023-06-12","end_date":"2023-06-15","name":"ASHPC: Austrian-Slovenian HPC Meeting"},"has_accepted_license":"1","article_processing_charge":"No","month":"07","day":"01"},{"quality_controlled":"1","oa":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"language":[{"iso":"eng"}],"conference":{"start_date":"2023-06-13","location":"Maribor, Slovenia","end_date":"2023-06-15","name":"ASHPC: Austrian-Slovenian HPC Meeting"},"month":"07","publication_status":"inpress","department":[{"_id":"ScienComp"},{"_id":"EM-Fac"}],"publisher":"EuroCC","acknowledgement":"Thanks to Jesse Hansen for his suggestions on improving the abstract.","year":"2023","date_updated":"2023-07-18T09:30:54Z","date_created":"2023-06-23T11:01:23Z","author":[{"full_name":"Schlögl, Alois","last_name":"Schlögl","first_name":"Alois","orcid":"0000-0002-5621-8100","id":"45BF87EE-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Elefante, Stefano","id":"490F40CE-F248-11E8-B48F-1D18A9856A87","first_name":"Stefano","last_name":"Elefante"},{"full_name":"Hodirnau, Victor-Valentin","first_name":"Victor-Valentin","last_name":"Hodirnau","id":"3661B498-F248-11E8-B48F-1D18A9856A87"}],"file_date_updated":"2023-07-18T09:18:55Z","page":"59-59","publication":"ASHPC23 - Austrian-Slovenian HPC Meeting 2023","citation":{"mla":"Schlögl, Alois, et al. “Running Windows-Applications on a Linux HPC Cluster Using WINE.” ASHPC23 - Austrian-Slovenian HPC Meeting 2023, EuroCC, pp. 59–59.","short":"A. Schlögl, S. Elefante, V.-V. Hodirnau, in:, ASHPC23 - Austrian-Slovenian HPC Meeting 2023, EuroCC, n.d., pp. 59–59.","chicago":"Schlögl, Alois, Stefano Elefante, and Victor-Valentin Hodirnau. “Running Windows-Applications on a Linux HPC Cluster Using WINE.” In ASHPC23 - Austrian-Slovenian HPC Meeting 2023, 59–59. EuroCC, n.d.","ama":"Schlögl A, Elefante S, Hodirnau V-V. Running Windows-applications on a Linux HPC cluster using WINE. In: ASHPC23 - Austrian-Slovenian HPC Meeting 2023. EuroCC; :59-59.","ista":"Schlögl A, Elefante S, Hodirnau V-V. Running Windows-applications on a Linux HPC cluster using WINE. ASHPC23 - Austrian-Slovenian HPC Meeting 2023. ASHPC: Austrian-Slovenian HPC Meeting, 59–59.","ieee":"A. Schlögl, S. Elefante, and V.-V. Hodirnau, “Running Windows-applications on a Linux HPC cluster using WINE,” in ASHPC23 - Austrian-Slovenian HPC Meeting 2023, Maribor, Slovenia, pp. 59–59.","apa":"Schlögl, A., Elefante, S., & Hodirnau, V.-V. (n.d.). Running Windows-applications on a Linux HPC cluster using WINE. In ASHPC23 - Austrian-Slovenian HPC Meeting 2023 (pp. 59–59). Maribor, Slovenia: EuroCC."},"date_published":"2023-07-01T00:00:00Z","day":"01","article_processing_charge":"No","has_accepted_license":"1","status":"public","ddc":["000"],"title":"Running Windows-applications on a Linux HPC cluster using WINE","_id":"13161","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Submitted Version","file":[{"file_size":316959,"content_type":"application/pdf","creator":"dernst","access_level":"open_access","file_name":"2023_ASHPC_Schloegl.pdf","checksum":"ec8e4295d54171032cdd1b01423eb4a6","success":1,"date_updated":"2023-07-18T09:18:55Z","date_created":"2023-07-18T09:18:55Z","relation":"main_file","file_id":"13249"}],"type":"conference_abstract"}]