[{"has_accepted_license":"1","department":[{"_id":"HeEd"}],"file":[{"success":1,"relation":"main_file","content_type":"application/pdf","file_id":"14740","creator":"dernst","file_size":2370988,"file_name":"2023_IEEEToP_Ali.pdf","checksum":"465c28ef0b151b4b1fb47977ed5581ab","date_created":"2024-01-08T10:09:14Z","access_level":"open_access","date_updated":"2024-01-08T10:09:14Z"}],"date_created":"2024-01-08T09:59:46Z","month":"12","date_published":"2023-12-01T00:00:00Z","article_type":"original","publisher":"IEEE","language":[{"iso":"eng"}],"issue":"12","publication":"IEEE Transactions on Pattern Analysis and Machine Intelligence","page":"14069-14080","file_date_updated":"2024-01-08T10:09:14Z","day":"01","type":"journal_article","intvolume":"        45","status":"public","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"],"year":"2023","doi":"10.1109/tpami.2023.3308391","title":"A survey of vectorization methods in topological data analysis","oa":1,"volume":45,"date_updated":"2024-01-08T10:11:46Z","article_processing_charge":"Yes (in subscription journal)","_id":"14739","publication_identifier":{"issn":["0162-8828"],"eissn":["1939-3539"]},"acknowledgement":"The work of Maria-Jose Jimenez, Eduardo Paluzo-Hidalgo and Manuel Soriano-Trigueros was supported in part by the Spanish grant Ministerio de Ciencia e Innovacion under Grants TED2021-129438B-I00 and PID2019-107339GB-I00, and in part by REXASI-PRO H-EU project, call HORIZON-CL4-2021-HUMAN-01-01 under Grant 101070028. The work of\r\nMaria-Jose Jimenez was supported by a grant of Convocatoria de la Universidad de Sevilla para la recualificacion del sistema universitario español, 2021-23, funded by the European Union, NextGenerationEU. The work of Vidit Nanda was supported in part by EPSRC under Grant EP/R018472/1 and in part by US AFOSR under Grant FA9550-22-1-0462. \r\nWe are grateful to the team of GUDHI and TEASPOON developers, for their work and their support. We are also grateful to Streamlit for providing extra resources to deploy the web app\r\nonline on Streamlit community cloud. We thank the anonymous referees for their helpful suggestions.","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","oa_version":"Published Version","publication_status":"published","citation":{"apa":"Ali, D., Asaad, A., Jimenez, M.-J., Nanda, V., Paluzo-Hidalgo, E., &#38; Soriano Trigueros, M. (2023). A survey of vectorization methods in topological data analysis. <i>IEEE Transactions on Pattern Analysis and Machine Intelligence</i>. IEEE. <a href=\"https://doi.org/10.1109/tpami.2023.3308391\">https://doi.org/10.1109/tpami.2023.3308391</a>","ieee":"D. Ali, A. Asaad, M.-J. Jimenez, V. Nanda, E. Paluzo-Hidalgo, and M. Soriano Trigueros, “A survey of vectorization methods in topological data analysis,” <i>IEEE Transactions on Pattern Analysis and Machine Intelligence</i>, vol. 45, no. 12. IEEE, pp. 14069–14080, 2023.","chicago":"Ali, Dashti, Aras Asaad, Maria-Jose Jimenez, Vidit Nanda, Eduardo Paluzo-Hidalgo, and Manuel Soriano Trigueros. “A Survey of Vectorization Methods in Topological Data Analysis.” <i>IEEE Transactions on Pattern Analysis and Machine Intelligence</i>. IEEE, 2023. <a href=\"https://doi.org/10.1109/tpami.2023.3308391\">https://doi.org/10.1109/tpami.2023.3308391</a>.","mla":"Ali, Dashti, et al. “A Survey of Vectorization Methods in Topological Data Analysis.” <i>IEEE Transactions on Pattern Analysis and Machine Intelligence</i>, vol. 45, no. 12, IEEE, 2023, pp. 14069–80, doi:<a href=\"https://doi.org/10.1109/tpami.2023.3308391\">10.1109/tpami.2023.3308391</a>.","ama":"Ali D, Asaad A, Jimenez M-J, Nanda V, Paluzo-Hidalgo E, Soriano Trigueros M. A survey of vectorization methods in topological data analysis. <i>IEEE Transactions on Pattern Analysis and Machine Intelligence</i>. 2023;45(12):14069-14080. doi:<a href=\"https://doi.org/10.1109/tpami.2023.3308391\">10.1109/tpami.2023.3308391</a>","ista":"Ali D, Asaad A, Jimenez M-J, Nanda V, Paluzo-Hidalgo E, Soriano Trigueros M. 2023. A survey of vectorization methods in topological data analysis. IEEE Transactions on Pattern Analysis and Machine Intelligence. 45(12), 14069–14080.","short":"D. Ali, A. Asaad, M.-J. Jimenez, V. Nanda, E. Paluzo-Hidalgo, M. Soriano Trigueros, IEEE Transactions on Pattern Analysis and Machine Intelligence 45 (2023) 14069–14080."},"abstract":[{"text":"Attempts to incorporate topological information in supervised learning tasks have resulted in the creation of several techniques for vectorizing persistent homology barcodes. In this paper, we study thirteen such methods. Besides describing an organizational framework for these methods, we comprehensively benchmark them against three well-known classification tasks. Surprisingly, we discover that the best-performing method is a simple vectorization, which consists only of a few elementary summary statistics. Finally, we provide a convenient web application which has been designed to facilitate exploration and experimentation with various vectorization methods.","lang":"eng"}],"keyword":["Applied Mathematics","Artificial Intelligence","Computational Theory and Mathematics","Computer Vision and Pattern Recognition","Software"],"author":[{"first_name":"Dashti","last_name":"Ali","full_name":"Ali, Dashti"},{"last_name":"Asaad","full_name":"Asaad, Aras","first_name":"Aras"},{"full_name":"Jimenez, Maria-Jose","last_name":"Jimenez","first_name":"Maria-Jose"},{"first_name":"Vidit","full_name":"Nanda, Vidit","last_name":"Nanda"},{"first_name":"Eduardo","last_name":"Paluzo-Hidalgo","full_name":"Paluzo-Hidalgo, Eduardo"},{"id":"15ebd7cf-15bf-11ee-aebd-bb4bb5121ea8","orcid":"0000-0003-2449-1433","last_name":"Soriano Trigueros","full_name":"Soriano Trigueros, Manuel","first_name":"Manuel"}]},{"issue":"2","publication":"Formal Aspects of Computing","file_date_updated":"2024-01-16T08:11:24Z","intvolume":"        35","status":"public","day":"23","type":"journal_article","file":[{"access_level":"open_access","date_updated":"2024-01-16T08:11:24Z","checksum":"3bb133eeb27ec01649a9a36445d952d9","date_created":"2024-01-16T08:11:24Z","file_size":502522,"file_name":"2023_FormalAspectsComputing_Chatterjee.pdf","creator":"dernst","file_id":"14804","relation":"main_file","content_type":"application/pdf","success":1}],"date_created":"2024-01-10T09:27:43Z","has_accepted_license":"1","department":[{"_id":"KrCh"}],"publisher":"Association for Computing Machinery","language":[{"iso":"eng"}],"month":"06","article_type":"original","date_published":"2023-06-23T00:00:00Z","_id":"14778","publication_identifier":{"eissn":["1433-299X"],"issn":["0934-5043"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","acknowledgement":"This research was partially supported by the ERC CoG (grant no. 863818; ForM-SMArt), the Czech Science Foundation (grant no. GA21-24711S), and the European Union’s Horizon 2020 research and innovation program under the Marie Skłodowska-Curie Grant Agreement No. 665385.","project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"},{"grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","name":"International IST Doctoral Program","call_identifier":"H2020"}],"quality_controlled":"1","oa_version":"Published Version","arxiv":1,"oa":1,"date_updated":"2025-07-14T09:10:10Z","volume":35,"article_processing_charge":"Yes (via OA deal)","abstract":[{"text":"We consider the almost-sure (a.s.) termination problem for probabilistic programs, which are a stochastic extension of classical imperative programs. Lexicographic ranking functions provide a sound and practical approach for termination of non-probabilistic programs, and their extension to probabilistic programs is achieved via lexicographic ranking supermartingales (LexRSMs). However, LexRSMs introduced in the previous work have a limitation that impedes their automation: all of their components have to be non-negative in all reachable states. This might result in a LexRSM not existing even for simple terminating programs. Our contributions are twofold. First, we introduce a generalization of LexRSMs that allows for some components to be negative. This standard feature of non-probabilistic termination proofs was hitherto not known to be sound in the probabilistic setting, as the soundness proof requires a careful analysis of the underlying stochastic process. Second, we present polynomial-time algorithms using our generalized LexRSMs for proving a.s. termination in broad classes of linear-arithmetic programs.","lang":"eng"}],"keyword":["Theoretical Computer Science","Software"],"author":[{"first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ehsan","last_name":"Kafshdar Goharshady","full_name":"Kafshdar Goharshady, Ehsan"},{"id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","first_name":"Petr","last_name":"Novotný","full_name":"Novotný, Petr"},{"full_name":"Zárevúcky, Jiří","last_name":"Zárevúcky","first_name":"Jiří"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic","full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","first_name":"Dorde"}],"publication_status":"published","citation":{"ama":"Chatterjee K, Kafshdar Goharshady E, Novotný P, Zárevúcky J, Zikelic D. On lexicographic proof rules for probabilistic termination. <i>Formal Aspects of Computing</i>. 2023;35(2). doi:<a href=\"https://doi.org/10.1145/3585391\">10.1145/3585391</a>","mla":"Chatterjee, Krishnendu, et al. “On Lexicographic Proof Rules for Probabilistic Termination.” <i>Formal Aspects of Computing</i>, vol. 35, no. 2, 11, Association for Computing Machinery, 2023, doi:<a href=\"https://doi.org/10.1145/3585391\">10.1145/3585391</a>.","ista":"Chatterjee K, Kafshdar Goharshady E, Novotný P, Zárevúcky J, Zikelic D. 2023. On lexicographic proof rules for probabilistic termination. Formal Aspects of Computing. 35(2), 11.","short":"K. Chatterjee, E. Kafshdar Goharshady, P. Novotný, J. Zárevúcky, D. Zikelic, Formal Aspects of Computing 35 (2023).","apa":"Chatterjee, K., Kafshdar Goharshady, E., Novotný, P., Zárevúcky, J., &#38; Zikelic, D. (2023). On lexicographic proof rules for probabilistic termination. <i>Formal Aspects of Computing</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3585391\">https://doi.org/10.1145/3585391</a>","ieee":"K. Chatterjee, E. Kafshdar Goharshady, P. Novotný, J. Zárevúcky, and D. Zikelic, “On lexicographic proof rules for probabilistic termination,” <i>Formal Aspects of Computing</i>, vol. 35, no. 2. Association for Computing Machinery, 2023.","chicago":"Chatterjee, Krishnendu, Ehsan Kafshdar Goharshady, Petr Novotný, Jiří Zárevúcky, and Dorde Zikelic. “On Lexicographic Proof Rules for Probabilistic Termination.” <i>Formal Aspects of Computing</i>. Association for Computing Machinery, 2023. <a href=\"https://doi.org/10.1145/3585391\">https://doi.org/10.1145/3585391</a>."},"related_material":{"record":[{"id":"10414","relation":"earlier_version","status":"public"}]},"ddc":["000"],"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)"},"article_number":"11","external_id":{"arxiv":["2108.02188"]},"title":"On lexicographic proof rules for probabilistic termination","doi":"10.1145/3585391","year":"2023","ec_funded":1},{"article_type":"original","date_published":"2022-10-01T00:00:00Z","month":"10","language":[{"iso":"eng"}],"scopus_import":"1","publisher":"Springer Nature","department":[{"_id":"KrCh"}],"has_accepted_license":"1","date_created":"2022-01-06T12:37:27Z","file":[{"success":1,"content_type":"application/pdf","relation":"main_file","file_id":"10603","creator":"cchlebak","file_name":"2021_ActaInfor_Křetínský.pdf","file_size":1066082,"date_created":"2022-01-07T07:50:31Z","checksum":"bf1c195b6aaf59e8530cf9e3a9d731f7","date_updated":"2022-01-07T07:50:31Z","access_level":"open_access"}],"type":"journal_article","day":"01","status":"public","intvolume":"        59","page":"585-618","file_date_updated":"2022-01-07T07:50:31Z","publication":"Acta Informatica","doi":"10.1007/s00236-021-00412-y","year":"2022","title":"Index appearance record with preorders","external_id":{"isi":["000735765500001"]},"isi":1,"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"],"citation":{"apa":"Kretinsky, J., Meggendorfer, T., Waldmann, C., &#38; Weininger, M. (2022). Index appearance record with preorders. <i>Acta Informatica</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s00236-021-00412-y\">https://doi.org/10.1007/s00236-021-00412-y</a>","ieee":"J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance record with preorders,” <i>Acta Informatica</i>, vol. 59. Springer Nature, pp. 585–618, 2022.","chicago":"Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger. “Index Appearance Record with Preorders.” <i>Acta Informatica</i>. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/s00236-021-00412-y\">https://doi.org/10.1007/s00236-021-00412-y</a>.","ama":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record with preorders. <i>Acta Informatica</i>. 2022;59:585-618. doi:<a href=\"https://doi.org/10.1007/s00236-021-00412-y\">10.1007/s00236-021-00412-y</a>","mla":"Kretinsky, Jan, et al. “Index Appearance Record with Preorders.” <i>Acta Informatica</i>, vol. 59, Springer Nature, 2022, pp. 585–618, doi:<a href=\"https://doi.org/10.1007/s00236-021-00412-y\">10.1007/s00236-021-00412-y</a>.","short":"J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, Acta Informatica 59 (2022) 585–618.","ista":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2022. Index appearance record with preorders. Acta Informatica. 59, 585–618."},"publication_status":"published","author":[{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","first_name":"Jan"},{"id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","first_name":"Tobias","last_name":"Meggendorfer","full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165"},{"last_name":"Waldmann","full_name":"Waldmann, Clara","first_name":"Clara"},{"first_name":"Maximilian","last_name":"Weininger","full_name":"Weininger, Maximilian"}],"keyword":["computer networks and communications","information systems","software"],"abstract":[{"text":"Transforming ω-automata into parity automata is traditionally done using appearance records. We present an efficient variant of this idea, tailored to Rabin automata, and several optimizations applicable to all appearance records. We compare the methods experimentally and show that our method produces significantly smaller automata than previous approaches.","lang":"eng"}],"article_processing_charge":"Yes (via OA deal)","volume":59,"oa":1,"date_updated":"2023-08-02T13:49:28Z","project":[{"_id":"B67AFEDC-15C9-11EA-A837-991A96BB2854","name":"IST Austria Open Access Fund"}],"oa_version":"Published Version","quality_controlled":"1","acknowledgement":"This work is partially funded by the German Research Foundation (DFG) projects Verified Model Checkers (No. 317422601) and Statistical Unbounded Verification (No. 383882557), and the Alexander von Humboldt Foundation with funds from the German Federal Ministry of Education and Research. It is an extended version of [21], including all proofs together with further explanations and examples. Moreover, we provide a new, more efficient construction based on (total) preorders, unifying previous optimizations. Experiments are performed with a new, performant implementation, comparing our approach to the current state of the art.","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","publication_identifier":{"issn":["0001-5903"],"eissn":["1432-0525"]},"_id":"10602"},{"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)"},"isi":1,"article_number":"040501","related_material":{"link":[{"url":"https://github.com/capoe/benchml","relation":"software"}]},"ddc":["000"],"doi":"10.1088/2632-2153/ac4d11","year":"2022","external_id":{"isi":["000886534000001"]},"title":"BenchML: An extensible pipelining framework for benchmarking representations of materials and molecules at scale","oa":1,"volume":3,"date_updated":"2023-08-04T08:49:53Z","article_processing_charge":"No","_id":"12128","publication_identifier":{"issn":["2632-2153"]},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","acknowledgement":"C P acknowledges funding from Astex through the Sustaining Innovation Program under the Milner Consortium. B C acknowledges resources provided by the Cambridge Tier-2 system operated by the University of Cambridge Research Computing Service funded by EPSRC Tier-2 capital Grant EP/P020259/1. F A F acknowledges funding from the Swiss National Science Foundation (Grant No. P2BSP2_191736). ","quality_controlled":"1","oa_version":"Published Version","publication_status":"published","citation":{"chicago":"Poelking, Carl, Felix A Faber, and Bingqing Cheng. “BenchML: An Extensible Pipelining Framework for Benchmarking Representations of Materials and Molecules at Scale.” <i>Machine Learning: Science and Technology</i>. IOP Publishing, 2022. <a href=\"https://doi.org/10.1088/2632-2153/ac4d11\">https://doi.org/10.1088/2632-2153/ac4d11</a>.","ieee":"C. Poelking, F. A. Faber, and B. Cheng, “BenchML: An extensible pipelining framework for benchmarking representations of materials and molecules at scale,” <i>Machine Learning: Science and Technology</i>, vol. 3, no. 4. IOP Publishing, 2022.","apa":"Poelking, C., Faber, F. A., &#38; Cheng, B. (2022). BenchML: An extensible pipelining framework for benchmarking representations of materials and molecules at scale. <i>Machine Learning: Science and Technology</i>. IOP Publishing. <a href=\"https://doi.org/10.1088/2632-2153/ac4d11\">https://doi.org/10.1088/2632-2153/ac4d11</a>","short":"C. Poelking, F.A. Faber, B. Cheng, Machine Learning: Science and Technology 3 (2022).","ista":"Poelking C, Faber FA, Cheng B. 2022. BenchML: An extensible pipelining framework for benchmarking representations of materials and molecules at scale. Machine Learning: Science and Technology. 3(4), 040501.","mla":"Poelking, Carl, et al. “BenchML: An Extensible Pipelining Framework for Benchmarking Representations of Materials and Molecules at Scale.” <i>Machine Learning: Science and Technology</i>, vol. 3, no. 4, 040501, IOP Publishing, 2022, doi:<a href=\"https://doi.org/10.1088/2632-2153/ac4d11\">10.1088/2632-2153/ac4d11</a>.","ama":"Poelking C, Faber FA, Cheng B. BenchML: An extensible pipelining framework for benchmarking representations of materials and molecules at scale. <i>Machine Learning: Science and Technology</i>. 2022;3(4). doi:<a href=\"https://doi.org/10.1088/2632-2153/ac4d11\">10.1088/2632-2153/ac4d11</a>"},"abstract":[{"text":"We introduce a machine-learning (ML) framework for high-throughput benchmarking of diverse representations of chemical systems against datasets of materials and molecules. The guiding principle underlying the benchmarking approach is to evaluate raw descriptor performance by limiting model complexity to simple regression schemes while enforcing best ML practices, allowing for unbiased hyperparameter optimization, and assessing learning progress through learning curves along series of synchronized train-test splits. The resulting models are intended as baselines that can inform future method development, in addition to indicating how easily a given dataset can be learnt. Through a comparative analysis of the training outcome across a diverse set of physicochemical, topological and geometric representations, we glean insight into the relative merits of these representations as well as their interrelatedness.","lang":"eng"}],"author":[{"last_name":"Poelking","full_name":"Poelking, Carl","first_name":"Carl"},{"full_name":"Faber, Felix A","last_name":"Faber","first_name":"Felix A"},{"id":"cbe3cda4-d82c-11eb-8dc7-8ff94289fcc9","first_name":"Bingqing","full_name":"Cheng, Bingqing","last_name":"Cheng","orcid":"0000-0002-3584-9632"}],"keyword":["Artificial Intelligence","Human-Computer Interaction","Software"],"has_accepted_license":"1","department":[{"_id":"BiCh"}],"date_created":"2023-01-12T12:02:21Z","file":[{"date_created":"2023-01-23T10:42:04Z","checksum":"8930d4ad6ed9b47358c6f1a68666adb6","file_name":"2022_MachLearning_Poelking.pdf","file_size":13814559,"date_updated":"2023-01-23T10:42:04Z","access_level":"open_access","success":1,"file_id":"12343","creator":"dernst","content_type":"application/pdf","relation":"main_file"}],"month":"11","date_published":"2022-11-17T00:00:00Z","article_type":"original","publisher":"IOP Publishing","scopus_import":"1","language":[{"iso":"eng"}],"issue":"4","publication":"Machine Learning: Science and Technology","file_date_updated":"2023-01-23T10:42:04Z","day":"17","type":"journal_article","intvolume":"         3","status":"public"},{"publisher":"Springer Nature","scopus_import":"1","language":[{"iso":"eng"}],"month":"11","date_published":"2022-11-15T00:00:00Z","article_type":"original","file":[{"relation":"main_file","content_type":"application/pdf","file_id":"12355","creator":"dernst","success":1,"access_level":"open_access","date_updated":"2023-01-24T09:49:44Z","file_size":3259553,"file_name":"2022_NatureMachineIntelligence_Hasani.pdf","checksum":"b4789122ce04bfb4ac042390f59aaa8b","date_created":"2023-01-24T09:49:44Z"}],"date_created":"2023-01-12T12:07:21Z","has_accepted_license":"1","department":[{"_id":"ToHe"}],"intvolume":"         4","status":"public","day":"15","type":"journal_article","issue":"11","publication":"Nature Machine Intelligence","page":"992-1003","file_date_updated":"2023-01-24T09:49:44Z","title":"Closed-form continuous-time neural networks","external_id":{"isi":["000884215600003"],"arxiv":["2106.13898"]},"year":"2022","doi":"10.1038/s42256-022-00556-7","related_material":{"link":[{"relation":"erratum","url":"https://doi.org/10.1038/s42256-022-00597-y"}]},"ddc":["000"],"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)"},"isi":1,"abstract":[{"lang":"eng","text":"Continuous-time neural networks are a class of machine learning systems that can tackle representation learning on spatiotemporal decision-making tasks. These models are typically represented by continuous differential equations. However, their expressive power when they are deployed on computers is bottlenecked by numerical differential equation solvers. This limitation has notably slowed down the scaling and understanding of numerous natural physical phenomena such as the dynamics of nervous systems. Ideally, we would circumvent this bottleneck by solving the given dynamical system in closed form. This is known to be intractable in general. Here, we show that it is possible to closely approximate the interaction between neurons and synapses—the building blocks of natural and artificial neural networks—constructed by liquid time-constant networks efficiently in closed form. To this end, we compute a tightly bounded approximation of the solution of an integral appearing in liquid time-constant dynamics that has had no known closed-form solution so far. This closed-form solution impacts the design of continuous-time and continuous-depth neural models. For instance, since time appears explicitly in closed form, the formulation relaxes the need for complex numerical solvers. Consequently, we obtain models that are between one and five orders of magnitude faster in training and inference compared with differential equation-based counterparts. More importantly, in contrast to ordinary differential equation-based continuous networks, closed-form networks can scale remarkably well compared with other deep learning instances. Lastly, as these models are derived from liquid networks, they show good performance in time-series modelling compared with advanced recurrent neural network models."}],"keyword":["Artificial Intelligence","Computer Networks and Communications","Computer Vision and Pattern Recognition","Human-Computer Interaction","Software"],"author":[{"first_name":"Ramin","last_name":"Hasani","full_name":"Hasani, Ramin"},{"first_name":"Mathias","full_name":"Lechner, Mathias","last_name":"Lechner","id":"3DC22916-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Amini","full_name":"Amini, Alexander","first_name":"Alexander"},{"first_name":"Lucas","last_name":"Liebenwein","full_name":"Liebenwein, Lucas"},{"first_name":"Aaron","last_name":"Ray","full_name":"Ray, Aaron"},{"first_name":"Max","last_name":"Tschaikowski","full_name":"Tschaikowski, Max"},{"first_name":"Gerald","last_name":"Teschl","full_name":"Teschl, Gerald"},{"first_name":"Daniela","full_name":"Rus, Daniela","last_name":"Rus"}],"publication_status":"published","citation":{"chicago":"Hasani, Ramin, Mathias Lechner, Alexander Amini, Lucas Liebenwein, Aaron Ray, Max Tschaikowski, Gerald Teschl, and Daniela Rus. “Closed-Form Continuous-Time Neural Networks.” <i>Nature Machine Intelligence</i>. Springer Nature, 2022. <a href=\"https://doi.org/10.1038/s42256-022-00556-7\">https://doi.org/10.1038/s42256-022-00556-7</a>.","apa":"Hasani, R., Lechner, M., Amini, A., Liebenwein, L., Ray, A., Tschaikowski, M., … Rus, D. (2022). Closed-form continuous-time neural networks. <i>Nature Machine Intelligence</i>. Springer Nature. <a href=\"https://doi.org/10.1038/s42256-022-00556-7\">https://doi.org/10.1038/s42256-022-00556-7</a>","ieee":"R. Hasani <i>et al.</i>, “Closed-form continuous-time neural networks,” <i>Nature Machine Intelligence</i>, vol. 4, no. 11. Springer Nature, pp. 992–1003, 2022.","ista":"Hasani R, Lechner M, Amini A, Liebenwein L, Ray A, Tschaikowski M, Teschl G, Rus D. 2022. Closed-form continuous-time neural networks. Nature Machine Intelligence. 4(11), 992–1003.","short":"R. Hasani, M. Lechner, A. Amini, L. Liebenwein, A. Ray, M. Tschaikowski, G. Teschl, D. Rus, Nature Machine Intelligence 4 (2022) 992–1003.","ama":"Hasani R, Lechner M, Amini A, et al. Closed-form continuous-time neural networks. <i>Nature Machine Intelligence</i>. 2022;4(11):992-1003. doi:<a href=\"https://doi.org/10.1038/s42256-022-00556-7\">10.1038/s42256-022-00556-7</a>","mla":"Hasani, Ramin, et al. “Closed-Form Continuous-Time Neural Networks.” <i>Nature Machine Intelligence</i>, vol. 4, no. 11, Springer Nature, 2022, pp. 992–1003, doi:<a href=\"https://doi.org/10.1038/s42256-022-00556-7\">10.1038/s42256-022-00556-7</a>."},"_id":"12147","publication_identifier":{"issn":["2522-5839"]},"acknowledgement":"This research was supported in part by the AI2050 program at Schmidt Futures (grant G-22-63172), the Boeing Company, and the United States Air Force Research Laboratory and the United States Air Force Artificial Intelligence Accelerator and was accomplished under cooperative agreement number FA8750-19-2-1000. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of the United States Air Force or the U.S. Government. The U.S. Government is authorized to reproduce and distribute reprints for Government purposes, notwithstanding any copyright notation herein. This work was further supported by The Boeing Company and Office of Naval Research grant N00014-18-1-2830. M.T. is supported by the Poul Due Jensen Foundation, grant 883901. M.L. was supported in part by the Austrian Science Fund under grant Z211-N23 (Wittgenstein Award). A.A. was supported by the National Science Foundation Graduate Research Fellowship Program. We thank T.-H. Wang, P. Kao, M. Chahine, W. Xiao, X. Li, L. Yin and Y. Ben for useful suggestions and for testing of CfC models to confirm the results across other domains.","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","project":[{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}],"quality_controlled":"1","oa_version":"Published Version","arxiv":1,"oa":1,"volume":4,"date_updated":"2023-08-04T09:00:10Z","article_processing_charge":"No"},{"month":"06","date_published":"2021-06-01T00:00:00Z","article_type":"original","scopus_import":"1","publisher":"Springer Nature","language":[{"iso":"eng"}],"has_accepted_license":"1","department":[{"_id":"VlKo"}],"date_created":"2021-03-10T12:18:47Z","file":[{"date_updated":"2021-08-11T12:44:16Z","access_level":"open_access","file_name":"2021_NetworksSpatialEconomics_Shehu.pdf","file_size":834964,"date_created":"2021-08-11T12:44:16Z","checksum":"22b4253a2e5da843622a2df713784b4c","content_type":"application/pdf","relation":"main_file","creator":"kschuh","file_id":"9884","success":1}],"day":"01","type":"journal_article","intvolume":"        21","status":"public","publication":"Networks and Spatial Economics","issue":"2","page":"291-323","file_date_updated":"2021-08-11T12:44:16Z","doi":"10.1007/s11067-021-09517-w","year":"2021","ec_funded":1,"external_id":{"isi":["000625002100001"]},"title":"New inertial projection methods for solving multivalued variational inequality problems beyond monotonicity","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)"},"isi":1,"ddc":["510"],"citation":{"apa":"Izuchukwu, C., &#38; Shehu, Y. (2021). New inertial projection methods for solving multivalued variational inequality problems beyond monotonicity. <i>Networks and Spatial Economics</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s11067-021-09517-w\">https://doi.org/10.1007/s11067-021-09517-w</a>","ieee":"C. Izuchukwu and Y. Shehu, “New inertial projection methods for solving multivalued variational inequality problems beyond monotonicity,” <i>Networks and Spatial Economics</i>, vol. 21, no. 2. Springer Nature, pp. 291–323, 2021.","chicago":"Izuchukwu, Chinedu, and Yekini Shehu. “New Inertial Projection Methods for Solving Multivalued Variational Inequality Problems beyond Monotonicity.” <i>Networks and Spatial Economics</i>. Springer Nature, 2021. <a href=\"https://doi.org/10.1007/s11067-021-09517-w\">https://doi.org/10.1007/s11067-021-09517-w</a>.","ama":"Izuchukwu C, Shehu Y. New inertial projection methods for solving multivalued variational inequality problems beyond monotonicity. <i>Networks and Spatial Economics</i>. 2021;21(2):291-323. doi:<a href=\"https://doi.org/10.1007/s11067-021-09517-w\">10.1007/s11067-021-09517-w</a>","mla":"Izuchukwu, Chinedu, and Yekini Shehu. “New Inertial Projection Methods for Solving Multivalued Variational Inequality Problems beyond Monotonicity.” <i>Networks and Spatial Economics</i>, vol. 21, no. 2, Springer Nature, 2021, pp. 291–323, doi:<a href=\"https://doi.org/10.1007/s11067-021-09517-w\">10.1007/s11067-021-09517-w</a>.","short":"C. Izuchukwu, Y. Shehu, Networks and Spatial Economics 21 (2021) 291–323.","ista":"Izuchukwu C, Shehu Y. 2021. New inertial projection methods for solving multivalued variational inequality problems beyond monotonicity. Networks and Spatial Economics. 21(2), 291–323."},"publication_status":"published","abstract":[{"text":"In this paper, we present two new inertial projection-type methods for solving multivalued variational inequality problems in finite-dimensional spaces. We establish the convergence of the sequence generated by these methods when the multivalued mapping associated with the problem is only required to be locally bounded without any monotonicity assumption. Furthermore, the inertial techniques that we employ in this paper are quite different from the ones used in most papers. Moreover, based on the weaker assumptions on the inertial factor in our methods, we derive several special cases of our methods. Finally, we present some experimental results to illustrate the profits that we gain by introducing the inertial extrapolation steps.","lang":"eng"}],"keyword":["Computer Networks and Communications","Software","Artificial Intelligence"],"author":[{"last_name":"Izuchukwu","full_name":"Izuchukwu, Chinedu","first_name":"Chinedu"},{"full_name":"Shehu, Yekini","last_name":"Shehu","orcid":"0000-0001-9224-7139","first_name":"Yekini","id":"3FC7CB58-F248-11E8-B48F-1D18A9856A87"}],"article_processing_charge":"Yes (via OA deal)","volume":21,"date_updated":"2023-09-05T15:32:32Z","oa":1,"publication_identifier":{"issn":["1566-113X"],"eissn":["1572-9427"]},"_id":"9234","oa_version":"Published Version","project":[{"grant_number":"616160","_id":"25FBA906-B435-11E9-9278-68D0E5697425","name":"Discrete Optimization in Computer Vision: Theory and Practice","call_identifier":"FP7"},{"name":"IST Austria Open Access Fund","_id":"B67AFEDC-15C9-11EA-A837-991A96BB2854"}],"quality_controlled":"1","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","acknowledgement":"The authors sincerely thank the Editor-in-Chief and anonymous referees for their careful reading, constructive comments and fruitful suggestions that help improve the manuscript. The research of the first author is supported by the National Research Foundation (NRF) South Africa (S& F-DSI/NRF Free Standing Postdoctoral Fellowship; Grant Number: 120784). The first author also acknowledges the financial support from DSI/NRF, South Africa Center of Excellence in Mathematical and Statistical Sciences (CoE-MaSS) Postdoctoral Fellowship. The second author has received funding from the European Research Council (ERC) under the European Union’s Seventh Framework Program (FP7 - 2007-2013) (Grant agreement No. 616160). Open Access funding provided by Institute of Science and Technology (IST Austria)."},{"doi":"10.1007/978-3-030-88494-9_12","place":"Cham","year":"2021","title":"Differential monitoring","external_id":{"isi":["000719383800012"]},"alternative_title":["LNCS"],"isi":1,"related_material":{"record":[{"id":"9946","relation":"extended_version","status":"public"}]},"ddc":["005"],"citation":{"mla":"Mühlböck, Fabian, and Thomas A. Henzinger. “Differential Monitoring.” <i>International Conference on Runtime Verification</i>, vol. 12974, Springer Nature, 2021, pp. 231–43, doi:<a href=\"https://doi.org/10.1007/978-3-030-88494-9_12\">10.1007/978-3-030-88494-9_12</a>.","ama":"Mühlböck F, Henzinger TA. Differential monitoring. In: <i>International Conference on Runtime Verification</i>. Vol 12974. Cham: Springer Nature; 2021:231-243. doi:<a href=\"https://doi.org/10.1007/978-3-030-88494-9_12\">10.1007/978-3-030-88494-9_12</a>","ista":"Mühlböck F, Henzinger TA. 2021. Differential monitoring. International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 12974, 231–243.","short":"F. Mühlböck, T.A. Henzinger, in:, International Conference on Runtime Verification, Springer Nature, Cham, 2021, pp. 231–243.","apa":"Mühlböck, F., &#38; Henzinger, T. A. (2021). Differential monitoring. In <i>International Conference on Runtime Verification</i> (Vol. 12974, pp. 231–243). Cham: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-88494-9_12\">https://doi.org/10.1007/978-3-030-88494-9_12</a>","ieee":"F. Mühlböck and T. A. Henzinger, “Differential monitoring,” in <i>International Conference on Runtime Verification</i>, Virtual, 2021, vol. 12974, pp. 231–243.","chicago":"Mühlböck, Fabian, and Thomas A Henzinger. “Differential Monitoring.” In <i>International Conference on Runtime Verification</i>, 12974:231–43. Cham: Springer Nature, 2021. <a href=\"https://doi.org/10.1007/978-3-030-88494-9_12\">https://doi.org/10.1007/978-3-030-88494-9_12</a>."},"publication_status":"published","abstract":[{"text":"We argue that the time is ripe to investigate differential monitoring, in which the specification of a program's behavior is implicitly given by a second program implementing the same informal specification. Similar ideas have been proposed before, and are currently implemented in restricted form for testing and specialized run-time analyses, aspects of which we combine. We discuss the challenges of implementing differential monitoring as a general-purpose, black-box run-time monitoring framework, and present promising results of a preliminary implementation, showing low monitoring overheads for diverse programs.","lang":"eng"}],"author":[{"id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","orcid":"0000-0003-1548-0177","full_name":"Mühlböck, Fabian","last_name":"Mühlböck","first_name":"Fabian"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","first_name":"Thomas A"}],"keyword":["run-time verification","software engineering","implicit specification"],"article_processing_charge":"No","oa":1,"date_updated":"2023-08-14T07:20:30Z","volume":12974,"publication_identifier":{"eissn":["1611-3349"],"eisbn":["978-3-030-88494-9"],"isbn":["978-3-030-88493-2"],"issn":["0302-9743"]},"_id":"10108","quality_controlled":"1","oa_version":"Preprint","project":[{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","call_identifier":"FWF"}],"acknowledgement":"The authors would like to thank Borzoo Bonakdarpour, Derek Dreyer, Adrian Francalanza, Owolabi Legunsen, Mae Milano, Manuel Rigger, Cesar Sanchez, and the members of the IST Verification Seminar for their helpful comments and insights on various stages of this work, as well as the reviewers of RV’21 for their helpful suggestions on the actual paper.","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","month":"10","date_published":"2021-10-06T00:00:00Z","scopus_import":"1","publisher":"Springer Nature","language":[{"iso":"eng"}],"has_accepted_license":"1","department":[{"_id":"ToHe"}],"conference":{"start_date":"2021-10-11","location":"Virtual","end_date":"2021-10-14","name":"RV: Runtime Verification"},"file":[{"access_level":"open_access","date_updated":"2021-10-07T23:32:18Z","file_size":350632,"file_name":"differentialmonitoring-cameraready-openaccess.pdf","checksum":"554c7fdb259eda703a8b6328a6dad55a","date_created":"2021-10-07T23:32:18Z","relation":"main_file","content_type":"application/pdf","file_id":"10109","creator":"fmuehlbo","success":1}],"date_created":"2021-10-07T23:30:10Z","day":"06","type":"conference","intvolume":"     12974","status":"public","publication":"International Conference on Runtime Verification","page":"231-243","file_date_updated":"2021-10-07T23:32:18Z"},{"doi":"10.1145/3485541","year":"2021","ec_funded":1,"title":"The reads-from equivalence for the TSO and PSO memory models","external_id":{"arxiv":["2011.11763"]},"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)"},"article_number":"164","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"10199"}]},"ddc":["000"],"citation":{"ama":"Bui TL, Chatterjee K, Gautam T, Pavlogiannis A, Toman V. The reads-from equivalence for the TSO and PSO memory models. <i>Proceedings of the ACM on Programming Languages</i>. 2021;5(OOPSLA). doi:<a href=\"https://doi.org/10.1145/3485541\">10.1145/3485541</a>","mla":"Bui, Truc Lam, et al. “The Reads-from Equivalence for the TSO and PSO Memory Models.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 5, no. OOPSLA, 164, Association for Computing Machinery, 2021, doi:<a href=\"https://doi.org/10.1145/3485541\">10.1145/3485541</a>.","ista":"Bui TL, Chatterjee K, Gautam T, Pavlogiannis A, Toman V. 2021. The reads-from equivalence for the TSO and PSO memory models. Proceedings of the ACM on Programming Languages. 5(OOPSLA), 164.","short":"T.L. Bui, K. Chatterjee, T. Gautam, A. Pavlogiannis, V. Toman, Proceedings of the ACM on Programming Languages 5 (2021).","apa":"Bui, T. L., Chatterjee, K., Gautam, T., Pavlogiannis, A., &#38; Toman, V. (2021). The reads-from equivalence for the TSO and PSO memory models. <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3485541\">https://doi.org/10.1145/3485541</a>","ieee":"T. L. Bui, K. Chatterjee, T. Gautam, A. Pavlogiannis, and V. Toman, “The reads-from equivalence for the TSO and PSO memory models,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 5, no. OOPSLA. Association for Computing Machinery, 2021.","chicago":"Bui, Truc Lam, Krishnendu Chatterjee, Tushar Gautam, Andreas Pavlogiannis, and Viktor Toman. “The Reads-from Equivalence for the TSO and PSO Memory Models.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2021. <a href=\"https://doi.org/10.1145/3485541\">https://doi.org/10.1145/3485541</a>."},"publication_status":"published","abstract":[{"text":"In this work we solve the algorithmic problem of consistency verification for the TSO and PSO memory models given a reads-from map, denoted VTSO-rf and VPSO-rf, respectively. For an execution of n events over k threads and d variables, we establish novel bounds that scale as nk+1 for TSO and as nk+1· min(nk2, 2k· d) for PSO. Moreover, based on our solution to these problems, we develop an SMC algorithm under TSO and PSO that uses the RF equivalence. The algorithm is exploration-optimal, in the sense that it is guaranteed to explore each class of the RF partitioning exactly once, and spends polynomial time per class when k is bounded. Finally, we implement all our algorithms in the SMC tool Nidhugg, and perform a large number of experiments over benchmarks from existing literature. Our experimental results show that our algorithms for VTSO-rf and VPSO-rf provide significant scalability improvements over standard alternatives. Moreover, when used for SMC, the RF partitioning is often much coarser than the standard Shasha-Snir partitioning for TSO/PSO, which yields a significant speedup in the model checking task.\r\n\r\n","lang":"eng"}],"author":[{"first_name":"Truc Lam","last_name":"Bui","full_name":"Bui, Truc Lam"},{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Tushar","full_name":"Gautam, Tushar","last_name":"Gautam"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722"},{"id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","first_name":"Viktor","full_name":"Toman, Viktor","last_name":"Toman","orcid":"0000-0001-9036-063X"}],"keyword":["safety","risk","reliability and quality","software"],"arxiv":1,"article_processing_charge":"No","oa":1,"date_updated":"2025-07-14T09:10:16Z","volume":5,"publication_identifier":{"eissn":["2475-1421"]},"_id":"10191","quality_controlled":"1","oa_version":"Published Version","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"}],"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","acknowledgement":"The research was partially funded by the ERC CoG 863818 (ForM-SMArt) and the Vienna Science\r\nand Technology Fund (WWTF) through project ICT15-003.","month":"10","date_published":"2021-10-15T00:00:00Z","article_type":"original","scopus_import":"1","publisher":"Association for Computing Machinery","language":[{"iso":"eng"}],"has_accepted_license":"1","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"date_created":"2021-10-27T15:05:34Z","file":[{"date_updated":"2021-11-04T07:24:48Z","access_level":"open_access","file_name":"2021_ProcACMPL_Bui.pdf","file_size":2903485,"date_created":"2021-11-04T07:24:48Z","checksum":"9d6dce7b611853c529bb7b1915ac579e","content_type":"application/pdf","relation":"main_file","file_id":"10215","creator":"cchlebak","success":1}],"day":"15","type":"journal_article","intvolume":"         5","status":"public","publication":"Proceedings of the ACM on Programming Languages","issue":"OOPSLA","file_date_updated":"2021-11-04T07:24:48Z"},{"date_published":"2021-09-01T00:00:00Z","month":"09","language":[{"iso":"eng"}],"publisher":"IST Austria","department":[{"_id":"ToHe"}],"has_accepted_license":"1","date_created":"2021-08-20T20:00:37Z","file":[{"access_level":"open_access","date_updated":"2021-09-03T12:34:28Z","checksum":"0f9aafd59444cb6bdca6925d163ab946","date_created":"2021-08-20T19:59:44Z","file_size":"320453","file_name":"differentialmonitoring-techreport.pdf","creator":"fmuehlbo","file_id":"9948","relation":"main_file","content_type":"application/pdf"}],"type":"technical_report","day":"01","status":"public","file_date_updated":"2021-09-03T12:34:28Z","page":"17","doi":"10.15479/AT:ISTA:9946","year":"2021","title":"Differential monitoring","alternative_title":["IST Austria Technical Report"],"ddc":["005"],"related_material":{"record":[{"relation":"other","id":"9281","status":"public"},{"status":"public","id":"10108","relation":"shorter_version"}]},"citation":{"chicago":"Mühlböck, Fabian, and Thomas A Henzinger. <i>Differential Monitoring</i>. IST Austria, 2021. <a href=\"https://doi.org/10.15479/AT:ISTA:9946\">https://doi.org/10.15479/AT:ISTA:9946</a>.","ieee":"F. Mühlböck and T. A. Henzinger, <i>Differential monitoring</i>. IST Austria, 2021.","apa":"Mühlböck, F., &#38; Henzinger, T. A. (2021). <i>Differential monitoring</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:9946\">https://doi.org/10.15479/AT:ISTA:9946</a>","short":"F. Mühlböck, T.A. Henzinger, Differential Monitoring, IST Austria, 2021.","ista":"Mühlböck F, Henzinger TA. 2021. Differential monitoring, IST Austria, 17p.","ama":"Mühlböck F, Henzinger TA. <i>Differential Monitoring</i>. IST Austria; 2021. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:9946\">10.15479/AT:ISTA:9946</a>","mla":"Mühlböck, Fabian, and Thomas A. Henzinger. <i>Differential Monitoring</i>. IST Austria, 2021, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:9946\">10.15479/AT:ISTA:9946</a>."},"publication_status":"published","author":[{"id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","last_name":"Mühlböck","full_name":"Mühlböck, Fabian","orcid":"0000-0003-1548-0177","first_name":"Fabian"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","first_name":"Thomas A"}],"keyword":["run-time verification","software engineering","implicit specification"],"abstract":[{"lang":"eng","text":"We argue that the time is ripe to investigate differential monitoring, in which the specification of a program's behavior is implicitly given by a second program implementing the same informal specification. Similar ideas have been proposed before, and are currently implemented in restricted form for testing and specialized run-time analyses, aspects of which we combine. We discuss the challenges of implementing differential monitoring as a general-purpose, black-box run-time monitoring framework, and present promising results of a preliminary implementation, showing low monitoring overheads for diverse programs."}],"article_processing_charge":"No","oa":1,"date_updated":"2023-08-14T07:20:29Z","oa_version":"Published Version","project":[{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","call_identifier":"FWF"}],"acknowledgement":"The authors would like to thank Borzoo Bonakdarpour, Derek Dreyer, Adrian Francalanza, Owolabi Legunsen, Matthew Milano, Manuel Rigger, Cesar Sanchez, and the members of the IST Verification Seminar for their helpful comments and insights on various stages of this work, as well as the reviewers of RV’21 for their helpful suggestions on the actual paper.","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","publication_identifier":{"issn":["2664-1690"]},"_id":"9946"},{"department":[{"_id":"ToHe"}],"date_created":"2022-03-18T10:10:53Z","article_type":"original","date_published":"2020-08-03T00:00:00Z","month":"08","language":[{"iso":"eng"}],"publisher":"Springer Nature","scopus_import":"1","page":"741-758","issue":"6","publication":"International Journal on Software Tools for Technology Transfer","type":"journal_article","day":"03","status":"public","intvolume":"        22","isi":1,"related_material":{"record":[{"relation":"earlier_version","id":"299","status":"public"}]},"year":"2020","doi":"10.1007/s10009-020-00582-z","title":"AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic","external_id":{"isi":["000555398600001"]},"volume":22,"date_updated":"2023-09-08T11:52:02Z","article_processing_charge":"No","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","quality_controlled":"1","oa_version":"None","_id":"10861","publication_identifier":{"issn":["1433-2779"],"eissn":["1433-2787"]},"publication_status":"published","citation":{"ista":"Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. 2020. AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. International Journal on Software Tools for Technology Transfer. 22(6), 741–758.","short":"D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, D. Ulus, International Journal on Software Tools for Technology Transfer 22 (2020) 741–758.","mla":"Nickovic, Dejan, et al. “AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic.” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 22, no. 6, Springer Nature, 2020, pp. 741–58, doi:<a href=\"https://doi.org/10.1007/s10009-020-00582-z\">10.1007/s10009-020-00582-z</a>.","ama":"Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. <i>International Journal on Software Tools for Technology Transfer</i>. 2020;22(6):741-758. doi:<a href=\"https://doi.org/10.1007/s10009-020-00582-z\">10.1007/s10009-020-00582-z</a>","chicago":"Nickovic, Dejan, Olivier Lebeltel, Oded Maler, Thomas Ferrere, and Dogan Ulus. “AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic.” <i>International Journal on Software Tools for Technology Transfer</i>. Springer Nature, 2020. <a href=\"https://doi.org/10.1007/s10009-020-00582-z\">https://doi.org/10.1007/s10009-020-00582-z</a>.","ieee":"D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, and D. Ulus, “AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic,” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 22, no. 6. Springer Nature, pp. 741–758, 2020.","apa":"Nickovic, D., Lebeltel, O., Maler, O., Ferrere, T., &#38; Ulus, D. (2020). AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. <i>International Journal on Software Tools for Technology Transfer</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s10009-020-00582-z\">https://doi.org/10.1007/s10009-020-00582-z</a>"},"keyword":["Information Systems","Software"],"author":[{"first_name":"Dejan","full_name":"Nickovic, Dejan","last_name":"Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Olivier","last_name":"Lebeltel","full_name":"Lebeltel, Olivier"},{"last_name":"Maler","full_name":"Maler, Oded","first_name":"Oded"},{"first_name":"Thomas","orcid":"0000-0001-5199-3143","last_name":"Ferrere","full_name":"Ferrere, Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Dogan","full_name":"Ulus, Dogan","last_name":"Ulus"}],"abstract":[{"lang":"eng","text":"We introduce in this paper AMT2.0, a tool for qualitative and quantitative analysis of hybrid continuous and Boolean signals that combine numerical values and discrete events. The evaluation of the signals is based on rich temporal specifications expressed in extended signal temporal logic, which integrates timed regular expressions within signal temporal logic. The tool features qualitative monitoring (property satisfaction checking), trace diagnostics for explaining and justifying property violations and specification-driven measurement of quantitative features of the signal. We demonstrate the tool functionality on several running examples and case studies, and evaluate its performance."}]},{"date_published":"2019-10-10T00:00:00Z","month":"10","language":[{"iso":"eng"}],"publisher":"ACM","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"has_accepted_license":"1","date_created":"2021-10-27T14:57:06Z","file":[{"access_level":"open_access","date_updated":"2021-11-12T11:41:56Z","checksum":"2149979c46964c4d117af06ccb6c0834","date_created":"2021-11-12T11:41:56Z","file_size":570829,"file_name":"2019_ACM_Chatterjee.pdf","file_id":"10278","creator":"cchlebak","relation":"main_file","content_type":"application/pdf","success":1}],"conference":{"name":"OOPSLA: Object-oriented Programming, Systems, Languages and Applications","location":"Athens, Greece","end_date":"2019-10-25","start_date":"2019-10-23"},"type":"conference","day":"10","status":"public","intvolume":"         3","file_date_updated":"2021-11-12T11:41:56Z","publication":"Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications","year":"2019","doi":"10.1145/3360550","external_id":{"arxiv":["1909.00989"]},"title":"Value-centric dynamic partial order reduction","main_file_link":[{"open_access":"1","url":"https://dl.acm.org/doi/10.1145/3360550"}],"article_number":"124","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"],"related_material":{"record":[{"id":"10199","relation":"dissertation_contains","status":"public"}]},"publication_status":"published","citation":{"ista":"Chatterjee K, Pavlogiannis A, Toman V. 2019. Value-centric dynamic partial order reduction. Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications. OOPSLA: Object-oriented Programming, Systems, Languages and Applications vol. 3, 124.","short":"K. Chatterjee, A. Pavlogiannis, V. Toman, in:, Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications, ACM, 2019.","ama":"Chatterjee K, Pavlogiannis A, Toman V. Value-centric dynamic partial order reduction. In: <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications</i>. Vol 3. ACM; 2019. doi:<a href=\"https://doi.org/10.1145/3360550\">10.1145/3360550</a>","mla":"Chatterjee, Krishnendu, et al. “Value-Centric Dynamic Partial Order Reduction.” <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications</i>, vol. 3, 124, ACM, 2019, doi:<a href=\"https://doi.org/10.1145/3360550\">10.1145/3360550</a>.","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, and Viktor Toman. “Value-Centric Dynamic Partial Order Reduction.” In <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications</i>, Vol. 3. ACM, 2019. <a href=\"https://doi.org/10.1145/3360550\">https://doi.org/10.1145/3360550</a>.","ieee":"K. Chatterjee, A. Pavlogiannis, and V. Toman, “Value-centric dynamic partial order reduction,” in <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications</i>, Athens, Greece, 2019, vol. 3.","apa":"Chatterjee, K., Pavlogiannis, A., &#38; Toman, V. (2019). Value-centric dynamic partial order reduction. In <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications</i> (Vol. 3). Athens, Greece: ACM. <a href=\"https://doi.org/10.1145/3360550\">https://doi.org/10.1145/3360550</a>"},"keyword":["safety","risk","reliability and quality","software"],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"first_name":"Andreas","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Viktor","orcid":"0000-0001-9036-063X","last_name":"Toman","full_name":"Toman, Viktor","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87"}],"abstract":[{"lang":"eng","text":"The verification of concurrent programs remains an open challenge, as thread interaction has to be accounted for, which leads to state-space explosion. Stateless model checking battles this problem by exploring traces rather than states of the program. As there are exponentially many traces, dynamic partial-order reduction (DPOR) techniques are used to partition the trace space into equivalence classes, and explore a few representatives from each class. The standard equivalence that underlies most DPOR techniques is the happens-before equivalence, however recent works have spawned a vivid interest towards coarser equivalences. The efficiency of such approaches is a product of two parameters: (i) the size of the partitioning induced by the equivalence, and (ii) the time spent by the exploration algorithm in each class of the partitioning. In this work, we present a new equivalence, called value-happens-before and show that it has two appealing features. First, value-happens-before is always at least as coarse as the happens-before equivalence, and can be even exponentially coarser. Second, the value-happens-before partitioning is efficiently explorable when the number of threads is bounded. We present an algorithm called value-centric DPOR (VCDPOR), which explores the underlying partitioning using polynomial time per class. Finally, we perform an experimental evaluation of VCDPOR on various benchmarks, and compare it against other state-of-the-art approaches. Our results show that value-happens-before typically induces a significant reduction in the size of the underlying partitioning, which leads to a considerable reduction in the running time for exploring the whole partitioning."}],"oa":1,"volume":3,"date_updated":"2025-07-14T09:10:15Z","article_processing_charge":"No","arxiv":1,"acknowledgement":"The authors would also like to thank anonymous referees for their valuable comments and helpful suggestions. This work is supported by the Austrian Science Fund (FWF) NFN grants S11407-N23 (RiSE/SHiNE) and S11402-N23 (RiSE/SHiNE), by the Vienna Science and Technology Fund (WWTF) Project ICT15-003, and by the Austrian Science Fund (FWF) Schrodinger grant J-4220.\r\n","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","oa_version":"Published Version","project":[{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","call_identifier":"FWF","grant_number":"S11407"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23"}],"quality_controlled":"1","_id":"10190","publication_identifier":{"eissn":["2475-1421"]}},{"department":[{"_id":"PeJo"}],"has_accepted_license":"1","file":[{"access_level":"open_access","date_updated":"2021-12-01T14:38:08Z","checksum":"cdfc5339b530a25d6079f7223f0b1f16","date_created":"2021-12-01T14:38:08Z","file_size":149825,"file_name":"Schloegl_Abstract-BMT2013.pdf","creator":"schloegl","file_id":"10397","relation":"main_file","content_type":"application/pdf","success":1}],"date_created":"2021-12-01T14:35:35Z","conference":{"location":"Graz, Austria","end_date":"2013-09-21","name":"BMT: Biomedizinische Technik ","start_date":"2013-09-19"},"article_type":"original","date_published":"2013-08-01T00:00:00Z","month":"08","language":[{"iso":"eng"}],"publisher":"De Gruyter","file_date_updated":"2021-12-01T14:38:08Z","issue":"SI-1-Track-G","publication":"Biomedical Engineering / Biomedizinische Technik","type":"journal_article","day":"01","status":"public","intvolume":"        58","article_number":"000010151520134181","ddc":["005","610"],"year":"2013","doi":"10.1515/bmt-2013-4181","title":"Stimfit: A fast visualization and analysis environment for cellular neurophysiology","external_id":{"pmid":["24042795"]},"date_updated":"2021-12-02T12:51:12Z","volume":58,"oa":1,"article_processing_charge":"No","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","oa_version":"Submitted Version","quality_controlled":"1","_id":"10396","pmid":1,"publication_identifier":{"issn":["0013-5585"],"eissn":["1862-278X"]},"publication_status":"published","citation":{"ista":"Schlögl A, Jonas PM, Schmidt-Hieber C, Guzman SJ. 2013. Stimfit: A fast visualization and analysis environment for cellular neurophysiology. Biomedical Engineering / Biomedizinische Technik. 58(SI-1-Track-G), 000010151520134181.","short":"A. Schlögl, P.M. Jonas, C. Schmidt-Hieber, S.J. Guzman, Biomedical Engineering / Biomedizinische Technik 58 (2013).","ama":"Schlögl A, Jonas PM, Schmidt-Hieber C, Guzman SJ. Stimfit: A fast visualization and analysis environment for cellular neurophysiology. <i>Biomedical Engineering / Biomedizinische Technik</i>. 2013;58(SI-1-Track-G). doi:<a href=\"https://doi.org/10.1515/bmt-2013-4181\">10.1515/bmt-2013-4181</a>","mla":"Schlögl, Alois, et al. “Stimfit: A Fast Visualization and Analysis Environment for Cellular Neurophysiology.” <i>Biomedical Engineering / Biomedizinische Technik</i>, vol. 58, no. SI-1-Track-G, 000010151520134181, De Gruyter, 2013, doi:<a href=\"https://doi.org/10.1515/bmt-2013-4181\">10.1515/bmt-2013-4181</a>.","chicago":"Schlögl, Alois, Peter M Jonas, C. Schmidt-Hieber, and S. J. Guzman. “Stimfit: A Fast Visualization and Analysis Environment for Cellular Neurophysiology.” <i>Biomedical Engineering / Biomedizinische Technik</i>. De Gruyter, 2013. <a href=\"https://doi.org/10.1515/bmt-2013-4181\">https://doi.org/10.1515/bmt-2013-4181</a>.","ieee":"A. Schlögl, P. M. Jonas, C. Schmidt-Hieber, and S. J. Guzman, “Stimfit: A fast visualization and analysis environment for cellular neurophysiology,” <i>Biomedical Engineering / Biomedizinische Technik</i>, vol. 58, no. SI-1-Track-G. De Gruyter, 2013.","apa":"Schlögl, A., Jonas, P. M., Schmidt-Hieber, C., &#38; Guzman, S. J. (2013). Stimfit: A fast visualization and analysis environment for cellular neurophysiology. <i>Biomedical Engineering / Biomedizinische Technik</i>. Graz, Austria: De Gruyter. <a href=\"https://doi.org/10.1515/bmt-2013-4181\">https://doi.org/10.1515/bmt-2013-4181</a>"},"author":[{"id":"45BF87EE-F248-11E8-B48F-1D18A9856A87","first_name":"Alois","full_name":"Schlögl, Alois","last_name":"Schlögl","orcid":"0000-0002-5621-8100"},{"id":"353C1B58-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5001-4804","last_name":"Jonas","full_name":"Jonas, Peter M","first_name":"Peter M"},{"last_name":"Schmidt-Hieber","full_name":"Schmidt-Hieber, C.","first_name":"C."},{"full_name":"Guzman, S. J.","last_name":"Guzman","first_name":"S. J."}],"keyword":["biomedical engineering","data analysis","free software"],"abstract":[{"lang":"eng","text":"Stimfit is a free cross-platform software package for viewing and analyzing electrophysiological data. It supports most standard file types for cellular neurophysiology and other biomedical formats. Its analysis algorithms have been used and validated in several experimental laboratories. Its embedded Python scripting interface makes Stimfit highly extensible and customizable."}]}]