[{"has_accepted_license":"1","article_processing_charge":"No","day":"21","scopus_import":"1","date_published":"2023-04-21T00:00:00Z","citation":{"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.","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.","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.","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.","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.","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","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"},"publication":"26th International Conference Foundations of Software Science and Computation Structures","page":"349-370","abstract":[{"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.","lang":"eng"}],"type":"conference","alternative_title":["LNCS"],"file":[{"access_level":"open_access","file_name":"qsl.pdf","creator":"esarac","content_type":"application/pdf","file_size":449027,"file_id":"12468","relation":"main_file","success":1,"checksum":"981025aed580b6b27c426cb8856cf63e","date_updated":"2023-01-31T07:22:21Z","date_created":"2023-01-31T07:22:21Z"},{"file_name":"2023_LNCS_HenzingerT.pdf","access_level":"open_access","creator":"dernst","content_type":"application/pdf","file_size":1048171,"file_id":"13153","relation":"main_file","date_created":"2023-06-19T10:28:09Z","date_updated":"2023-06-19T10:28:09Z","success":1,"checksum":"f16e2af1e0eb243158ab0f0fe74e7d5a"}],"oa_version":"Published Version","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","_id":"12467","intvolume":" 13992","title":"Quantitative safety and liveness","ddc":["000"],"status":"public","publication_identifier":{"issn":["0302-9743"],"isbn":["9783031308284"],"eissn":["1611-3349"]},"month":"04","doi":"10.1007/978-3-031-30829-1_17","conference":{"end_date":"2023-04-27","start_date":"2023-04-22","location":"Paris, France","name":"FOSSACS: Foundations of Software Science and Computation Structures"},"language":[{"iso":"eng"}],"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"},"external_id":{"arxiv":["2301.11175"]},"project":[{"grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software"}],"quality_controlled":"1","ec_funded":1,"file_date_updated":"2023-06-19T10:28:09Z","author":[{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724"},{"first_name":"Nicolas Adrien","last_name":"Mazzocchi","id":"b26baa86-3308-11ec-87b0-8990f34baa85","full_name":"Mazzocchi, Nicolas Adrien"},{"full_name":"Sarac, Naci E","last_name":"Sarac","first_name":"Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425"}],"volume":13992,"date_created":"2023-01-31T07:23:56Z","date_updated":"2023-07-14T11:20:27Z","year":"2023","acknowledgement":"We thank the anonymous reviewers for their helpful comments. This work was supported in part by the ERC-2020-AdG 101020093.","publisher":"Springer Nature","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"publication_status":"published"},{"doi":"10.1145/3591230","language":[{"iso":"eng"}],"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"},"quality_controlled":"1","publication_identifier":{"eissn":["2475-1421"]},"month":"06","author":[{"full_name":"Koval, Nikita","id":"2F4DB10C-F248-11E8-B48F-1D18A9856A87","last_name":"Koval","first_name":"Nikita"},{"last_name":"Khalanskiy","first_name":"Dmitry","full_name":"Khalanskiy, Dmitry"},{"full_name":"Alistarh, Dan-Adrian","last_name":"Alistarh","first_name":"Dan-Adrian","orcid":"0000-0003-3650-940X","id":"4A899BFC-F248-11E8-B48F-1D18A9856A87"}],"volume":7,"date_updated":"2023-07-17T08:43:19Z","date_created":"2023-07-02T22:00:43Z","year":"2023","department":[{"_id":"DaAl"}],"publisher":"Association for Computing Machinery ","publication_status":"published","file_date_updated":"2023-07-03T13:09:39Z","article_number":"116","date_published":"2023-06-06T00:00:00Z","citation":{"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.","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).","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","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"},"publication":"Proceedings of the ACM on Programming Languages","article_type":"original","article_processing_charge":"No","has_accepted_license":"1","day":"06","scopus_import":"1","oa_version":"Published Version","file":[{"relation":"main_file","file_id":"13187","checksum":"5dba6e73f0ed79adbdae14d165bc2f68","success":1,"date_updated":"2023-07-03T13:09:39Z","date_created":"2023-07-03T13:09:39Z","access_level":"open_access","file_name":"2023_ACMProgram.Lang._Koval.pdf","file_size":1266773,"content_type":"application/pdf","creator":"alisjak"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"13179","intvolume":" 7","title":"CQS: A formally-verified framework for fair and abortable synchronization","ddc":["000"],"status":"public","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"},{"publication_status":"published","department":[{"_id":"TiBr"}],"publisher":"Mathematical Sciences Publishers","year":"2023","date_created":"2023-07-02T22:00:43Z","date_updated":"2023-07-17T08:39:19Z","volume":16,"author":[{"full_name":"Browning, Timothy D","orcid":"0000-0002-8314-0177","id":"35827D50-F248-11E8-B48F-1D18A9856A87","last_name":"Browning","first_name":"Timothy D"},{"last_name":"Lyczak","first_name":"Julian","id":"3572849A-F248-11E8-B48F-1D18A9856A87","full_name":"Lyczak, Julian"},{"last_name":"Sarapin","first_name":"Roman","full_name":"Sarapin, Roman"}],"quality_controlled":"1","oa":1,"external_id":{"arxiv":["2203.06881"]},"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2203.06881"}],"language":[{"iso":"eng"}],"doi":"10.2140/involve.2023.16.331","month":"05","publication_identifier":{"eissn":["1944-4184"],"issn":["1944-4176"]},"status":"public","title":"Local solubility for a family of quadrics over a split quadric surface","intvolume":" 16","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"13180","oa_version":"Preprint","type":"journal_article","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"}],"issue":"2","article_type":"original","page":"331-342","publication":"Involve","citation":{"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.","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","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.","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","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.","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.","short":"T.D. Browning, J. Lyczak, R. Sarapin, Involve 16 (2023) 331–342."},"date_published":"2023-05-26T00:00:00Z","scopus_import":"1","day":"26","article_processing_charge":"No"},{"language":[{"iso":"eng"}],"conference":{"name":"ASHPC: Austrian-Slovenian HPC Meeting","start_date":"2023-06-12","location":"Maribor, Slovenia","end_date":"2023-06-15"},"date_published":"2023-07-01T00:00:00Z","quality_controlled":"1","page":"42-42","publication":"ASHPC23 - Austrian-Slovenian HPC Meeting 2023","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":{"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.","short":"S. Elefante, S. Stadlbauer, M.F. Alexander, A. Schlögl, in:, ASHPC23 - Austrian-Slovenian HPC Meeting 2023, EuroCC, n.d., pp. 42–42.","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.","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.","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.","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.","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."},"month":"07","day":"01","article_processing_charge":"No","has_accepted_license":"1","date_created":"2023-06-23T11:03:18Z","date_updated":"2023-07-18T09:32:16Z","file":[{"date_created":"2023-07-18T09:28:30Z","date_updated":"2023-07-18T09:28:30Z","checksum":"0ab6173cd5c5634ed773cd37ff012681","success":1,"relation":"main_file","file_id":"13250","file_size":380354,"content_type":"application/pdf","creator":"dernst","file_name":"2023_ASHPC_Elefante.pdf","access_level":"open_access"}],"oa_version":"Submitted Version","author":[{"id":"490F40CE-F248-11E8-B48F-1D18A9856A87","first_name":"Stefano","last_name":"Elefante","full_name":"Elefante, Stefano"},{"full_name":"Stadlbauer, Stephan","first_name":"Stephan","last_name":"Stadlbauer","id":"4D0BC184-F248-11E8-B48F-1D18A9856A87"},{"id":"3A02A8FA-F248-11E8-B48F-1D18A9856A87","first_name":"Michael F","last_name":"Alexander","full_name":"Alexander, Michael F"},{"full_name":"Schlögl, Alois","first_name":"Alois","last_name":"Schlögl","id":"45BF87EE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-5621-8100"}],"title":"Cryo-EM software packages: A sys-admins point of view","status":"public","publication_status":"accepted","ddc":["000"],"department":[{"_id":"ScienComp"}],"publisher":"EuroCC","year":"2023","_id":"13162","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file_date_updated":"2023-07-18T09:28:30Z","type":"conference_abstract"},{"publication_status":"inpress","department":[{"_id":"ScienComp"},{"_id":"EM-Fac"}],"publisher":"EuroCC","year":"2023","acknowledgement":"Thanks to Jesse Hansen for his suggestions on improving the abstract.","date_updated":"2023-07-18T09:30:54Z","date_created":"2023-06-23T11:01:23Z","author":[{"full_name":"Schlögl, Alois","first_name":"Alois","last_name":"Schlögl","id":"45BF87EE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-5621-8100"},{"id":"490F40CE-F248-11E8-B48F-1D18A9856A87","first_name":"Stefano","last_name":"Elefante","full_name":"Elefante, Stefano"},{"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","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":{"end_date":"2023-06-15","location":"Maribor, Slovenia","start_date":"2023-06-13","name":"ASHPC: Austrian-Slovenian HPC Meeting"},"month":"07","ddc":["000"],"status":"public","title":"Running Windows-applications on a Linux HPC cluster using WINE","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"13161","file":[{"file_id":"13249","relation":"main_file","date_updated":"2023-07-18T09:18:55Z","date_created":"2023-07-18T09:18:55Z","success":1,"checksum":"ec8e4295d54171032cdd1b01423eb4a6","file_name":"2023_ASHPC_Schloegl.pdf","access_level":"open_access","creator":"dernst","file_size":316959,"content_type":"application/pdf"}],"oa_version":"Submitted Version","type":"conference_abstract","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.","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.","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."},"date_published":"2023-07-01T00:00:00Z","day":"01","has_accepted_license":"1","article_processing_charge":"No"},{"date_published":"2023-07-05T00:00:00Z","article_type":"original","page":"6309-6314","publication":"The Journal of Physical Chemistry Letters","citation":{"chicago":"Wei, Yujing, Artem Volosniev, Dusan Lorenc, Ayan A. Zhumekenov, Osman M. Bakr, Mikhail Lemeshko, and Zhanybek Alpichshev. “Bond Polarizability as a Probe of Local Crystal Fields in Hybrid Lead-Halide Perovskites.” The Journal of Physical Chemistry Letters. American Chemical Society, 2023. https://doi.org/10.1021/acs.jpclett.3c01158.","mla":"Wei, Yujing, et al. “Bond Polarizability as a Probe of Local Crystal Fields in Hybrid Lead-Halide Perovskites.” The Journal of Physical Chemistry Letters, vol. 14, no. 27, American Chemical Society, 2023, pp. 6309–14, doi:10.1021/acs.jpclett.3c01158.","short":"Y. Wei, A. Volosniev, D. Lorenc, A.A. Zhumekenov, O.M. Bakr, M. Lemeshko, Z. Alpichshev, The Journal of Physical Chemistry Letters 14 (2023) 6309–6314.","ista":"Wei Y, Volosniev A, Lorenc D, Zhumekenov AA, Bakr OM, Lemeshko M, Alpichshev Z. 2023. Bond polarizability as a probe of local crystal fields in hybrid lead-halide perovskites. The Journal of Physical Chemistry Letters. 14(27), 6309–6314.","apa":"Wei, Y., Volosniev, A., Lorenc, D., Zhumekenov, A. A., Bakr, O. M., Lemeshko, M., & Alpichshev, Z. (2023). Bond polarizability as a probe of local crystal fields in hybrid lead-halide perovskites. The Journal of Physical Chemistry Letters. American Chemical Society. https://doi.org/10.1021/acs.jpclett.3c01158","ieee":"Y. Wei et al., “Bond polarizability as a probe of local crystal fields in hybrid lead-halide perovskites,” The Journal of Physical Chemistry Letters, vol. 14, no. 27. American Chemical Society, pp. 6309–6314, 2023.","ama":"Wei Y, Volosniev A, Lorenc D, et al. Bond polarizability as a probe of local crystal fields in hybrid lead-halide perovskites. The Journal of Physical Chemistry Letters. 2023;14(27):6309-6314. doi:10.1021/acs.jpclett.3c01158"},"day":"05","article_processing_charge":"Yes (via OA deal)","has_accepted_license":"1","keyword":["General Materials Science","Physical and Theoretical Chemistry"],"oa_version":"Published Version","file":[{"file_id":"13253","relation":"main_file","date_updated":"2023-07-19T06:55:39Z","date_created":"2023-07-19T06:55:39Z","success":1,"checksum":"c0c040063f06a51b9c463adc504f1a23","file_name":"2023_JourPhysChemistry_Wei.pdf","access_level":"open_access","creator":"dernst","file_size":2121252,"content_type":"application/pdf"}],"title":"Bond polarizability as a probe of local crystal fields in hybrid lead-halide perovskites","status":"public","ddc":["530"],"intvolume":" 14","_id":"13251","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"text":"A rotating organic cation and a dynamically disordered soft inorganic cage are the hallmark features of organic-inorganic lead-halide perovskites. Understanding the interplay between these two subsystems is a challenging problem, but it is this coupling that is widely conjectured to be responsible for the unique behavior of photocarriers in these materials. In this work, we use the fact that the polarizability of the organic cation strongly depends on the ambient electrostatic environment to put the molecule forward as a sensitive probe of the local crystal fields inside the lattice cell. We measure the average polarizability of the C/N–H bond stretching mode by means of infrared spectroscopy, which allows us to deduce the character of the motion of the cation molecule, find the magnitude of the local crystal field, and place an estimate on the strength of the hydrogen bond between the hydrogen and halide atoms. Our results pave the way for understanding electric fields in lead-halide perovskites using infrared bond spectroscopy.","lang":"eng"}],"issue":"27","type":"journal_article","language":[{"iso":"eng"}],"doi":"10.1021/acs.jpclett.3c01158","isi":1,"quality_controlled":"1","project":[{"name":"Angulon: physics and applications of a new quasiparticle","call_identifier":"H2020","_id":"2688CF98-B435-11E9-9278-68D0E5697425","grant_number":"801770"}],"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":["2304.14198"],"isi":["001022811500001"]},"month":"07","publication_identifier":{"eissn":["1948-7185"]},"date_updated":"2023-07-19T06:59:19Z","date_created":"2023-07-18T11:13:17Z","volume":14,"author":[{"full_name":"Wei, Yujing","id":"0c5ff007-2600-11ee-b896-98bd8d663294","orcid":"0000-0001-8913-9719","first_name":"Yujing","last_name":"Wei"},{"orcid":"0000-0003-0393-5525","id":"37D278BC-F248-11E8-B48F-1D18A9856A87","last_name":"Volosniev","first_name":"Artem","full_name":"Volosniev, Artem"},{"full_name":"Lorenc, Dusan","id":"40D8A3E6-F248-11E8-B48F-1D18A9856A87","first_name":"Dusan","last_name":"Lorenc"},{"last_name":"Zhumekenov","first_name":"Ayan A.","full_name":"Zhumekenov, Ayan A."},{"first_name":"Osman M.","last_name":"Bakr","full_name":"Bakr, Osman M."},{"id":"37CB05FA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-6990-7802","first_name":"Mikhail","last_name":"Lemeshko","full_name":"Lemeshko, Mikhail"},{"full_name":"Alpichshev, Zhanybek","first_name":"Zhanybek","last_name":"Alpichshev","id":"45E67A2A-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-7183-5203"}],"publication_status":"published","department":[{"_id":"MiLe"},{"_id":"ZhAl"}],"publisher":"American Chemical Society","acknowledgement":"We thank Bingqing Cheng and Hong-Zhou Ye for valuable discussions; Y.W.’s work at IST Austria was supported through ISTernship summer internship program funded by OeADGmbH; D.L. and Z.A. acknowledge support by IST Austria (ISTA); M.L. acknowledges support by the European Research Council (ERC) Starting Grant No. 801770 (ANGULON).\r\nA.A.Z. and O.M.B. acknowledge support by KAUST.","year":"2023","file_date_updated":"2023-07-19T06:55:39Z","ec_funded":1},{"type":"conference","alternative_title":["LIPIcs"],"abstract":[{"text":"The operator precedence languages (OPLs) represent the largest known subclass of the context-free languages which enjoys all desirable closure and decidability properties. This includes the decidability of language inclusion, which is the ultimate verification problem. Operator precedence grammars, automata, and logics have been investigated and used, for example, to verify programs with arithmetic expressions and exceptions (both of which are deterministic pushdown but lie outside the scope of the visibly pushdown languages). In this paper, we complete the picture and give, for the first time, an algebraic characterization of the class of OPLs in the form of a syntactic congruence that has finitely many equivalence classes exactly for the operator precedence languages. This is a generalization of the celebrated Myhill-Nerode theorem for the regular languages to OPLs. As one of the consequences, we show that universality and language inclusion for nondeterministic operator precedence automata can be solved by an antichain algorithm. Antichain algorithms avoid determinization and complementation through an explicit subset construction, by leveraging a quasi-order on words, which allows the pruning of the search space for counterexample words without sacrificing completeness. Antichain algorithms can be implemented symbolically, and these implementations are today the best-performing algorithms in practice for the inclusion of finite automata. We give a generic construction of the quasi-order needed for antichain algorithms from a finite syntactic congruence. This yields the first antichain algorithm for OPLs, an algorithm that solves the ExpTime-hard language inclusion problem for OPLs in exponential time.","lang":"eng"}],"_id":"13292","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":" 261","ddc":["000"],"status":"public","title":"Regular methods for operator precedence languages","oa_version":"Published Version","file":[{"file_name":"icalp23.pdf","access_level":"open_access","creator":"esarac","file_size":859379,"content_type":"application/pdf","file_id":"13293","relation":"main_file","date_created":"2023-07-24T15:11:05Z","date_updated":"2023-07-24T15:11:05Z","success":1,"checksum":"5d4c8932ef3450615a53b9bb15d92eb2"}],"has_accepted_license":"1","article_processing_charge":"Yes","day":"05","citation":{"ama":"Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. Regular methods for operator precedence languages. In: 50th International Colloquium on Automata, Languages, and Programming. Vol 261. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023:129:1--129:20. doi:10.4230/LIPIcs.ICALP.2023.129","ista":"Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. 2023. Regular methods for operator precedence languages. 50th International Colloquium on Automata, Languages, and Programming. ICALP: International Colloquium on Automata, Languages, and Programming, LIPIcs, vol. 261, 129:1--129:20.","ieee":"T. A. Henzinger, P. Kebis, N. A. Mazzocchi, and N. E. Sarac, “Regular methods for operator precedence languages,” in 50th International Colloquium on Automata, Languages, and Programming, Paderborn, Germany, 2023, vol. 261, p. 129:1--129:20.","apa":"Henzinger, T. A., Kebis, P., Mazzocchi, N. A., & Sarac, N. E. (2023). Regular methods for operator precedence languages. In 50th International Colloquium on Automata, Languages, and Programming (Vol. 261, p. 129:1--129:20). Paderborn, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.ICALP.2023.129","mla":"Henzinger, Thomas A., et al. “Regular Methods for Operator Precedence Languages.” 50th International Colloquium on Automata, Languages, and Programming, vol. 261, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, p. 129:1--129:20, doi:10.4230/LIPIcs.ICALP.2023.129.","short":"T.A. Henzinger, P. Kebis, N.A. Mazzocchi, N.E. Sarac, in:, 50th International Colloquium on Automata, Languages, and Programming, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, p. 129:1--129:20.","chicago":"Henzinger, Thomas A, Pavol Kebis, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Regular Methods for Operator Precedence Languages.” In 50th International Colloquium on Automata, Languages, and Programming, 261:129:1--129:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. https://doi.org/10.4230/LIPIcs.ICALP.2023.129."},"publication":"50th International Colloquium on Automata, Languages, and Programming","page":"129:1--129:20","date_published":"2023-07-05T00:00:00Z","ec_funded":1,"file_date_updated":"2023-07-24T15:11:05Z","year":"2023","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093.\r\nWe thank Pierre Ganty for early discussions and the anonymous reviewers for their helpful comments.\r\n","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"publication_status":"published","author":[{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724"},{"last_name":"Kebis","first_name":"Pavol","full_name":"Kebis, Pavol"},{"full_name":"Mazzocchi, Nicolas Adrien","id":"b26baa86-3308-11ec-87b0-8990f34baa85","last_name":"Mazzocchi","first_name":"Nicolas Adrien"},{"last_name":"Sarac","first_name":"Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","full_name":"Sarac, Naci E"}],"volume":261,"date_updated":"2023-07-31T08:38:38Z","date_created":"2023-07-24T15:11:41Z","publication_identifier":{"isbn":["9783959772785"],"eissn":["1868-8969"]},"month":"07","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":["2305.03447"]},"project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"quality_controlled":"1","doi":"10.4230/LIPIcs.ICALP.2023.129","conference":{"name":"ICALP: International Colloquium on Automata, Languages, and Programming","start_date":"2023-07-10","location":"Paderborn, Germany","end_date":"2023-07-14"},"language":[{"iso":"eng"}]},{"publication_identifier":{"issn":["2666-9366"]},"month":"04","doi":"10.21468/scipostphyscore.6.2.029","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"},"external_id":{"arxiv":["2211.01923"]},"oa":1,"project":[{"name":"ISTplus - Postdoctoral Fellowships","call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425","grant_number":"754411"}],"quality_controlled":"1","ec_funded":1,"file_date_updated":"2023-07-31T09:02:27Z","article_number":"029","author":[{"last_name":"Tucci","first_name":"Gennaro","full_name":"Tucci, Gennaro"},{"full_name":"De Nicola, Stefano","first_name":"Stefano","last_name":"De Nicola","id":"42832B76-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4842-6671"},{"last_name":"Wald","first_name":"Sascha","full_name":"Wald, Sascha"},{"first_name":"Andrea","last_name":"Gambassi","full_name":"Gambassi, Andrea"}],"volume":6,"date_created":"2023-07-24T10:47:46Z","date_updated":"2023-07-31T09:03:28Z","year":"2023","acknowledgement":"S. De Nicola acknowledges funding from the Institute of Science and Technology Austria (ISTA), and from the European Union’s Horizon 2020 research and innovation program under the Marie Skłodowska-Curie Grant Agreement No. 754411. S. De Nicola also acknowledges funding from the EPSRC Center for Doctoral Training in Cross-Disciplinary Approaches to NonEquilibrium Systems (CANES) under Grant EP/L015854/1. ","publisher":"SciPost Foundation","department":[{"_id":"MaSe"}],"publication_status":"published","has_accepted_license":"1","article_processing_charge":"No","day":"14","keyword":["Statistical and Nonlinear Physics","Atomic and Molecular Physics","and Optics","Nuclear and High Energy Physics","Condensed Matter Physics"],"date_published":"2023-04-14T00:00:00Z","citation":{"ama":"Tucci G, De Nicola S, Wald S, Gambassi A. Stochastic representation of the quantum quartic oscillator. SciPost Physics Core. 2023;6(2). doi:10.21468/scipostphyscore.6.2.029","apa":"Tucci, G., De Nicola, S., Wald, S., & Gambassi, A. (2023). Stochastic representation of the quantum quartic oscillator. SciPost Physics Core. SciPost Foundation. https://doi.org/10.21468/scipostphyscore.6.2.029","ieee":"G. Tucci, S. De Nicola, S. Wald, and A. Gambassi, “Stochastic representation of the quantum quartic oscillator,” SciPost Physics Core, vol. 6, no. 2. SciPost Foundation, 2023.","ista":"Tucci G, De Nicola S, Wald S, Gambassi A. 2023. Stochastic representation of the quantum quartic oscillator. SciPost Physics Core. 6(2), 029.","short":"G. Tucci, S. De Nicola, S. Wald, A. Gambassi, SciPost Physics Core 6 (2023).","mla":"Tucci, Gennaro, et al. “Stochastic Representation of the Quantum Quartic Oscillator.” SciPost Physics Core, vol. 6, no. 2, 029, SciPost Foundation, 2023, doi:10.21468/scipostphyscore.6.2.029.","chicago":"Tucci, Gennaro, Stefano De Nicola, Sascha Wald, and Andrea Gambassi. “Stochastic Representation of the Quantum Quartic Oscillator.” SciPost Physics Core. SciPost Foundation, 2023. https://doi.org/10.21468/scipostphyscore.6.2.029."},"publication":"SciPost Physics Core","article_type":"original","issue":"2","abstract":[{"lang":"eng","text":"Recent experimental advances have inspired the development of theoretical tools to describe the non-equilibrium dynamics of quantum systems. Among them an exact representation of quantum spin systems in terms of classical stochastic processes has been proposed. Here we provide first steps towards the extension of this stochastic approach to bosonic systems by considering the one-dimensional quantum quartic oscillator. We show how to exactly parameterize the time evolution of this prototypical model via the dynamics of a set of classical variables. We interpret these variables as stochastic processes, which allows us to propose a novel way to numerically simulate the time evolution of the system. We benchmark our findings by considering analytically solvable limits and providing alternative derivations of known results."}],"type":"journal_article","file":[{"date_updated":"2023-07-31T09:02:27Z","date_created":"2023-07-31T09:02:27Z","success":1,"checksum":"b472bc82108747eda5d52adf9e2ac7f3","file_id":"13329","relation":"main_file","creator":"dernst","content_type":"application/pdf","file_size":523236,"file_name":"2023_SciPostPhysCore_Tucci.pdf","access_level":"open_access"}],"oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"13277","intvolume":" 6","title":"Stochastic representation of the quantum quartic oscillator","ddc":["530"],"status":"public"},{"doi":"10.21468/scipostphyscodeb.12","language":[{"iso":"eng"}],"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"},"external_id":{"arxiv":["2202.04603"]},"quality_controlled":"1","project":[{"grant_number":"754411","_id":"260C2330-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","name":"ISTplus - Postdoctoral Fellowships"}],"month":"04","publication_identifier":{"issn":["2949-804X"]},"author":[{"full_name":"Rammelmüller, Lukas","first_name":"Lukas","last_name":"Rammelmüller"},{"first_name":"David","last_name":"Huber","full_name":"Huber, David"},{"id":"37D278BC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-0393-5525","first_name":"Artem","last_name":"Volosniev","full_name":"Volosniev, Artem"}],"related_material":{"record":[{"id":"13275","status":"public","relation":"research_data"}]},"date_updated":"2023-07-31T09:16:02Z","date_created":"2023-07-24T10:47:15Z","acknowledgement":"We acknowledge fruitful discussions with Hans-Werner Hammer and thank Gerhard Zürn and\r\nPietro Massignan for sending us their data. We thank Fabian Brauneis for beta-testing the\r\nprovided code-package, and comments on the manuscript.\r\nL.R. is supported by FP7/ERC Consolidator Grant QSIMCORR, No.\r\n771891, and the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) under\r\nGermany’s Excellence Strategy –EXC–2111–390814868. A.G.V. acknowledges support\r\nby European Union’s Horizon 2020 research and innovation programme under the Marie\r\nSkłodowska-Curie Grant Agreement No. 754411.","year":"2023","publication_status":"published","department":[{"_id":"MiLe"}],"publisher":"SciPost Foundation","file_date_updated":"2023-07-31T09:09:23Z","ec_funded":1,"article_number":"12","date_published":"2023-04-19T00:00:00Z","publication":"SciPost Physics Codebases","citation":{"apa":"Rammelmüller, L., Huber, D., & Volosniev, A. (2023). A modular implementation of an effective interaction approach for harmonically trapped fermions in 1D. SciPost Physics Codebases. SciPost Foundation. https://doi.org/10.21468/scipostphyscodeb.12","ieee":"L. Rammelmüller, D. Huber, and A. Volosniev, “A modular implementation of an effective interaction approach for harmonically trapped fermions in 1D,” SciPost Physics Codebases. SciPost Foundation, 2023.","ista":"Rammelmüller L, Huber D, Volosniev A. 2023. A modular implementation of an effective interaction approach for harmonically trapped fermions in 1D. SciPost Physics Codebases., 12.","ama":"Rammelmüller L, Huber D, Volosniev A. A modular implementation of an effective interaction approach for harmonically trapped fermions in 1D. SciPost Physics Codebases. 2023. doi:10.21468/scipostphyscodeb.12","chicago":"Rammelmüller, Lukas, David Huber, and Artem Volosniev. “A Modular Implementation of an Effective Interaction Approach for Harmonically Trapped Fermions in 1D.” SciPost Physics Codebases. SciPost Foundation, 2023. https://doi.org/10.21468/scipostphyscodeb.12.","short":"L. Rammelmüller, D. Huber, A. Volosniev, SciPost Physics Codebases (2023).","mla":"Rammelmüller, Lukas, et al. “A Modular Implementation of an Effective Interaction Approach for Harmonically Trapped Fermions in 1D.” SciPost Physics Codebases, 12, SciPost Foundation, 2023, doi:10.21468/scipostphyscodeb.12."},"article_type":"original","day":"19","has_accepted_license":"1","article_processing_charge":"No","file":[{"success":1,"checksum":"f583a70fe915d2208c803f5afb426daa","date_created":"2023-07-31T09:09:23Z","date_updated":"2023-07-31T09:09:23Z","file_id":"13330","relation":"main_file","creator":"dernst","content_type":"application/pdf","file_size":551418,"access_level":"open_access","file_name":"2023_SciPostPhysCodebase_Rammelmueller.pdf"}],"oa_version":"Published Version","_id":"13276","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["530"],"title":"A modular implementation of an effective interaction approach for harmonically trapped fermions in 1D","status":"public","abstract":[{"lang":"eng","text":"We introduce a generic and accessible implementation of an exact diagonalization method for studying few-fermion models. Our aim is to provide a testbed for the newcomers to the field as well as a stepping stone for trying out novel optimizations and approximations. This userguide consists of a description of the algorithm, and several examples in varying orders of sophistication. In particular, we exemplify our routine using an effective-interaction approach that fixes the low-energy physics. We benchmark this approach against the existing data, and show that it is able to deliver state-of-the-art numerical results at a significantly reduced computational cost."}],"type":"journal_article"},{"related_material":{"record":[{"id":"13276","relation":"used_in_publication","status":"public"}]},"author":[{"full_name":"Rammelmüller, Lukas","last_name":"Rammelmüller","first_name":"Lukas"},{"full_name":"Huber, David","first_name":"David","last_name":"Huber"},{"full_name":"Volosniev, Artem","last_name":"Volosniev","first_name":"Artem","orcid":"0000-0003-0393-5525","id":"37D278BC-F248-11E8-B48F-1D18A9856A87"}],"oa_version":"Published Version","date_updated":"2023-07-31T09:16:02Z","date_created":"2023-07-24T10:46:23Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"13275","year":"2023","department":[{"_id":"MiLe"}],"publisher":"SciPost Foundation","status":"public","ddc":["530"],"title":"Codebase release 1.0 for FermiFCI","ec_funded":1,"abstract":[{"text":"We introduce a generic and accessible implementation of an exact diagonalization method for studying few-fermion models. Our aim is to provide a testbed for the newcomers to the field as well as a stepping stone for trying out novel optimizations and approximations. This userguide consists of a description of the algorithm, and several examples in varying orders of sophistication. In particular, we exemplify our routine using an effective-interaction approach that fixes the low-energy physics. We benchmark this approach against the existing data, and show that it is able to deliver state-of-the-art numerical results at a significantly reduced computational cost.","lang":"eng"}],"type":"research_data_reference","date_published":"2023-04-19T00:00:00Z","doi":"10.21468/scipostphyscodeb.12-r1.0","citation":{"ista":"Rammelmüller L, Huber D, Volosniev A. 2023. Codebase release 1.0 for FermiFCI, SciPost Foundation, 10.21468/scipostphyscodeb.12-r1.0.","ieee":"L. Rammelmüller, D. Huber, and A. Volosniev, “Codebase release 1.0 for FermiFCI.” SciPost Foundation, 2023.","apa":"Rammelmüller, L., Huber, D., & Volosniev, A. (2023). Codebase release 1.0 for FermiFCI. SciPost Foundation. https://doi.org/10.21468/scipostphyscodeb.12-r1.0","ama":"Rammelmüller L, Huber D, Volosniev A. Codebase release 1.0 for FermiFCI. 2023. doi:10.21468/scipostphyscodeb.12-r1.0","chicago":"Rammelmüller, Lukas, David Huber, and Artem Volosniev. “Codebase Release 1.0 for FermiFCI.” SciPost Foundation, 2023. https://doi.org/10.21468/scipostphyscodeb.12-r1.0.","mla":"Rammelmüller, Lukas, et al. Codebase Release 1.0 for FermiFCI. SciPost Foundation, 2023, doi:10.21468/scipostphyscodeb.12-r1.0.","short":"L. Rammelmüller, D. Huber, A. Volosniev, (2023)."},"oa":1,"main_file_link":[{"url":"https://doi.org/10.21468/SciPostPhysCodeb.12-r1.0","open_access":"1"}],"project":[{"grant_number":"754411","_id":"260C2330-B435-11E9-9278-68D0E5697425","name":"ISTplus - Postdoctoral Fellowships","call_identifier":"H2020"}],"article_processing_charge":"No","month":"04","day":"19"}]