[{"quality_controlled":"1","ddc":["570"],"_id":"10731","date_updated":"2025-07-14T09:10:12Z","type":"journal_article","article_processing_charge":"No","doi":"10.1038/s41598-022-05333-5","publisher":"Springer Nature","ec_funded":1,"date_published":"2022-01-27T00:00:00Z","acknowledgement":"K.C. acknowledges support from ERC Consolidator Grant No. (863818: ForM-SMart). A.P. acknowledges support from FWF Grant No. J-4220. M.A.N. acknowledges support from Office of Naval Research grant N00014-16-1-2914 and from the John Templeton Foundation.","status":"public","publication":"Scientific Reports","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"year":"2022","isi":1,"external_id":{"arxiv":["2012.15155"],"isi":["000749198000039"]},"file_date_updated":"2022-02-07T14:57:59Z","publication_status":"published","publication_identifier":{"eissn":["2045-2322"]},"has_accepted_license":"1","abstract":[{"lang":"eng","text":"Motivated by COVID-19, we develop and analyze a simple stochastic model for the spread of disease in human population. We track how the number of infected and critically ill people develops over time in order to estimate the demand that is imposed on the hospital system. To keep this demand under control, we consider a class of simple policies for slowing down and reopening society and we compare their efficiency in mitigating the spread of the virus from several different points of view. We find that in order to avoid overwhelming of the hospital system, a policy must impose a harsh lockdown or it must react swiftly (or both). While reacting swiftly is universally beneficial, being harsh pays off only when the country is patient about reopening and when the neighboring countries coordinate their mitigation efforts. Our work highlights the importance of acting decisively when closing down and the importance of patience and coordination between neighboring countries when reopening."}],"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","image":"/images/cc_by.png","short":"CC BY (4.0)"},"intvolume":"        12","volume":12,"date_created":"2022-02-06T23:01:30Z","article_type":"original","scopus_import":"1","day":"27","author":[{"full_name":"Svoboda, Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","last_name":"Svoboda","orcid":"0000-0002-1419-3267","first_name":"Jakub"},{"first_name":"Josef","full_name":"Tkadlec, Josef","last_name":"Tkadlec"},{"first_name":"Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"last_name":"Nowak","full_name":"Nowak, Martin A.","first_name":"Martin A."}],"title":"Infection dynamics of COVID-19 virus under lockdown and reopening","oa_version":"Published Version","citation":{"ama":"Svoboda J, Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. Infection dynamics of COVID-19 virus under lockdown and reopening. <i>Scientific Reports</i>. 2022;12(1). doi:<a href=\"https://doi.org/10.1038/s41598-022-05333-5\">10.1038/s41598-022-05333-5</a>","ieee":"J. Svoboda, J. Tkadlec, A. Pavlogiannis, K. Chatterjee, and M. A. Nowak, “Infection dynamics of COVID-19 virus under lockdown and reopening,” <i>Scientific Reports</i>, vol. 12, no. 1. Springer Nature, 2022.","short":"J. Svoboda, J. Tkadlec, A. Pavlogiannis, K. Chatterjee, M.A. Nowak, Scientific Reports 12 (2022).","chicago":"Svoboda, Jakub, Josef Tkadlec, Andreas Pavlogiannis, Krishnendu Chatterjee, and Martin A. Nowak. “Infection Dynamics of COVID-19 Virus under Lockdown and Reopening.” <i>Scientific Reports</i>. Springer Nature, 2022. <a href=\"https://doi.org/10.1038/s41598-022-05333-5\">https://doi.org/10.1038/s41598-022-05333-5</a>.","ista":"Svoboda J, Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. 2022. Infection dynamics of COVID-19 virus under lockdown and reopening. Scientific Reports. 12(1), 1526.","apa":"Svoboda, J., Tkadlec, J., Pavlogiannis, A., Chatterjee, K., &#38; Nowak, M. A. (2022). Infection dynamics of COVID-19 virus under lockdown and reopening. <i>Scientific Reports</i>. Springer Nature. <a href=\"https://doi.org/10.1038/s41598-022-05333-5\">https://doi.org/10.1038/s41598-022-05333-5</a>","mla":"Svoboda, Jakub, et al. “Infection Dynamics of COVID-19 Virus under Lockdown and Reopening.” <i>Scientific Reports</i>, vol. 12, no. 1, 1526, Springer Nature, 2022, doi:<a href=\"https://doi.org/10.1038/s41598-022-05333-5\">10.1038/s41598-022-05333-5</a>."},"issue":"1","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","oa":1,"language":[{"iso":"eng"}],"department":[{"_id":"KrCh"}],"file":[{"date_updated":"2022-02-07T14:57:59Z","creator":"alisjak","file_size":2971922,"date_created":"2022-02-07T14:57:59Z","file_id":"10744","access_level":"open_access","content_type":"application/pdf","success":1,"file_name":"2022_ScientificReports_Svoboda.pdf","checksum":"247afd30c173390940f099ead35a28ed","relation":"main_file"}],"article_number":"1526","month":"01","arxiv":1},{"date_published":"2022-09-29T00:00:00Z","acknowledgement":"K.C. acknowledges support from ERC Start Grant No. (279307: Graph Games), ERC Consolidator Grant No. (863818: ForM-SMart), and Austrian Science Fund (FWF)\r\nGrants No. P23499-N23 and No. S11407-N23 (RiSE). This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie\r\nSkłodowska-Curie Grant Agreement No. 665385.","ec_funded":1,"publication":"Physical Review E","status":"public","project":[{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"grant_number":"S11407","name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"_id":"2564DBCA-B435-11E9-9278-68D0E5697425","name":"International IST Doctoral Program","grant_number":"665385","call_identifier":"H2020"}],"external_id":{"isi":["000870243100001"],"arxiv":["2210.02394"]},"isi":1,"year":"2022","quality_controlled":"1","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2210.02394"}],"type":"journal_article","_id":"12257","date_updated":"2025-07-14T09:09:49Z","publisher":"American Physical Society","article_processing_charge":"No","doi":"10.1103/physreve.106.034321","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"chicago":"Chatterjee, Krishnendu, Jakub Svoboda, Dorde Zikelic, Andreas Pavlogiannis, and Josef Tkadlec. “Social Balance on Networks: Local Minima and Best-Edge Dynamics.” <i>Physical Review E</i>. American Physical Society, 2022. <a href=\"https://doi.org/10.1103/physreve.106.034321\">https://doi.org/10.1103/physreve.106.034321</a>.","ista":"Chatterjee K, Svoboda J, Zikelic D, Pavlogiannis A, Tkadlec J. 2022. Social balance on networks: Local minima and best-edge dynamics. Physical Review E. 106(3), 034321.","mla":"Chatterjee, Krishnendu, et al. “Social Balance on Networks: Local Minima and Best-Edge Dynamics.” <i>Physical Review E</i>, vol. 106, no. 3, 034321, American Physical Society, 2022, doi:<a href=\"https://doi.org/10.1103/physreve.106.034321\">10.1103/physreve.106.034321</a>.","apa":"Chatterjee, K., Svoboda, J., Zikelic, D., Pavlogiannis, A., &#38; Tkadlec, J. (2022). Social balance on networks: Local minima and best-edge dynamics. <i>Physical Review E</i>. American Physical Society. <a href=\"https://doi.org/10.1103/physreve.106.034321\">https://doi.org/10.1103/physreve.106.034321</a>","ama":"Chatterjee K, Svoboda J, Zikelic D, Pavlogiannis A, Tkadlec J. Social balance on networks: Local minima and best-edge dynamics. <i>Physical Review E</i>. 2022;106(3). doi:<a href=\"https://doi.org/10.1103/physreve.106.034321\">10.1103/physreve.106.034321</a>","short":"K. Chatterjee, J. Svoboda, D. Zikelic, A. Pavlogiannis, J. Tkadlec, Physical Review E 106 (2022).","ieee":"K. Chatterjee, J. Svoboda, D. Zikelic, A. Pavlogiannis, and J. Tkadlec, “Social balance on networks: Local minima and best-edge dynamics,” <i>Physical Review E</i>, vol. 106, no. 3. American Physical Society, 2022."},"issue":"3","language":[{"iso":"eng"}],"oa":1,"article_number":"034321","department":[{"_id":"KrCh"}],"arxiv":1,"month":"09","publication_status":"published","publication_identifier":{"eissn":["2470-0053"],"issn":["2470-0045"]},"abstract":[{"text":"Structural balance theory is an established framework for studying social relationships of friendship and enmity. These relationships are modeled by a signed network whose energy potential measures the level of imbalance, while stochastic dynamics drives the network toward a state of minimum energy that captures social balance. It is known that this energy landscape has local minima that can trap socially aware dynamics, preventing it from reaching balance. Here we first study the robustness and attractor properties of these local minima. We show that a stochastic process can reach them from an abundance of initial states and that some local minima cannot be escaped by mild perturbations of the network. Motivated by these anomalies, we introduce best-edge dynamics (BED), a new plausible stochastic process. We prove that BED always reaches balance and that it does so fast in various interesting settings.","lang":"eng"}],"intvolume":"       106","date_created":"2023-01-16T09:57:57Z","article_type":"original","volume":106,"oa_version":"Preprint","title":"Social balance on networks: Local minima and best-edge dynamics","day":"29","scopus_import":"1","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"last_name":"Svoboda","full_name":"Svoboda, Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","orcid":"0000-0002-1419-3267","first_name":"Jakub"},{"first_name":"Dorde","orcid":"0000-0002-4681-1699","last_name":"Zikelic","full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","first_name":"Andreas"},{"full_name":"Tkadlec, Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","last_name":"Tkadlec","orcid":"0000-0002-1097-9684","first_name":"Josef"}]},{"publisher":"Springer","doi":"10.1007/s10703-021-00373-5","article_processing_charge":"No","type":"journal_article","date_updated":"2023-10-10T11:13:20Z","_id":"9393","page":"401-428","quality_controlled":"1","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1504.07384"}],"external_id":{"arxiv":["1504.07384"],"isi":["000645490300001"]},"isi":1,"year":"2021","project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"status":"public","publication":"Formal Methods in System Design","acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499- N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start Grant (279307: Graph Games), and Microsoft faculty fellows award.","date_published":"2021-09-01T00:00:00Z","ec_funded":1,"title":"Faster algorithms for quantitative verification in bounded treewidth graphs","oa_version":"Preprint","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"orcid":"0000-0003-4783-0389","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen"},{"orcid":"0000-0002-8943-0722","first_name":"Andreas","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"day":"01","scopus_import":"1","article_type":"original","date_created":"2021-05-16T22:01:47Z","volume":57,"intvolume":"        57","abstract":[{"lang":"eng","text":"We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean-payoff, the ratio, and the minimum initial credit for energy property. The algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the graph. We consider graphs with bounded treewidth—a class that contains the control flow graphs of most programs. Let n denote the number of nodes of a graph, m the number of edges (for bounded treewidth 𝑚=𝑂(𝑛)) and W the largest absolute value of the weights. Our main theoretical results are as follows. First, for the minimum initial credit problem we show that (1) for general graphs the problem can be solved in 𝑂(𝑛2⋅𝑚) time and the associated decision problem in 𝑂(𝑛⋅𝑚) time, improving the previous known 𝑂(𝑛3⋅𝑚⋅log(𝑛⋅𝑊)) and 𝑂(𝑛2⋅𝑚) bounds, respectively; and (2) for bounded treewidth graphs we present an algorithm that requires 𝑂(𝑛⋅log𝑛) time. Second, for bounded treewidth graphs we present an algorithm that approximates the mean-payoff value within a factor of 1+𝜖 in time 𝑂(𝑛⋅log(𝑛/𝜖)) as compared to the classical exact algorithms on general graphs that require quadratic time. Third, for the ratio property we present an algorithm that for bounded treewidth graphs works in time 𝑂(𝑛⋅log(|𝑎⋅𝑏|))=𝑂(𝑛⋅log(𝑛⋅𝑊)), when the output is 𝑎𝑏, as compared to the previously best known algorithm on general graphs with running time 𝑂(𝑛2⋅log(𝑛⋅𝑊)). We have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks."}],"publication_status":"published","publication_identifier":{"eissn":["1572-8102"],"issn":["0925-9856"]},"arxiv":1,"month":"09","department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Faster algorithms for quantitative verification in bounded treewidth graphs. <i>Formal Methods in System Design</i>. 2021;57:401-428. doi:<a href=\"https://doi.org/10.1007/s10703-021-00373-5\">10.1007/s10703-021-00373-5</a>","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Formal Methods in System Design 57 (2021) 401–428.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for quantitative verification in bounded treewidth graphs,” <i>Formal Methods in System Design</i>, vol. 57. Springer, pp. 401–428, 2021.","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2021. Faster algorithms for quantitative verification in bounded treewidth graphs. Formal Methods in System Design. 57, 401–428.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Faster Algorithms for Quantitative Verification in Bounded Treewidth Graphs.” <i>Formal Methods in System Design</i>. Springer, 2021. <a href=\"https://doi.org/10.1007/s10703-021-00373-5\">https://doi.org/10.1007/s10703-021-00373-5</a>.","mla":"Chatterjee, Krishnendu, et al. “Faster Algorithms for Quantitative Verification in Bounded Treewidth Graphs.” <i>Formal Methods in System Design</i>, vol. 57, Springer, 2021, pp. 401–28, doi:<a href=\"https://doi.org/10.1007/s10703-021-00373-5\">10.1007/s10703-021-00373-5</a>.","apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2021). Faster algorithms for quantitative verification in bounded treewidth graphs. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1007/s10703-021-00373-5\">https://doi.org/10.1007/s10703-021-00373-5</a>"}},{"publication_status":"published","publication_identifier":{"eissn":["20411723"]},"file_date_updated":"2021-07-19T13:02:20Z","abstract":[{"text":"Selection and random drift determine the probability that novel mutations fixate in a population. Population structure is known to affect the dynamics of the evolutionary process. Amplifiers of selection are population structures that increase the fixation probability of beneficial mutants compared to well-mixed populations. Over the past 15 years, extensive research has produced remarkable structures called strong amplifiers which guarantee that every beneficial mutation fixates with high probability. But strong amplification has come at the cost of considerably delaying the fixation event, which can slow down the overall rate of evolution. However, the precise relationship between fixation probability and time has remained elusive. Here we characterize the slowdown effect of strong amplification. First, we prove that all strong amplifiers must delay the fixation event at least to some extent. Second, we construct strong amplifiers that delay the fixation event only marginally as compared to the well-mixed populations. Our results thus establish a tight relationship between fixation probability and time: Strong amplification always comes at a cost of a slowdown, but more than a marginal slowdown is not needed.","lang":"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","image":"/images/cc_by.png","short":"CC BY (4.0)"},"intvolume":"        12","has_accepted_license":"1","article_type":"original","date_created":"2021-07-11T22:01:15Z","volume":12,"title":"Fast and strong amplifiers of natural selection","oa_version":"Published Version","author":[{"last_name":"Tkadlec","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","full_name":"Tkadlec, Josef","orcid":"0000-0002-1097-9684","first_name":"Josef"},{"first_name":"Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis"},{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"first_name":"Martin A.","last_name":"Nowak","full_name":"Nowak, Martin A."}],"day":"29","scopus_import":"1","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","issue":"1","citation":{"ama":"Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. Fast and strong amplifiers of natural selection. <i>Nature Communications</i>. 2021;12(1). doi:<a href=\"https://doi.org/10.1038/s41467-021-24271-w\">10.1038/s41467-021-24271-w</a>","short":"J. Tkadlec, A. Pavlogiannis, K. Chatterjee, M.A. Nowak, Nature Communications 12 (2021).","ieee":"J. Tkadlec, A. Pavlogiannis, K. Chatterjee, and M. A. Nowak, “Fast and strong amplifiers of natural selection,” <i>Nature Communications</i>, vol. 12, no. 1. Springer Nature, 2021.","chicago":"Tkadlec, Josef, Andreas Pavlogiannis, Krishnendu Chatterjee, and Martin A. Nowak. “Fast and Strong Amplifiers of Natural Selection.” <i>Nature Communications</i>. Springer Nature, 2021. <a href=\"https://doi.org/10.1038/s41467-021-24271-w\">https://doi.org/10.1038/s41467-021-24271-w</a>.","ista":"Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. 2021. Fast and strong amplifiers of natural selection. Nature Communications. 12(1), 4009.","mla":"Tkadlec, Josef, et al. “Fast and Strong Amplifiers of Natural Selection.” <i>Nature Communications</i>, vol. 12, no. 1, 4009, Springer Nature, 2021, doi:<a href=\"https://doi.org/10.1038/s41467-021-24271-w\">10.1038/s41467-021-24271-w</a>.","apa":"Tkadlec, J., Pavlogiannis, A., Chatterjee, K., &#38; Nowak, M. A. (2021). Fast and strong amplifiers of natural selection. <i>Nature Communications</i>. Springer Nature. <a href=\"https://doi.org/10.1038/s41467-021-24271-w\">https://doi.org/10.1038/s41467-021-24271-w</a>"},"language":[{"iso":"eng"}],"oa":1,"file":[{"content_type":"application/pdf","access_level":"open_access","file_name":"2021_NatCoom_Tkadlec.pdf","success":1,"checksum":"5767418926a7f7fb76151de29473dae0","relation":"main_file","creator":"cziletti","date_updated":"2021-07-19T13:02:20Z","date_created":"2021-07-19T13:02:20Z","file_size":628992,"file_id":"9692"}],"article_number":"4009","department":[{"_id":"KrCh"}],"month":"06","quality_controlled":"1","ddc":["510"],"type":"journal_article","date_updated":"2025-07-14T09:10:05Z","_id":"9640","publisher":"Springer Nature","doi":"10.1038/s41467-021-24271-w","article_processing_charge":"No","acknowledgement":"K.C. acknowledges support from ERC Start grant no. (279307: Graph Games), ERC Consolidator grant no. (863818: ForM-SMart), Austrian Science Fund (FWF) grant no. P23499-N23 and S11407-N23 (RiSE). M.A.N. acknowledges support from Office of Naval Research grant N00014-16-1-2914 and from the John Templeton Foundation.","date_published":"2021-06-29T00:00:00Z","pmid":1,"ec_funded":1,"project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"},{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"publication":"Nature Communications","status":"public","external_id":{"pmid":["34188036"],"isi":["000671752100003"]},"year":"2021","isi":1},{"citation":{"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.","short":"T.L. Bui, K. Chatterjee, T. Gautam, A. Pavlogiannis, V. Toman, Proceedings of the ACM on Programming Languages 5 (2021).","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>","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>","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>.","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>.","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."},"issue":"OOPSLA","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","oa":1,"language":[{"iso":"eng"}],"department":[{"_id":"GradSch"},{"_id":"KrCh"}],"article_number":"164","file":[{"file_size":2903485,"date_created":"2021-11-04T07:24:48Z","date_updated":"2021-11-04T07:24:48Z","creator":"cchlebak","file_id":"10215","success":1,"file_name":"2021_ProcACMPL_Bui.pdf","access_level":"open_access","content_type":"application/pdf","relation":"main_file","checksum":"9d6dce7b611853c529bb7b1915ac579e"}],"arxiv":1,"month":"10","file_date_updated":"2021-11-04T07:24:48Z","publication_status":"published","publication_identifier":{"eissn":["2475-1421"]},"has_accepted_license":"1","intvolume":"         5","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","image":"/images/cc_by.png","short":"CC BY (4.0)"},"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"}],"volume":5,"date_created":"2021-10-27T15:05:34Z","article_type":"original","day":"15","scopus_import":"1","author":[{"first_name":"Truc Lam","full_name":"Bui, Truc Lam","last_name":"Bui"},{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"first_name":"Tushar","full_name":"Gautam, Tushar","last_name":"Gautam"},{"first_name":"Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis"},{"last_name":"Toman","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","full_name":"Toman, Viktor","first_name":"Viktor","orcid":"0000-0001-9036-063X"}],"title":"The reads-from equivalence for the TSO and PSO memory models","oa_version":"Published Version","ec_funded":1,"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.","date_published":"2021-10-15T00:00:00Z","publication":"Proceedings of the ACM on Programming Languages","status":"public","project":[{"call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"}],"keyword":["safety","risk","reliability and quality","software"],"year":"2021","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"10199"}]},"external_id":{"arxiv":["2011.11763"]},"quality_controlled":"1","ddc":["000"],"_id":"10191","date_updated":"2025-07-14T09:10:16Z","type":"journal_article","article_processing_charge":"No","doi":"10.1145/3485541","publisher":"Association for Computing Machinery"},{"date_created":"2022-01-16T23:01:28Z","volume":213,"oa_version":"Published Version","title":"Quantitative verification on product graphs of small treewidth","author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","first_name":"Rasmus","orcid":"0000-0003-4783-0389"},{"first_name":"Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"day":"29","scopus_import":"1","publication_identifier":{"isbn":["978-3-9597-7215-0"],"issn":["1868-8969"]},"publication_status":"published","file_date_updated":"2022-01-17T10:36:08Z","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","image":"/images/cc_by.png","short":"CC BY (4.0)"},"abstract":[{"text":"Product graphs arise naturally in formal verification and program analysis. For example, the analysis of two concurrent threads requires the product of two component control-flow graphs, and for language inclusion of deterministic automata the product of two automata is constructed. In many cases, the component graphs have constant treewidth, e.g., when the input contains control-flow graphs of programs. We consider the algorithmic analysis of products of two constant-treewidth graphs with respect to three classic specification languages, namely, (a) algebraic properties, (b) mean-payoff properties, and (c) initial credit for energy properties.\r\nOur main contributions are as follows. Consider a graph G that is the product of two constant-treewidth graphs of size n each. First, given an idempotent semiring, we present an algorithm that computes the semiring transitive closure of G in time Õ(n⁴). Since the output has size Θ(n⁴), our algorithm is optimal (up to polylog factors). Second, given a mean-payoff objective, we present an O(n³)-time algorithm for deciding whether the value of a starting state is non-negative, improving the previously known O(n⁴) bound. Third, given an initial credit for energy objective, we present an O(n⁵)-time algorithm for computing the minimum initial credit for all nodes of G, improving the previously known O(n⁸) bound. At the heart of our approach lies an algorithm for the efficient construction of strongly-balanced tree decompositions of constant-treewidth graphs. Given a constant-treewidth graph G' of n nodes and a positive integer λ, our algorithm constructs a binary tree decomposition of G' of width O(λ) with the property that the size of each subtree decreases geometrically with rate (1/2 + 2^{-λ}).","lang":"eng"}],"intvolume":"       213","has_accepted_license":"1","file":[{"success":1,"file_name":"2021_LIPIcs_Chatterjee.pdf","access_level":"open_access","content_type":"application/pdf","relation":"main_file","checksum":"71141acdeffa9056f24d6dbef952d254","file_size":891566,"date_created":"2022-01-17T10:36:08Z","date_updated":"2022-01-17T10:36:08Z","creator":"cchlebak","file_id":"10633"}],"article_number":"42","department":[{"_id":"KrCh"}],"month":"11","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","citation":{"ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Quantitative verification on product graphs of small treewidth,” in <i>41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, Virtual, 2021, vol. 213.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, in:, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Quantitative verification on product graphs of small treewidth. In: <i>41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>. Vol 213. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2021. doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2021.42\">10.4230/LIPIcs.FSTTCS.2021.42</a>","apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2021). Quantitative verification on product graphs of small treewidth. In <i>41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i> (Vol. 213). Virtual: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2021.42\">https://doi.org/10.4230/LIPIcs.FSTTCS.2021.42</a>","mla":"Chatterjee, Krishnendu, et al. “Quantitative Verification on Product Graphs of Small Treewidth.” <i>41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, vol. 213, 42, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021, doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2021.42\">10.4230/LIPIcs.FSTTCS.2021.42</a>.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Quantitative Verification on Product Graphs of Small Treewidth.” In <i>41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, Vol. 213. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. <a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2021.42\">https://doi.org/10.4230/LIPIcs.FSTTCS.2021.42</a>.","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2021. Quantitative verification on product graphs of small treewidth. 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. FSTTCS: Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol. 213, 42."},"language":[{"iso":"eng"}],"oa":1,"type":"conference","date_updated":"2022-01-17T10:39:40Z","_id":"10629","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","doi":"10.4230/LIPIcs.FSTTCS.2021.42","alternative_title":["LIPIcs"],"article_processing_charge":"No","quality_controlled":"1","ddc":["000"],"year":"2021","date_published":"2021-11-29T00:00:00Z","conference":{"location":"Virtual","end_date":"2021-12-17","start_date":"2021-12-15","name":"FSTTCS: Foundations of Software Technology and Theoretical Computer Science"},"publication":"41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science","status":"public"},{"publication_identifier":{"eissn":["1611-3349"],"eisbn":["978-3-030-81685-8"],"issn":["0302-9743"],"isbn":["978-3-030-81684-1"]},"publication_status":"published","file_date_updated":"2022-05-13T07:00:20Z","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","image":"/images/cc_by.png","short":"CC BY (4.0)"},"abstract":[{"lang":"eng","text":"Stateless model checking (SMC) is one of the standard approaches to the verification of concurrent programs. As scheduling non-determinism creates exponentially large spaces of thread interleavings, SMC attempts to partition this space into equivalence classes and explore only a few representatives from each class. The efficiency of this approach depends on two factors: (a) the coarseness of the partitioning, and (b) the time to generate representatives in each class. For this reason, the search for coarse partitionings that are efficiently explorable is an active research challenge. In this work we present   RVF-SMC , a new SMC algorithm that uses a novel reads-value-from (RVF) partitioning. Intuitively, two interleavings are deemed equivalent if they agree on the value obtained in each read event, and read events induce consistent causal orderings between them. The RVF partitioning is provably coarser than recent approaches based on Mazurkiewicz and “reads-from” partitionings. Our experimental evaluation reveals that RVF is quite often a very effective equivalence, as the underlying partitioning is exponentially coarser than other approaches. Moreover,   RVF-SMC  generates representatives very efficiently, as the reduction in the partitioning is often met with significant speed-ups in the model checking task."}],"has_accepted_license":"1","date_created":"2021-09-05T22:01:24Z","volume":"12759 ","oa_version":"Published Version","title":"Stateless model checking under a reads-value-from equivalence","author":[{"full_name":"Agarwal, Pratyush","last_name":"Agarwal","first_name":"Pratyush"},{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"last_name":"Pathak","full_name":"Pathak, Shreya","first_name":"Shreya"},{"last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","first_name":"Andreas"},{"id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","full_name":"Toman, Viktor","last_name":"Toman","first_name":"Viktor","orcid":"0000-0001-9036-063X"}],"day":"15","scopus_import":"1","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"ama":"Agarwal P, Chatterjee K, Pathak S, Pavlogiannis A, Toman V. Stateless model checking under a reads-value-from equivalence. In: <i>33rd International Conference on Computer-Aided Verification </i>. Vol 12759. Springer Nature; 2021:341-366. doi:<a href=\"https://doi.org/10.1007/978-3-030-81685-8_16\">10.1007/978-3-030-81685-8_16</a>","ieee":"P. Agarwal, K. Chatterjee, S. Pathak, A. Pavlogiannis, and V. Toman, “Stateless model checking under a reads-value-from equivalence,” in <i>33rd International Conference on Computer-Aided Verification </i>, Virtual, 2021, vol. 12759, pp. 341–366.","short":"P. Agarwal, K. Chatterjee, S. Pathak, A. Pavlogiannis, V. Toman, in:, 33rd International Conference on Computer-Aided Verification , Springer Nature, 2021, pp. 341–366.","chicago":"Agarwal, Pratyush, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis, and Viktor Toman. “Stateless Model Checking under a Reads-Value-from Equivalence.” In <i>33rd International Conference on Computer-Aided Verification </i>, 12759:341–66. Springer Nature, 2021. <a href=\"https://doi.org/10.1007/978-3-030-81685-8_16\">https://doi.org/10.1007/978-3-030-81685-8_16</a>.","ista":"Agarwal P, Chatterjee K, Pathak S, Pavlogiannis A, Toman V. 2021. Stateless model checking under a reads-value-from equivalence. 33rd International Conference on Computer-Aided Verification . CAV: Computer Aided Verification , LNCS, vol. 12759, 341–366.","apa":"Agarwal, P., Chatterjee, K., Pathak, S., Pavlogiannis, A., &#38; Toman, V. (2021). Stateless model checking under a reads-value-from equivalence. In <i>33rd International Conference on Computer-Aided Verification </i> (Vol. 12759, pp. 341–366). Virtual: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-81685-8_16\">https://doi.org/10.1007/978-3-030-81685-8_16</a>","mla":"Agarwal, Pratyush, et al. “Stateless Model Checking under a Reads-Value-from Equivalence.” <i>33rd International Conference on Computer-Aided Verification </i>, vol. 12759, Springer Nature, 2021, pp. 341–66, doi:<a href=\"https://doi.org/10.1007/978-3-030-81685-8_16\">10.1007/978-3-030-81685-8_16</a>."},"language":[{"iso":"eng"}],"oa":1,"file":[{"creator":"dernst","date_updated":"2022-05-13T07:00:20Z","date_created":"2022-05-13T07:00:20Z","file_size":1516756,"file_id":"11368","access_level":"open_access","content_type":"application/pdf","success":1,"file_name":"2021_LNCS_Agarwal.pdf","checksum":"4b346e5fbaa8b9bdf107819c7b2aadee","relation":"main_file"}],"department":[{"_id":"KrCh"}],"arxiv":1,"month":"07","quality_controlled":"1","ddc":["000"],"page":"341-366","type":"conference","date_updated":"2025-07-14T09:10:15Z","_id":"9987","publisher":"Springer Nature","doi":"10.1007/978-3-030-81685-8_16","article_processing_charge":"Yes","alternative_title":["LNCS"],"date_published":"2021-07-15T00:00:00Z","acknowledgement":"The research was partially funded by the ERC CoG 863818 (ForM-SMArt) and the Vienna Science and Technology Fund (WWTF) through project ICT15-003.","conference":{"location":"Virtual","name":"CAV: Computer Aided Verification ","start_date":"2021-07-20","end_date":"2021-07-23"},"ec_funded":1,"project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"}],"publication":"33rd International Conference on Computer-Aided Verification ","status":"public","external_id":{"isi":["000698732400016"],"arxiv":["2105.06424"]},"related_material":{"record":[{"id":"10199","status":"public","relation":"dissertation_contains"}]},"year":"2021","isi":1},{"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"ista":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Pavlogiannis A. 2020. Optimal and perfectly parallel algorithms for on-demand data-flow analysis. European Symposium on Programming. ESOP: Programming Languages and Systems, LNCS, vol. 12075, 112–140.","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Optimal and Perfectly Parallel Algorithms for On-Demand Data-Flow Analysis.” In <i>European Symposium on Programming</i>, 12075:112–40. Springer Nature, 2020. <a href=\"https://doi.org/10.1007/978-3-030-44914-8_5\">https://doi.org/10.1007/978-3-030-44914-8_5</a>.","apa":"Chatterjee, K., Goharshady, A. K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2020). Optimal and perfectly parallel algorithms for on-demand data-flow analysis. In <i>European Symposium on Programming</i> (Vol. 12075, pp. 112–140). Dublin, Ireland: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-44914-8_5\">https://doi.org/10.1007/978-3-030-44914-8_5</a>","mla":"Chatterjee, Krishnendu, et al. “Optimal and Perfectly Parallel Algorithms for On-Demand Data-Flow Analysis.” <i>European Symposium on Programming</i>, vol. 12075, Springer Nature, 2020, pp. 112–40, doi:<a href=\"https://doi.org/10.1007/978-3-030-44914-8_5\">10.1007/978-3-030-44914-8_5</a>.","ama":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Pavlogiannis A. Optimal and perfectly parallel algorithms for on-demand data-flow analysis. In: <i>European Symposium on Programming</i>. Vol 12075. Springer Nature; 2020:112-140. doi:<a href=\"https://doi.org/10.1007/978-3-030-44914-8_5\">10.1007/978-3-030-44914-8_5</a>","ieee":"K. Chatterjee, A. K. Goharshady, R. Ibsen-Jensen, and A. Pavlogiannis, “Optimal and perfectly parallel algorithms for on-demand data-flow analysis,” in <i>European Symposium on Programming</i>, Dublin, Ireland, 2020, vol. 12075, pp. 112–140.","short":"K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, A. Pavlogiannis, in:, European Symposium on Programming, Springer Nature, 2020, pp. 112–140."},"language":[{"iso":"eng"}],"oa":1,"file":[{"date_created":"2020-05-26T13:34:48Z","file_size":651250,"creator":"dernst","date_updated":"2020-07-14T12:48:03Z","file_id":"7895","file_name":"2020_LNCS_Chatterjee.pdf","content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"8618b80f4cf7b39a60e61a6445ad9807"}],"department":[{"_id":"KrCh"}],"month":"04","file_date_updated":"2020-07-14T12:48:03Z","publication_identifier":{"isbn":["9783030449131"],"issn":["03029743"],"eissn":["16113349"]},"publication_status":"published","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","image":"/images/cc_by.png","short":"CC BY (4.0)"},"intvolume":"     12075","abstract":[{"text":"Interprocedural data-flow analyses form an expressive and useful paradigm of numerous static analysis applications, such as live variables analysis, alias analysis and null pointers analysis. The most widely-used framework for interprocedural data-flow analysis is IFDS, which encompasses distributive data-flow functions over a finite domain. On-demand data-flow analyses restrict the focus of the analysis on specific program locations and data facts. This setting provides a natural split between (i) an offline (or preprocessing) phase, where the program is partially analyzed and analysis summaries are created, and (ii) an online (or query) phase, where analysis queries arrive on demand and the summaries are used to speed up answering queries.\r\nIn this work, we consider on-demand IFDS analyses where the queries concern program locations of the same procedure (aka same-context queries). We exploit the fact that flow graphs of programs have low treewidth to develop faster algorithms that are space and time optimal for many common data-flow analyses, in both the preprocessing and the query phase. We also use treewidth to develop query solutions that are embarrassingly parallelizable, i.e. the total work for answering each query is split to a number of threads such that each thread performs only a constant amount of work. Finally, we implement a static analyzer based on our algorithms, and perform a series of on-demand analysis experiments on standard benchmarks. Our experimental results show a drastic speed-up of the queries after only a lightweight preprocessing phase, which significantly outperforms existing techniques.","lang":"eng"}],"has_accepted_license":"1","date_created":"2020-05-10T22:00:50Z","volume":12075,"title":"Optimal and perfectly parallel algorithms for on-demand data-flow analysis","oa_version":"Published Version","day":"18","scopus_import":"1","author":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0003-1702-6584","first_name":"Amir Kafshdar","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87","full_name":"Goharshady, Amir Kafshdar"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389","first_name":"Rasmus"},{"last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","first_name":"Andreas"}],"date_published":"2020-04-18T00:00:00Z","conference":{"location":"Dublin, Ireland","name":"ESOP: Programming Languages and Systems","end_date":"2020-04-30","start_date":"2020-04-25"},"status":"public","publication":"European Symposium on Programming","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"},{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"_id":"266EEEC0-B435-11E9-9278-68D0E5697425","name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts"},{"_id":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies"}],"related_material":{"record":[{"id":"8934","relation":"dissertation_contains","status":"public"}]},"external_id":{"isi":["000681656800005"]},"year":"2020","isi":1,"quality_controlled":"1","ddc":["000"],"page":"112-140","type":"conference","_id":"7810","date_updated":"2025-06-02T08:53:42Z","publisher":"Springer Nature","article_processing_charge":"No","alternative_title":["LNCS"],"doi":"10.1007/978-3-030-44914-8_5"},{"publisher":"Springer Nature","article_processing_charge":"No","alternative_title":["LNCS"],"doi":"10.1007/978-3-030-59152-6_14","type":"conference","_id":"8728","date_updated":"2025-06-02T08:53:43Z","ddc":["000"],"page":"253-270","quality_controlled":"1","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"8934"}]},"external_id":{"isi":["000723555700014"]},"year":"2020","isi":1,"publication":"Automated Technology for Verification and Analysis","status":"public","project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"},{"_id":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies"}],"date_published":"2020-10-12T00:00:00Z","conference":{"start_date":"2020-10-19","end_date":"2020-10-23","name":"ATVA: Automated Technology for Verification and Analysis","location":"Hanoi, Vietnam"},"title":"Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth","oa_version":"Submitted Version","day":"12","scopus_import":"1","author":[{"full_name":"Asadi, Ali","last_name":"Asadi","first_name":"Ali"},{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"last_name":"Goharshady","full_name":"Goharshady, Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1702-6584","first_name":"Amir Kafshdar"},{"first_name":"Kiarash","last_name":"Mohammadi","full_name":"Mohammadi, Kiarash"},{"orcid":"0000-0002-8943-0722","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis"}],"date_created":"2020-11-06T07:30:05Z","volume":12302,"abstract":[{"lang":"eng","text":"Discrete-time Markov Chains (MCs) and Markov Decision Processes (MDPs) are two standard formalisms in system analysis. Their main associated quantitative objectives are hitting probabilities, discounted sum, and mean payoff. Although there are many techniques for computing these objectives in general MCs/MDPs, they have not been thoroughly studied in terms of parameterized algorithms, particularly when treewidth is used as the parameter. This is in sharp contrast to qualitative objectives for MCs, MDPs and graph games, for which treewidth-based algorithms yield significant complexity improvements. In this work, we show that treewidth can also be used to obtain faster algorithms for the quantitative problems. For an MC with n states and m transitions, we show that each of the classical quantitative objectives can be computed in   O((n+m)⋅t2)  time, given a tree decomposition of the MC with width t. Our results also imply a bound of   O(κ⋅(n+m)⋅t2)  for each objective on MDPs, where   κ  is the number of strategy-iteration refinements required for the given input and objective. Finally, we make an experimental evaluation of our new algorithms on low-treewidth MCs and MDPs obtained from the DaCapo benchmark suite. Our experiments show that on low-treewidth MCs and MDPs, our algorithms outperform existing well-established methods by one or more orders of magnitude."}],"intvolume":"     12302","has_accepted_license":"1","file_date_updated":"2020-11-06T07:41:03Z","publication_status":"published","publication_identifier":{"eisbn":["9783030591526"],"eissn":["1611-3349"],"isbn":["9783030591519"],"issn":["0302-9743"]},"month":"10","file":[{"date_updated":"2020-11-06T07:41:03Z","creator":"dernst","date_created":"2020-11-06T07:41:03Z","file_size":726648,"file_id":"8729","access_level":"open_access","content_type":"application/pdf","success":1,"file_name":"2020_LNCS_ATVA_Asadi_accepted.pdf","checksum":"ae83f27e5b189d5abc2e7514f1b7e1b5","relation":"main_file"}],"department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"oa":1,"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"ama":"Asadi A, Chatterjee K, Goharshady AK, Mohammadi K, Pavlogiannis A. Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth. In: <i>Automated Technology for Verification and Analysis</i>. Vol 12302. Springer Nature; 2020:253-270. doi:<a href=\"https://doi.org/10.1007/978-3-030-59152-6_14\">10.1007/978-3-030-59152-6_14</a>","short":"A. Asadi, K. Chatterjee, A.K. Goharshady, K. Mohammadi, A. Pavlogiannis, in:, Automated Technology for Verification and Analysis, Springer Nature, 2020, pp. 253–270.","ieee":"A. Asadi, K. Chatterjee, A. K. Goharshady, K. Mohammadi, and A. Pavlogiannis, “Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth,” in <i>Automated Technology for Verification and Analysis</i>, Hanoi, Vietnam, 2020, vol. 12302, pp. 253–270.","chicago":"Asadi, Ali, Krishnendu Chatterjee, Amir Kafshdar Goharshady, Kiarash Mohammadi, and Andreas Pavlogiannis. “Faster Algorithms for Quantitative Analysis of MCs and MDPs with Small Treewidth.” In <i>Automated Technology for Verification and Analysis</i>, 12302:253–70. Springer Nature, 2020. <a href=\"https://doi.org/10.1007/978-3-030-59152-6_14\">https://doi.org/10.1007/978-3-030-59152-6_14</a>.","ista":"Asadi A, Chatterjee K, Goharshady AK, Mohammadi K, Pavlogiannis A. 2020. Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth. Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 12302, 253–270.","mla":"Asadi, Ali, et al. “Faster Algorithms for Quantitative Analysis of MCs and MDPs with Small Treewidth.” <i>Automated Technology for Verification and Analysis</i>, vol. 12302, Springer Nature, 2020, pp. 253–70, doi:<a href=\"https://doi.org/10.1007/978-3-030-59152-6_14\">10.1007/978-3-030-59152-6_14</a>.","apa":"Asadi, A., Chatterjee, K., Goharshady, A. K., Mohammadi, K., &#38; Pavlogiannis, A. (2020). Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth. In <i>Automated Technology for Verification and Analysis</i> (Vol. 12302, pp. 253–270). Hanoi, Vietnam: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-59152-6_14\">https://doi.org/10.1007/978-3-030-59152-6_14</a>"}},{"department":[{"_id":"KrCh"}],"month":"11","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","issue":"11","citation":{"short":"A. Pavlogiannis, N. Schaumberger, U. Schmid, K. Chatterjee, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 39 (2020) 3981–3992.","ieee":"A. Pavlogiannis, N. Schaumberger, U. Schmid, and K. Chatterjee, “Precedence-aware automated competitive analysis of real-time scheduling,” <i>IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems</i>, vol. 39, no. 11. IEEE, pp. 3981–3992, 2020.","ama":"Pavlogiannis A, Schaumberger N, Schmid U, Chatterjee K. Precedence-aware automated competitive analysis of real-time scheduling. <i>IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems</i>. 2020;39(11):3981-3992. doi:<a href=\"https://doi.org/10.1109/TCAD.2020.3012803\">10.1109/TCAD.2020.3012803</a>","mla":"Pavlogiannis, Andreas, et al. “Precedence-Aware Automated Competitive Analysis of Real-Time Scheduling.” <i>IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems</i>, vol. 39, no. 11, IEEE, 2020, pp. 3981–92, doi:<a href=\"https://doi.org/10.1109/TCAD.2020.3012803\">10.1109/TCAD.2020.3012803</a>.","apa":"Pavlogiannis, A., Schaumberger, N., Schmid, U., &#38; Chatterjee, K. (2020). Precedence-aware automated competitive analysis of real-time scheduling. <i>IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems</i>. IEEE. <a href=\"https://doi.org/10.1109/TCAD.2020.3012803\">https://doi.org/10.1109/TCAD.2020.3012803</a>","chicago":"Pavlogiannis, Andreas, Nico Schaumberger, Ulrich Schmid, and Krishnendu Chatterjee. “Precedence-Aware Automated Competitive Analysis of Real-Time Scheduling.” <i>IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems</i>. IEEE, 2020. <a href=\"https://doi.org/10.1109/TCAD.2020.3012803\">https://doi.org/10.1109/TCAD.2020.3012803</a>.","ista":"Pavlogiannis A, Schaumberger N, Schmid U, Chatterjee K. 2020. Precedence-aware automated competitive analysis of real-time scheduling. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. 39(11), 3981–3992."},"language":[{"iso":"eng"}],"article_type":"original","date_created":"2020-11-22T23:01:24Z","volume":39,"oa_version":"None","title":"Precedence-aware automated competitive analysis of real-time scheduling","author":[{"first_name":"Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas"},{"last_name":"Schaumberger","full_name":"Schaumberger, Nico","first_name":"Nico"},{"first_name":"Ulrich","full_name":"Schmid, Ulrich","last_name":"Schmid"},{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"}],"scopus_import":"1","day":"01","publication_status":"published","publication_identifier":{"eissn":["19374151"],"issn":["02780070"]},"intvolume":"        39","abstract":[{"text":"We consider a real-time setting where an environment releases sequences of firm-deadline tasks, and an online scheduler chooses on-the-fly the ones to execute on a single processor so as to maximize cumulated utility. The competitive ratio is a well-known performance measure for the scheduler: it gives the worst-case ratio, among all possible choices for the environment, of the cumulated utility of the online scheduler versus an offline scheduler that knows these choices in advance. Traditionally, competitive analysis is performed by hand, while automated techniques are rare and only handle static environments with independent tasks. We present a quantitative-verification framework for precedence-aware competitive analysis, where task releases may depend on preceding scheduling choices, i.e., the environment can respond to scheduling decisions dynamically . We consider two general classes of precedences: 1) follower precedences force the release of a dependent task upon the completion of a set of precursor tasks, while and 2) pairing precedences modify the characteristics of a dependent task provided the completion of a set of precursor tasks. Precedences make competitive analysis challenging, as the online and offline schedulers operate on diverging sequences. We make a formal presentation of our framework, and use a GPU-based implementation to analyze ten well-known schedulers on precedence-based application examples taken from the existing literature: 1) a handshake protocol (HP); 2) network packet-switching; 3) query scheduling (QS); and 4) a sporadic-interrupt setting. Our experimental results show that precedences and task parameters can vary drastically the best scheduler. Our framework thus supports application designers in choosing the best scheduler among a given set automatically.","lang":"eng"}],"external_id":{"isi":["000587712700069"]},"year":"2020","isi":1,"date_published":"2020-11-01T00:00:00Z","acknowledgement":"This work was supported by the Austrian Science Foundation (FWF) under the NFN RiSE/SHiNE under Grant S11405 and Grant S11407. This article was presented in the International Conference on Embedded Software 2020 and appears as part of the ESWEEK-TCAD special issue. ","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407","call_identifier":"FWF"}],"publication":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems","status":"public","type":"journal_article","date_updated":"2023-08-22T13:27:05Z","_id":"8788","publisher":"IEEE","doi":"10.1109/TCAD.2020.3012803","article_processing_charge":"No","quality_controlled":"1","page":"3981-3992"},{"quality_controlled":"1","ddc":["000"],"_id":"7212","date_updated":"2023-10-17T12:29:47Z","type":"journal_article","article_processing_charge":"No","doi":"10.1371/journal.pcbi.1007494","publisher":"Public Library of Science","ec_funded":1,"date_published":"2020-01-17T00:00:00Z","publication":"PLoS computational biology","status":"public","project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory","call_identifier":"FWF"}],"year":"2020","isi":1,"related_material":{"record":[{"status":"public","relation":"part_of_dissertation","id":"7196"}]},"external_id":{"isi":["000510916500025"],"arxiv":["1906.02785"]},"file_date_updated":"2020-07-14T12:47:53Z","publication_identifier":{"eissn":["15537358"]},"publication_status":"published","has_accepted_license":"1","intvolume":"        16","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","image":"/images/cc_by.png","short":"CC BY (4.0)"},"abstract":[{"lang":"eng","text":"The fixation probability of a single mutant invading a population of residents is among the most widely-studied quantities in evolutionary dynamics. Amplifiers of natural selection are population structures that increase the fixation probability of advantageous mutants, compared to well-mixed populations. Extensive studies have shown that many amplifiers exist for the Birth-death Moran process, some of them substantially increasing the fixation probability or even guaranteeing fixation in the limit of large population size. On the other hand, no amplifiers are known for the death-Birth Moran process, and computer-assisted exhaustive searches have failed to discover amplification. In this work we resolve this disparity, by showing that any amplification under death-Birth updating is necessarily bounded and transient. Our boundedness result states that even if a population structure does amplify selection, the resulting fixation probability is close to that of the well-mixed population. Our transience result states that for any population structure there exists a threshold r⋆ such that the population structure ceases to amplify selection if the mutant fitness advantage r is larger than r⋆. Finally, we also extend the above results to δ-death-Birth updating, which is a combination of Birth-death and death-Birth updating. On the positive side, we identify population structures that maintain amplification for a wide range of values r and δ. These results demonstrate that amplification of natural selection depends on the specific mechanisms of the evolutionary process."}],"volume":16,"date_created":"2019-12-23T13:45:11Z","article_type":"original","day":"17","scopus_import":"1","author":[{"orcid":"0000-0002-1097-9684","first_name":"Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","full_name":"Tkadlec, Josef","last_name":"Tkadlec"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis","first_name":"Andreas","orcid":"0000-0002-8943-0722"},{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Nowak","full_name":"Nowak, Martin A.","first_name":"Martin A."}],"oa_version":"Published Version","title":"Limits on amplifiers of natural selection under death-Birth updating","citation":{"short":"J. Tkadlec, A. Pavlogiannis, K. Chatterjee, M.A. Nowak, PLoS Computational Biology 16 (2020).","ieee":"J. Tkadlec, A. Pavlogiannis, K. Chatterjee, and M. A. Nowak, “Limits on amplifiers of natural selection under death-Birth updating,” <i>PLoS computational biology</i>, vol. 16. Public Library of Science, 2020.","ama":"Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. Limits on amplifiers of natural selection under death-Birth updating. <i>PLoS computational biology</i>. 2020;16. doi:<a href=\"https://doi.org/10.1371/journal.pcbi.1007494\">10.1371/journal.pcbi.1007494</a>","mla":"Tkadlec, Josef, et al. “Limits on Amplifiers of Natural Selection under Death-Birth Updating.” <i>PLoS Computational Biology</i>, vol. 16, e1007494, Public Library of Science, 2020, doi:<a href=\"https://doi.org/10.1371/journal.pcbi.1007494\">10.1371/journal.pcbi.1007494</a>.","apa":"Tkadlec, J., Pavlogiannis, A., Chatterjee, K., &#38; Nowak, M. A. (2020). Limits on amplifiers of natural selection under death-Birth updating. <i>PLoS Computational Biology</i>. Public Library of Science. <a href=\"https://doi.org/10.1371/journal.pcbi.1007494\">https://doi.org/10.1371/journal.pcbi.1007494</a>","chicago":"Tkadlec, Josef, Andreas Pavlogiannis, Krishnendu Chatterjee, and Martin A. Nowak. “Limits on Amplifiers of Natural Selection under Death-Birth Updating.” <i>PLoS Computational Biology</i>. Public Library of Science, 2020. <a href=\"https://doi.org/10.1371/journal.pcbi.1007494\">https://doi.org/10.1371/journal.pcbi.1007494</a>.","ista":"Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. 2020. Limits on amplifiers of natural selection under death-Birth updating. PLoS computational biology. 16, e1007494."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa":1,"language":[{"iso":"eng"}],"department":[{"_id":"KrCh"}],"article_number":"e1007494","file":[{"file_size":1817531,"date_created":"2020-02-03T07:32:42Z","creator":"dernst","date_updated":"2020-07-14T12:47:53Z","file_id":"7441","file_name":"2020_PlosCompBio_Tkadlec.pdf","access_level":"open_access","content_type":"application/pdf","relation":"main_file","checksum":"ce32ee2d2f53aed832f78bbd47e882df"}],"arxiv":1,"month":"01"},{"publisher":"ACM","doi":"10.1145/3363525","article_processing_charge":"No","type":"journal_article","date_updated":"2024-03-25T23:30:19Z","_id":"7158","ddc":["000"],"quality_controlled":"1","external_id":{"isi":["000564108400004"]},"related_material":{"record":[{"id":"8934","status":"public","relation":"dissertation_contains"}]},"isi":1,"year":"2019","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory","call_identifier":"FWF"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"publication":"ACM Transactions on Programming Languages and Systems","status":"public","date_published":"2019-11-01T00:00:00Z","ec_funded":1,"title":"Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth","oa_version":"Submitted Version","author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0003-1702-6584","first_name":"Amir Kafshdar","last_name":"Goharshady","full_name":"Goharshady, Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Prateesh","full_name":"Goyal, Prateesh","last_name":"Goyal"},{"orcid":"0000-0003-4783-0389","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen"},{"last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","first_name":"Andreas"}],"day":"01","scopus_import":"1","article_type":"original","date_created":"2019-12-09T08:33:33Z","volume":41,"abstract":[{"text":"Interprocedural analysis is at the heart of numerous applications in programming languages, such as alias analysis, constant propagation, and so on. Recursive state machines (RSMs) are standard models for interprocedural analysis. We consider a general framework with RSMs where the transitions are labeled from a semiring and path properties are algebraic with semiring operations. RSMs with algebraic path properties can model interprocedural dataflow analysis problems, the shortest path problem, the most probable path problem, and so on. The traditional algorithms for interprocedural analysis focus on path properties where the starting point is fixed as the entry point of a specific method. In this work, we consider possible multiple queries as required in many applications such as in alias analysis. The study of multiple queries allows us to bring in an important algorithmic distinction between the resource usage of the one-time preprocessing vs for each individual query. The second aspect we consider is that the control flow graphs for most programs have constant treewidth.\r\n\r\nOur main contributions are simple and implementable algorithms that support multiple queries for algebraic path properties for RSMs that have constant treewidth. Our theoretical results show that our algorithms have small additional one-time preprocessing but can answer subsequent queries significantly faster as compared to the current algorithmic solutions for interprocedural dataflow analysis. We have also implemented our algorithms and evaluated their performance for performing on-demand interprocedural dataflow analysis on various domains, such as for live variable analysis and reaching definitions, on a standard benchmark set. Our experimental results align with our theoretical statements and show that after a lightweight preprocessing, on-demand queries are answered much faster than the standard existing algorithmic approaches.\r\n","lang":"eng"}],"intvolume":"        41","has_accepted_license":"1","publication_status":"published","publication_identifier":{"issn":["0164-0925"]},"file_date_updated":"2020-10-08T12:58:10Z","month":"11","file":[{"date_created":"2020-10-08T12:58:10Z","file_size":667357,"creator":"dernst","date_updated":"2020-10-08T12:58:10Z","file_id":"8632","file_name":"2019_ACMTransactions_Chatterjee.pdf","success":1,"content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"291cc86a07bd010d4815e177dac57b70"}],"article_number":"23","department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"oa":1,"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","issue":"4","citation":{"ista":"Chatterjee K, Goharshady AK, Goyal P, Ibsen-Jensen R, Pavlogiannis A. 2019. Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth. ACM Transactions on Programming Languages and Systems. 41(4), 23.","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Prateesh Goyal, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Faster Algorithms for Dynamic Algebraic Queries in Basic RSMs with Constant Treewidth.” <i>ACM Transactions on Programming Languages and Systems</i>. ACM, 2019. <a href=\"https://doi.org/10.1145/3363525\">https://doi.org/10.1145/3363525</a>.","mla":"Chatterjee, Krishnendu, et al. “Faster Algorithms for Dynamic Algebraic Queries in Basic RSMs with Constant Treewidth.” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 41, no. 4, 23, ACM, 2019, doi:<a href=\"https://doi.org/10.1145/3363525\">10.1145/3363525</a>.","apa":"Chatterjee, K., Goharshady, A. K., Goyal, P., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2019). Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth. <i>ACM Transactions on Programming Languages and Systems</i>. ACM. <a href=\"https://doi.org/10.1145/3363525\">https://doi.org/10.1145/3363525</a>","ama":"Chatterjee K, Goharshady AK, Goyal P, Ibsen-Jensen R, Pavlogiannis A. Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth. <i>ACM Transactions on Programming Languages and Systems</i>. 2019;41(4). doi:<a href=\"https://doi.org/10.1145/3363525\">10.1145/3363525</a>","short":"K. Chatterjee, A.K. Goharshady, P. Goyal, R. Ibsen-Jensen, A. Pavlogiannis, ACM Transactions on Programming Languages and Systems 41 (2019).","ieee":"K. Chatterjee, A. K. Goharshady, P. Goyal, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth,” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 41, no. 4. ACM, 2019."}},{"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"ista":"Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. 2019. Population structure determines the tradeoff between fixation probability and fixation time. Communications Biology. 2, 138.","chicago":"Tkadlec, Josef, Andreas Pavlogiannis, Krishnendu Chatterjee, and Martin A. Nowak. “Population Structure Determines the Tradeoff between Fixation Probability and Fixation Time.” <i>Communications Biology</i>. Springer Nature, 2019. <a href=\"https://doi.org/10.1038/s42003-019-0373-y\">https://doi.org/10.1038/s42003-019-0373-y</a>.","mla":"Tkadlec, Josef, et al. “Population Structure Determines the Tradeoff between Fixation Probability and Fixation Time.” <i>Communications Biology</i>, vol. 2, 138, Springer Nature, 2019, doi:<a href=\"https://doi.org/10.1038/s42003-019-0373-y\">10.1038/s42003-019-0373-y</a>.","apa":"Tkadlec, J., Pavlogiannis, A., Chatterjee, K., &#38; Nowak, M. A. (2019). Population structure determines the tradeoff between fixation probability and fixation time. <i>Communications Biology</i>. Springer Nature. <a href=\"https://doi.org/10.1038/s42003-019-0373-y\">https://doi.org/10.1038/s42003-019-0373-y</a>","ama":"Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. Population structure determines the tradeoff between fixation probability and fixation time. <i>Communications Biology</i>. 2019;2. doi:<a href=\"https://doi.org/10.1038/s42003-019-0373-y\">10.1038/s42003-019-0373-y</a>","short":"J. Tkadlec, A. Pavlogiannis, K. Chatterjee, M.A. Nowak, Communications Biology 2 (2019).","ieee":"J. Tkadlec, A. Pavlogiannis, K. Chatterjee, and M. A. Nowak, “Population structure determines the tradeoff between fixation probability and fixation time,” <i>Communications Biology</i>, vol. 2. Springer Nature, 2019."},"language":[{"iso":"eng"}],"oa":1,"article_number":"138","file":[{"file_name":"2019_CommBio_Tkadlec.pdf","content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"d1a69bfe73767e4246f0a38e4e1554dd","date_created":"2019-12-23T13:39:30Z","file_size":1670274,"creator":"dernst","date_updated":"2020-07-14T12:47:53Z","file_id":"7211"}],"department":[{"_id":"KrCh"}],"month":"04","publication_status":"published","publication_identifier":{"issn":["2399-3642"]},"file_date_updated":"2020-07-14T12:47:53Z","abstract":[{"lang":"eng","text":"The rate of biological evolution depends on the fixation probability and on the fixation time of new mutants. Intensive research has focused on identifying population structures that augment the fixation probability of advantageous mutants. But these amplifiers of natural selection typically increase fixation time. Here we study population structures that achieve a tradeoff between fixation probability and time. First, we show that no amplifiers can have an asymptotically lower absorption time than the well-mixed population. Then we design population structures that substantially augment the fixation probability with just a minor increase in fixation time. Finally, we show that those structures enable higher effective rate of evolution than the well-mixed population provided that the rate of generating advantageous mutants is relatively low. Our work sheds light on how population structure affects the rate of evolution. Moreover, our structures could be useful for lab-based, medical, or industrial applications of evolutionary optimization."}],"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","image":"/images/cc_by.png","short":"CC BY (4.0)"},"intvolume":"         2","has_accepted_license":"1","article_type":"original","date_created":"2019-12-23T13:36:50Z","volume":2,"oa_version":"Published Version","title":"Population structure determines the tradeoff between fixation probability and fixation time","author":[{"orcid":"0000-0002-1097-9684","first_name":"Josef","full_name":"Tkadlec, Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","last_name":"Tkadlec"},{"full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","first_name":"Andreas"},{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"first_name":"Martin A.","last_name":"Nowak","full_name":"Nowak, Martin A."}],"day":"23","scopus_import":"1","date_published":"2019-04-23T00:00:00Z","pmid":1,"ec_funded":1,"project":[{"call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"}],"publication":"Communications Biology","status":"public","external_id":{"pmid":["31044163"],"isi":["000465425700006"]},"related_material":{"record":[{"id":"7196","relation":"part_of_dissertation","status":"public"}]},"year":"2019","isi":1,"quality_controlled":"1","ddc":["000"],"type":"journal_article","date_updated":"2023-09-07T13:19:22Z","_id":"7210","publisher":"Springer Nature","doi":"10.1038/s42003-019-0373-y","article_processing_charge":"No"},{"pubrep_id":"1056","language":[{"iso":"eng"}],"oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"short":"K. Chatterjee, A.K. Goharshady, N. Okati, A. Pavlogiannis, Proceedings of the ACM on Programming Languages 3 (2019).","ieee":"K. Chatterjee, A. K. Goharshady, N. Okati, and A. Pavlogiannis, “Efficient parameterized algorithms for data packing,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 3, no. POPL. ACM, 2019.","ama":"Chatterjee K, Goharshady AK, Okati N, Pavlogiannis A. Efficient parameterized algorithms for data packing. <i>Proceedings of the ACM on Programming Languages</i>. 2019;3(POPL). doi:<a href=\"https://doi.org/10.1145/3290366\">10.1145/3290366</a>","mla":"Chatterjee, Krishnendu, et al. “Efficient Parameterized Algorithms for Data Packing.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 3, no. POPL, 53, ACM, 2019, doi:<a href=\"https://doi.org/10.1145/3290366\">10.1145/3290366</a>.","apa":"Chatterjee, K., Goharshady, A. K., Okati, N., &#38; Pavlogiannis, A. (2019). Efficient parameterized algorithms for data packing. <i>Proceedings of the ACM on Programming Languages</i>. ACM. <a href=\"https://doi.org/10.1145/3290366\">https://doi.org/10.1145/3290366</a>","ista":"Chatterjee K, Goharshady AK, Okati N, Pavlogiannis A. 2019. Efficient parameterized algorithms for data packing. Proceedings of the ACM on Programming Languages. 3(POPL), 53.","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Nastaran Okati, and Andreas Pavlogiannis. “Efficient Parameterized Algorithms for Data Packing.” <i>Proceedings of the ACM on Programming Languages</i>. ACM, 2019. <a href=\"https://doi.org/10.1145/3290366\">https://doi.org/10.1145/3290366</a>."},"issue":"POPL","month":"01","article_number":"53","file":[{"content_type":"application/pdf","access_level":"open_access","file_name":"2019_ACM_POPL_Chatterjee.pdf","checksum":"c157752f96877b36685ad7063ada4524","relation":"main_file","date_updated":"2020-07-14T12:47:29Z","creator":"dernst","date_created":"2019-05-06T12:23:11Z","file_size":1294962,"file_id":"6381"}],"department":[{"_id":"KrCh"}],"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","image":"/images/cc_by.png","short":"CC BY (4.0)"},"abstract":[{"text":"There is a huge gap between the speeds of modern caches and main memories, and therefore cache misses account for a considerable loss of efficiency in programs. The predominant technique to address this issue has been Data Packing: data elements that are frequently accessed within time proximity are packed into the same cache block, thereby minimizing accesses to the main memory. We consider the algorithmic problem of Data Packing on a two-level memory system. Given a reference sequence R of accesses to data elements, the task is to partition the elements into cache blocks such that the number of cache misses on R is minimized. The problem is notoriously difficult: it is NP-hard even when the cache has size 1, and is hard to approximate for any cache size larger than 4. Therefore, all existing techniques for Data Packing are based on heuristics and lack theoretical guarantees. In this work, we present the first positive theoretical results for Data Packing, along with new and stronger negative results. We consider the problem under the lens of the underlying access hypergraphs, which are hypergraphs of affinities between the data elements, where the order of an access hypergraph corresponds to the size of the affinity group. We study the problem parameterized by the treewidth of access hypergraphs, which is a standard notion in graph theory to measure the closeness of a graph to a tree. Our main results are as follows: We show there is a number q* depending on the cache parameters such that (a) if the access hypergraph of order q* has constant treewidth, then there is a linear-time algorithm for Data Packing; (b)the Data Packing problem remains NP-hard even if the access hypergraph of order q*-1 has constant treewidth. Thus, we establish a fine-grained dichotomy depending on a single parameter, namely, the highest order among access hypegraphs that have constant treewidth; and establish the optimal value q* of this parameter. Finally, we present an experimental evaluation of a prototype implementation of our algorithm. Our results demonstrate that, in practice, access hypergraphs of many commonly-used algorithms have small treewidth. We compare our approach with several state-of-the-art heuristic-based algorithms and show that our algorithm leads to significantly fewer cache-misses. ","lang":"eng"}],"intvolume":"         3","has_accepted_license":"1","file_date_updated":"2020-07-14T12:47:29Z","publication_identifier":{"issn":["2475-1421"]},"publication_status":"published","title":"Efficient parameterized algorithms for data packing","oa_version":"Published Version","day":"01","author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"first_name":"Amir Kafshdar","orcid":"0000-0003-1702-6584","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87","full_name":"Goharshady, Amir Kafshdar"},{"first_name":"Nastaran","last_name":"Okati","full_name":"Okati, Nastaran"},{"orcid":"0000-0002-8943-0722","first_name":"Andreas","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas"}],"date_created":"2019-05-06T12:18:17Z","volume":3,"status":"public","publication":"Proceedings of the ACM on Programming Languages","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"}],"date_published":"2019-01-01T00:00:00Z","ec_funded":1,"related_material":{"record":[{"id":"8934","status":"public","relation":"dissertation_contains"}]},"year":"2019","ddc":["004"],"quality_controlled":"1","publisher":"ACM","doi":"10.1145/3290366","type":"journal_article","_id":"6380","date_updated":"2024-03-25T23:30:18Z"},{"status":"public","publication":"Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11407","name":"Game Theory"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"}],"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","date_published":"2019-10-10T00:00:00Z","conference":{"location":"Athens, Greece","end_date":"2019-10-25","start_date":"2019-10-23","name":"OOPSLA: Object-oriented Programming, Systems, Languages and Applications"},"year":"2019","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"10199"}]},"external_id":{"arxiv":["1909.00989"]},"keyword":["safety","risk","reliability and quality","software"],"ddc":["000"],"main_file_link":[{"url":"https://dl.acm.org/doi/10.1145/3360550","open_access":"1"}],"quality_controlled":"1","article_processing_charge":"No","doi":"10.1145/3360550","publisher":"ACM","_id":"10190","date_updated":"2025-07-14T09:10:15Z","type":"conference","oa":1,"language":[{"iso":"eng"}],"citation":{"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>","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.","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.","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>.","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.","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>.","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>"},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","arxiv":1,"month":"10","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"file":[{"content_type":"application/pdf","access_level":"open_access","file_name":"2019_ACM_Chatterjee.pdf","success":1,"checksum":"2149979c46964c4d117af06ccb6c0834","relation":"main_file","creator":"cchlebak","date_updated":"2021-11-12T11:41:56Z","date_created":"2021-11-12T11:41:56Z","file_size":570829,"file_id":"10278"}],"article_number":"124","has_accepted_license":"1","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."}],"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","image":"/images/cc_by.png","short":"CC BY (4.0)"},"intvolume":"         3","file_date_updated":"2021-11-12T11:41:56Z","publication_identifier":{"eissn":["2475-1421"]},"publication_status":"published","day":"10","author":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","orcid":"0000-0002-8943-0722"},{"first_name":"Viktor","orcid":"0000-0001-9036-063X","last_name":"Toman","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","full_name":"Toman, Viktor"}],"oa_version":"Published Version","title":"Value-centric dynamic partial order reduction","volume":3,"date_created":"2021-10-27T14:57:06Z"},{"language":[{"iso":"eng"}],"pubrep_id":"960","oa":1,"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, Alexander Kößler, and Ulrich Schmid. “Automated Competitive Analysis of Real Time Scheduling with Graph Games.” <i>Real-Time Systems</i>. Springer, 2018. <a href=\"https://doi.org/10.1007/s11241-017-9293-4\">https://doi.org/10.1007/s11241-017-9293-4</a>.","ista":"Chatterjee K, Pavlogiannis A, Kößler A, Schmid U. 2018. Automated competitive analysis of real time scheduling with graph games. Real-Time Systems. 54(1), 166–207.","mla":"Chatterjee, Krishnendu, et al. “Automated Competitive Analysis of Real Time Scheduling with Graph Games.” <i>Real-Time Systems</i>, vol. 54, no. 1, Springer, 2018, pp. 166–207, doi:<a href=\"https://doi.org/10.1007/s11241-017-9293-4\">10.1007/s11241-017-9293-4</a>.","apa":"Chatterjee, K., Pavlogiannis, A., Kößler, A., &#38; Schmid, U. (2018). Automated competitive analysis of real time scheduling with graph games. <i>Real-Time Systems</i>. Springer. <a href=\"https://doi.org/10.1007/s11241-017-9293-4\">https://doi.org/10.1007/s11241-017-9293-4</a>","ama":"Chatterjee K, Pavlogiannis A, Kößler A, Schmid U. Automated competitive analysis of real time scheduling with graph games. <i>Real-Time Systems</i>. 2018;54(1):166-207. doi:<a href=\"https://doi.org/10.1007/s11241-017-9293-4\">10.1007/s11241-017-9293-4</a>","short":"K. Chatterjee, A. Pavlogiannis, A. Kößler, U. Schmid, Real-Time Systems 54 (2018) 166–207.","ieee":"K. Chatterjee, A. Pavlogiannis, A. Kößler, and U. Schmid, “Automated competitive analysis of real time scheduling with graph games,” <i>Real-Time Systems</i>, vol. 54, no. 1. Springer, pp. 166–207, 2018."},"issue":"1","month":"01","file":[{"creator":"system","date_updated":"2020-07-14T12:47:56Z","date_created":"2018-12-12T10:17:14Z","file_size":1163507,"file_id":"5267","access_level":"open_access","content_type":"application/pdf","file_name":"IST-2018-960-v1+1_2017_Chatterjee_Automated_competetive.pdf","checksum":"c2590ef160709d8054cf29ee173f1454","relation":"main_file"}],"department":[{"_id":"KrCh"}],"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","image":"/images/cc_by.png","short":"CC BY (4.0)"},"intvolume":"        54","abstract":[{"lang":"eng","text":"This paper is devoted to automatic competitive analysis of real-time scheduling algorithms for firm-deadline tasksets, where only completed tasks con- tribute some utility to the system. Given such a taskset T , the competitive ratio of an on-line scheduling algorithm A for T is the worst-case utility ratio of A over the utility achieved by a clairvoyant algorithm. We leverage the theory of quantitative graph games to address the competitive analysis and competitive synthesis problems. For the competitive analysis case, given any taskset T and any finite-memory on- line scheduling algorithm A , we show that the competitive ratio of A in T can be computed in polynomial time in the size of the state space of A . Our approach is flexible as it also provides ways to model meaningful constraints on the released task sequences that determine the competitive ratio. We provide an experimental study of many well-known on-line scheduling algorithms, which demonstrates the feasibility of our competitive analysis approach that effectively replaces human ingenuity (required Preliminary versions of this paper have appeared in Chatterjee et al. ( 2013 , 2014 ). B Andreas Pavlogiannis pavlogiannis@ist.ac.at Krishnendu Chatterjee krish.chat@ist.ac.at Alexander Kößler koe@ecs.tuwien.ac.at Ulrich Schmid s@ecs.tuwien.ac.at 1 IST Austria (Institute of Science and Technology Austria), Am Campus 1, 3400 Klosterneuburg, Austria 2 Embedded Computing Systems Group, Vienna University of Technology, Treitlstrasse 3, 1040 Vienna, Austria 123 Real-Time Syst for finding worst-case scenarios) by computing power. For the competitive synthesis case, we are just given a taskset T , and the goal is to automatically synthesize an opti- mal on-line scheduling algorithm A , i.e., one that guarantees the largest competitive ratio possible for T . We show how the competitive synthesis problem can be reduced to a two-player graph game with partial information, and establish that the compu- tational complexity of solving this game is Np -complete. The competitive synthesis problem is hence in Np in the size of the state space of the non-deterministic labeled transition system encoding the taskset. Overall, the proposed framework assists in the selection of suitable scheduling algorithms for a given taskset, which is in fact the most common situation in real-time systems design. "}],"has_accepted_license":"1","file_date_updated":"2020-07-14T12:47:56Z","publication_status":"published","title":"Automated competitive analysis of real time scheduling with graph games","oa_version":"Published Version","day":"01","scopus_import":"1","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","first_name":"Andreas"},{"full_name":"Kößler, Alexander","last_name":"Kößler","first_name":"Alexander"},{"last_name":"Schmid","full_name":"Schmid, Ulrich","first_name":"Ulrich"}],"date_created":"2018-12-11T11:48:14Z","volume":54,"status":"public","publication":"Real-Time Systems","project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407","call_identifier":"FWF"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"date_published":"2018-01-01T00:00:00Z","ec_funded":1,"related_material":{"record":[{"id":"2820","relation":"earlier_version","status":"public"}]},"external_id":{"isi":["000419955500006"]},"isi":1,"year":"2018","publist_id":"6929","ddc":["000"],"page":"166 - 207","quality_controlled":"1","publisher":"Springer","article_processing_charge":"No","doi":"10.1007/s11241-017-9293-4","type":"journal_article","_id":"738","date_updated":"2023-09-27T12:52:38Z"},{"publication_identifier":{"issn":["2399-3642"]},"publication_status":"published","file_date_updated":"2020-07-14T12:47:10Z","has_accepted_license":"1","intvolume":"         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","image":"/images/cc_by.png","short":"CC BY (4.0)"},"abstract":[{"lang":"eng","text":"Because of the intrinsic randomness of the evolutionary process, a mutant with a fitness advantage has some chance to be selected but no certainty. Any experiment that searches for advantageous mutants will lose many of them due to random drift. It is therefore of great interest to find population structures that improve the odds of advantageous mutants. Such structures are called amplifiers of natural selection: they increase the probability that advantageous mutants are selected. Arbitrarily strong amplifiers guarantee the selection of advantageous mutants, even for very small fitness advantage. Despite intensive research over the past decade, arbitrarily strong amplifiers have remained rare. Here we show how to construct a large variety of them. Our amplifiers are so simple that they could be useful in biotechnology, when optimizing biological molecules, or as a diagnostic tool, when searching for faster dividing cells or viruses. They could also occur in natural population structures."}],"volume":1,"date_created":"2018-12-18T13:22:58Z","author":[{"last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","first_name":"Andreas"},{"last_name":"Tkadlec","full_name":"Tkadlec, Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-1097-9684","first_name":"Josef"},{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"last_name":"Nowak","full_name":"Nowak, Martin A.","first_name":"Martin A."}],"scopus_import":"1","day":"14","oa_version":"Published Version","title":"Construction of arbitrarily strong amplifiers of natural selection using evolutionary graph theory","issue":"1","citation":{"chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin A. Nowak. “Construction of Arbitrarily Strong Amplifiers of Natural Selection Using Evolutionary Graph Theory.” <i>Communications Biology</i>. Springer Nature, 2018. <a href=\"https://doi.org/10.1038/s42003-018-0078-7\">https://doi.org/10.1038/s42003-018-0078-7</a>.","ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak MA. 2018. Construction of arbitrarily strong amplifiers of natural selection using evolutionary graph theory. Communications Biology. 1(1), 71.","apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., &#38; Nowak, M. A. (2018). Construction of arbitrarily strong amplifiers of natural selection using evolutionary graph theory. <i>Communications Biology</i>. Springer Nature. <a href=\"https://doi.org/10.1038/s42003-018-0078-7\">https://doi.org/10.1038/s42003-018-0078-7</a>","mla":"Pavlogiannis, Andreas, et al. “Construction of Arbitrarily Strong Amplifiers of Natural Selection Using Evolutionary Graph Theory.” <i>Communications Biology</i>, vol. 1, no. 1, 71, Springer Nature, 2018, doi:<a href=\"https://doi.org/10.1038/s42003-018-0078-7\">10.1038/s42003-018-0078-7</a>.","ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak MA. Construction of arbitrarily strong amplifiers of natural selection using evolutionary graph theory. <i>Communications Biology</i>. 2018;1(1). doi:<a href=\"https://doi.org/10.1038/s42003-018-0078-7\">10.1038/s42003-018-0078-7</a>","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. A. Nowak, “Construction of arbitrarily strong amplifiers of natural selection using evolutionary graph theory,” <i>Communications Biology</i>, vol. 1, no. 1. Springer Nature, 2018.","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M.A. Nowak, Communications Biology 1 (2018)."},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","oa":1,"pubrep_id":"1045","language":[{"iso":"eng"}],"department":[{"_id":"KrCh"}],"article_number":"71","file":[{"access_level":"open_access","content_type":"application/pdf","file_name":"2018_CommBiology_Pavlogiannis.pdf","checksum":"a9db825fa3b64a51ff3de035ec973b3e","relation":"main_file","date_updated":"2020-07-14T12:47:10Z","creator":"dernst","file_size":1804194,"date_created":"2018-12-18T13:37:04Z","file_id":"5752"}],"month":"06","quality_controlled":"1","ddc":["004","519","576"],"date_updated":"2024-02-21T13:48:42Z","_id":"5751","type":"journal_article","doi":"10.1038/s42003-018-0078-7","article_processing_charge":"No","publisher":"Springer Nature","ec_funded":1,"date_published":"2018-06-14T00:00:00Z","project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"}],"publication":"Communications Biology","status":"public","isi":1,"year":"2018","external_id":{"isi":["000461126500071"]},"related_material":{"record":[{"relation":"part_of_dissertation","status":"public","id":"7196"},{"status":"public","relation":"popular_science","id":"5559"}]}},{"oa_version":"Preprint","title":"Algorithms for algebraic path properties in concurrent systems of constant treewidth components","author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"orcid":"0000-0003-4783-0389","first_name":"Rasmus","last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0003-1702-6584","first_name":"Amir Kafshdar","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87","full_name":"Goharshady, Amir Kafshdar"},{"first_name":"Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis"}],"day":"01","scopus_import":"1","date_created":"2019-02-14T14:31:52Z","volume":40,"abstract":[{"lang":"eng","text":"We study algorithmic questions wrt algebraic path properties in concurrent systems, where the transitions of the system are labeled from a complete, closed semiring. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural problems that arise in program analysis. We consider that each component of the concurrent system is a graph with constant treewidth, a property satisfied by the controlflow graphs of most programs. We allow for multiple possible queries, which arise naturally in demand driven dataflow analysis. The study of multiple queries allows us to consider the tradeoff between the resource usage of the one-time preprocessing and for each individual query. The traditional approach constructs the product graph of all components and applies the best-known graph algorithm on the product. In this approach, even the answer to a single query requires the transitive closure (i.e., the results of all possible queries), which provides no room for tradeoff between preprocessing and query time.\r\nOur main contributions are algorithms that significantly improve the worst-case running time of the traditional approach, and provide various tradeoffs depending on the number of queries. For example, in a concurrent system of two components, the traditional approach requires hexic time in the worst case for answering one query as well as computing the transitive closure, whereas we show that with one-time preprocessing in almost cubic time, each subsequent query can be answered in at most linear time, and even the transitive closure can be computed in almost quartic time. Furthermore, we establish conditional optimality results showing that the worst-case running time of our algorithms cannot be improved without achieving major breakthroughs in graph algorithms (i.e., improving the worst-case bound for the shortest path problem in general graphs). Preliminary experimental results show that our algorithms perform favorably on several benchmarks.\r\n"}],"intvolume":"        40","publication_status":"published","publication_identifier":{"issn":["0164-0925"]},"month":"08","arxiv":1,"article_number":"9","department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"oa":1,"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","issue":"3","citation":{"short":"K. Chatterjee, R. Ibsen-Jensen, A.K. Goharshady, A. Pavlogiannis, ACM Transactions on Programming Languages and Systems 40 (2018).","ieee":"K. Chatterjee, R. Ibsen-Jensen, A. K. Goharshady, and A. Pavlogiannis, “Algorithms for algebraic path properties in concurrent systems of constant treewidth components,” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 40, no. 3. Association for Computing Machinery (ACM), 2018.","ama":"Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. Algorithms for algebraic path properties in concurrent systems of constant treewidth components. <i>ACM Transactions on Programming Languages and Systems</i>. 2018;40(3). doi:<a href=\"https://doi.org/10.1145/3210257\">10.1145/3210257</a>","mla":"Chatterjee, Krishnendu, et al. “Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components.” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 40, no. 3, 9, Association for Computing Machinery (ACM), 2018, doi:<a href=\"https://doi.org/10.1145/3210257\">10.1145/3210257</a>.","apa":"Chatterjee, K., Ibsen-Jensen, R., Goharshady, A. K., &#38; Pavlogiannis, A. (2018). Algorithms for algebraic path properties in concurrent systems of constant treewidth components. <i>ACM Transactions on Programming Languages and Systems</i>. Association for Computing Machinery (ACM). <a href=\"https://doi.org/10.1145/3210257\">https://doi.org/10.1145/3210257</a>","ista":"Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. 2018. Algorithms for algebraic path properties in concurrent systems of constant treewidth components. ACM Transactions on Programming Languages and Systems. 40(3), 9.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Amir Kafshdar Goharshady, and Andreas Pavlogiannis. “Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components.” <i>ACM Transactions on Programming Languages and Systems</i>. Association for Computing Machinery (ACM), 2018. <a href=\"https://doi.org/10.1145/3210257\">https://doi.org/10.1145/3210257</a>."},"publisher":"Association for Computing Machinery (ACM)","doi":"10.1145/3210257","article_processing_charge":"No","type":"journal_article","date_updated":"2024-03-25T23:30:19Z","_id":"6009","quality_controlled":"1","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1510.07565"}],"external_id":{"isi":["000444694800001"],"arxiv":["1510.07565"]},"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"1437"},{"relation":"earlier_version","status":"public","id":"5441"},{"id":"5442","relation":"earlier_version","status":"public"},{"id":"8934","relation":"dissertation_contains","status":"public"}]},"year":"2018","isi":1,"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"}],"publication":"ACM Transactions on Programming Languages and Systems","status":"public","date_published":"2018-08-01T00:00:00Z","ec_funded":1},{"publist_id":"6828","year":"2017","related_material":{"record":[{"status":"public","relation":"part_of_dissertation","id":"1071"},{"status":"public","relation":"part_of_dissertation","id":"1437"},{"id":"1602","status":"public","relation":"part_of_dissertation"},{"id":"1604","relation":"part_of_dissertation","status":"public"},{"relation":"part_of_dissertation","status":"public","id":"1607"},{"id":"1714","status":"public","relation":"part_of_dissertation"}]},"ec_funded":1,"date_published":"2017-08-09T00:00:00Z","acknowledgement":"First, I am thankful to my advisor, Krishnendu Chatterjee, for offering me the opportunity to\r\nmaterialize my scientific curiosity in a remarkably wide range of interesting topics, as well as for his constant availability and continuous support throughout my doctoral studies. I have had the privilege of collaborating with, discussing and getting inspired by all members of my committee: Thomas A. Henzinger, Ulrich Schmid and Martin A. Nowak. The role of the above four people has been very instrumental both to the research carried out for this dissertation, and to the researcher I evolved to in the process.\r\nI have greatly enjoyed my numerous brainstorming sessions with Rasmus Ibsen-Jensen, many\r\nof which led to results on low-treewidth graphs presented here.  I thank Alex Kößler for our\r\ndiscussions on modeling and analyzing real-time scheduling algorithms, Yaron Velner for our\r\ncollaboration on the Quantitative Interprocedural Analysis framework, and Nishant Sinha for our initial discussions on partial order reduction techniques in stateless model checking. I also thank Jan Otop, Ben Adlam, Bernhard Kragl and Josef Tkadlec for our fruitful collaborations on\r\ntopics outside the scope of this dissertation, as well as the interns Prateesh Goyal, Amir Kafshdar Goharshady, Samarth Mishra, Bhavya Choudhary and Marek Chalupa, with whom I have shared my excitement on various research topics. Together with my collaborators, I thank officemates and members of the Chatterjee and Henzinger groups throughout the years, Thorsten Tarrach, Ventsi Chonev, Roopsha Samanta, Przemek Daca, Mirco Giacobbe, Tanja Petrov, Ashutosh\r\nGupta,  Arjun Radhakrishna,  Petr Novontý,  Christian Hilbe,  Jakob Ruess,  Martin Chmelik,\r\nCezara Dragoi, Johannes Reiter, Andrey Kupriyanov, Guy Avni, Sasha Rubin, Jessica Davies, Hongfei Fu, Thomas Ferrère, Pavol Cerný, Ali Sezgin, Jan Kretínský, Sergiy Bogomolov, Hui\r\nKong, Benjamin Aminof, Duc-Hiep Chu, and Damien Zufferey.  Besides collaborations and office spaces, with many of the above people I have been fortunate to share numerous whiteboard\r\ndiscussions, as well as memorable long walks and amicable meals accompanied by stimulating\r\nconversations. I am highly indebted to Elisabeth Hacker for her continuous assistance in matters\r\nthat often exceeded her official duties, and who made my integration in Austria a smooth process.","degree_awarded":"PhD","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"}],"status":"public","date_updated":"2023-09-07T12:01:59Z","_id":"821","type":"dissertation","doi":"10.15479/AT:ISTA:th_854","alternative_title":["ISTA Thesis"],"article_processing_charge":"No","publisher":"Institute of Science and Technology Austria","page":"418","ddc":["000"],"department":[{"_id":"KrCh"}],"file":[{"date_updated":"2020-07-14T12:48:10Z","creator":"system","date_created":"2018-12-12T10:11:44Z","file_size":4103115,"file_id":"4900","access_level":"open_access","content_type":"application/pdf","file_name":"IST-2017-854-v1+1_Pavlogiannis_Thesis_PubRep.pdf","checksum":"3a3ec003f6ee73f41f82a544d63dfc77","relation":"main_file"},{"relation":"source_file","checksum":"bd2facc45ff8a2e20c5ed313c2ccaa83","file_name":"2017_thesis_Pavlogiannis.zip","content_type":"application/zip","access_level":"closed","file_id":"6201","date_created":"2019-04-05T07:59:31Z","file_size":14744374,"date_updated":"2020-07-14T12:48:10Z","creator":"dernst"}],"supervisor":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"}],"month":"08","citation":{"apa":"Pavlogiannis, A. (2017). <i>Algorithmic advances in program analysis and their applications</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:th_854\">https://doi.org/10.15479/AT:ISTA:th_854</a>","mla":"Pavlogiannis, Andreas. <i>Algorithmic Advances in Program Analysis and Their Applications</i>. Institute of Science and Technology Austria, 2017, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:th_854\">10.15479/AT:ISTA:th_854</a>.","chicago":"Pavlogiannis, Andreas. “Algorithmic Advances in Program Analysis and Their Applications.” Institute of Science and Technology Austria, 2017. <a href=\"https://doi.org/10.15479/AT:ISTA:th_854\">https://doi.org/10.15479/AT:ISTA:th_854</a>.","ista":"Pavlogiannis A. 2017. Algorithmic advances in program analysis and their applications. Institute of Science and Technology Austria.","ieee":"A. Pavlogiannis, “Algorithmic advances in program analysis and their applications,” Institute of Science and Technology Austria, 2017.","short":"A. Pavlogiannis, Algorithmic Advances in Program Analysis and Their Applications, Institute of Science and Technology Austria, 2017.","ama":"Pavlogiannis A. Algorithmic advances in program analysis and their applications. 2017. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:th_854\">10.15479/AT:ISTA:th_854</a>"},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","oa":1,"language":[{"iso":"eng"}],"pubrep_id":"854","date_created":"2018-12-11T11:48:41Z","author":[{"orcid":"0000-0002-8943-0722","first_name":"Andreas","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis"}],"day":"09","title":"Algorithmic advances in program analysis and their applications","oa_version":"Published Version","publication_identifier":{"issn":["2663-337X"]},"publication_status":"published","file_date_updated":"2020-07-14T12:48:10Z","has_accepted_license":"1","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","image":"/image/cc_by_nd.png","short":"CC BY-ND (4.0)"},"license":"https://creativecommons.org/licenses/by-nd/4.0/","abstract":[{"text":"This dissertation focuses on algorithmic aspects of program verification, and presents modeling and complexity advances on several problems related to the\r\nstatic analysis of programs, the stateless model checking of concurrent programs, and the competitive analysis of real-time scheduling algorithms.\r\nOur contributions can be broadly grouped into five categories.\r\n\r\nOur first contribution is a set of new algorithms and data structures for the quantitative and data-flow analysis of programs, based on the graph-theoretic notion of treewidth.\r\nIt has been observed that the control-flow graphs of typical programs have special structure, and are characterized as graphs of small treewidth.\r\nWe utilize this structural property to provide faster algorithms for the quantitative and data-flow analysis of recursive and concurrent programs.\r\nIn most cases we make an algebraic treatment of the considered problem,\r\nwhere several interesting analyses, such as the reachability, shortest path, and certain kind of data-flow analysis problems follow as special cases. \r\nWe exploit the constant-treewidth property to obtain algorithmic improvements for on-demand versions of the problems, \r\nand provide data structures with various tradeoffs between the resources spent in the preprocessing and querying phase.\r\nWe also improve on the algorithmic complexity of quantitative problems outside the algebraic path framework,\r\nnamely of the minimum mean-payoff, minimum ratio, and minimum initial credit for energy problems.\r\n\r\n\r\nOur second contribution is a set of algorithms for Dyck reachability with applications to data-dependence analysis and alias analysis.\r\nIn particular, we develop an optimal algorithm for Dyck reachability on bidirected graphs, which are ubiquitous in context-insensitive, field-sensitive points-to analysis.\r\nAdditionally, we develop an efficient algorithm for context-sensitive data-dependence analysis via Dyck reachability,\r\nwhere the task is to obtain analysis summaries of library code in the presence of callbacks.\r\nOur algorithm preprocesses libraries in almost linear time, after which the contribution of the library in the complexity of the client analysis is (i)~linear in the number of call sites and (ii)~only logarithmic in the size of the whole library, as opposed to linear in the size of the whole library.\r\nFinally, we prove that Dyck reachability is Boolean Matrix Multiplication-hard in general, and the hardness also holds for graphs of constant treewidth.\r\nThis hardness result strongly indicates that there exist no combinatorial algorithms for Dyck reachability with truly subcubic complexity.\r\n\r\n\r\nOur third contribution is the formalization and algorithmic treatment of the Quantitative Interprocedural Analysis framework.\r\nIn this framework, the transitions of a recursive program are annotated as good, bad or neutral, and receive a weight which measures\r\nthe magnitude of their respective effect.\r\nThe Quantitative Interprocedural Analysis problem asks to determine whether there exists an infinite run of the program where the long-run ratio of the bad weights over the good weights is above a given threshold.\r\nWe illustrate how several quantitative problems related to static analysis of recursive programs can be instantiated in this framework,\r\nand present some case studies to this direction.\r\n\r\n\r\nOur fourth contribution is a new dynamic partial-order reduction for the stateless model checking of concurrent programs. Traditional approaches rely on the standard Mazurkiewicz equivalence between  traces, by means of partitioning the trace space into equivalence classes, and attempting to explore a few representatives from each class.\r\nWe present a new dynamic partial-order reduction method  called the Data-centric Partial Order Reduction (DC-DPOR).\r\nOur algorithm is based on a new equivalence between traces, called the observation equivalence.\r\nDC-DPOR explores a coarser partitioning of the trace space than any exploration method based on the standard Mazurkiewicz equivalence.\r\nDepending on the program, the new partitioning can be even exponentially coarser.\r\nAdditionally, DC-DPOR spends only polynomial time in each explored class.\r\n\r\n\r\nOur fifth contribution is the use of automata and game-theoretic verification techniques in the competitive analysis and synthesis of real-time scheduling algorithms for firm-deadline tasks.\r\nOn the analysis side, we leverage automata on infinite words to compute the competitive ratio of real-time schedulers subject to various environmental constraints.\r\nOn the synthesis side, we introduce a new instance of two-player mean-payoff partial-information games, and show\r\nhow the synthesis of an optimal real-time scheduler can be reduced to computing winning strategies in this new type of games.","lang":"eng"}]},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Pavlogiannis, Andreas, et al. “Amplification on Undirected Population Structures: Comets Beat Stars.” <i>Scientific Reports</i>, vol. 7, no. 1, 82, Nature Publishing Group, 2017, doi:<a href=\"https://doi.org/10.1038/s41598-017-00107-w\">10.1038/s41598-017-00107-w</a>.","apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., &#38; Nowak, M. (2017). Amplification on undirected population structures: Comets beat stars. <i>Scientific Reports</i>. Nature Publishing Group. <a href=\"https://doi.org/10.1038/s41598-017-00107-w\">https://doi.org/10.1038/s41598-017-00107-w</a>","chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. “Amplification on Undirected Population Structures: Comets Beat Stars.” <i>Scientific Reports</i>. Nature Publishing Group, 2017. <a href=\"https://doi.org/10.1038/s41598-017-00107-w\">https://doi.org/10.1038/s41598-017-00107-w</a>.","ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2017. Amplification on undirected population structures: Comets beat stars. Scientific Reports. 7(1), 82.","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Scientific Reports 7 (2017).","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, “Amplification on undirected population structures: Comets beat stars,” <i>Scientific Reports</i>, vol. 7, no. 1. Nature Publishing Group, 2017.","ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. Amplification on undirected population structures: Comets beat stars. <i>Scientific Reports</i>. 2017;7(1). doi:<a href=\"https://doi.org/10.1038/s41598-017-00107-w\">10.1038/s41598-017-00107-w</a>"},"issue":"1","pubrep_id":"938","language":[{"iso":"eng"}],"oa":1,"file":[{"checksum":"7d05cbdd914e194a019c0f91fb64e9a8","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_name":"IST-2018-938-v1+1_2017_Pavlogiannis_Amplification_on.pdf","file_id":"5357","date_updated":"2020-07-14T12:46:36Z","creator":"system","date_created":"2018-12-12T10:18:35Z","file_size":1536783}],"article_number":"82","department":[{"_id":"KrCh"}],"month":"03","file_date_updated":"2020-07-14T12:46:36Z","publication_status":"published","publication_identifier":{"issn":["20452322"]},"intvolume":"         7","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","image":"/images/cc_by.png","short":"CC BY (4.0)"},"abstract":[{"lang":"eng","text":"The fixation probability is the probability that a new mutant introduced in a homogeneous population eventually takes over the entire population. The fixation probability is a fundamental quantity of natural selection, and known to depend on the population structure. Amplifiers of natural selection are population structures which increase the fixation probability of advantageous mutants, as compared to the baseline case of well-mixed populations. In this work we focus on symmetric population structures represented as undirected graphs. In the regime of undirected graphs, the strongest amplifier known has been the Star graph, and the existence of undirected graphs with stronger amplification properties has remained open for over a decade. In this work we present the Comet and Comet-swarm families of undirected graphs. We show that for a range of fitness values of the mutants, the Comet and Cometswarm graphs have fixation probability strictly larger than the fixation probability of the Star graph, for fixed population size and at the limit of large populations, respectively. "}],"has_accepted_license":"1","date_created":"2018-12-11T11:46:53Z","volume":7,"title":"Amplification on undirected population structures: Comets beat stars","oa_version":"Published Version","scopus_import":1,"day":"06","author":[{"first_name":"Andreas","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis"},{"last_name":"Tkadlec","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","full_name":"Tkadlec, Josef","first_name":"Josef","orcid":"0000-0002-1097-9684"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"full_name":"Nowak, Martin","last_name":"Nowak","first_name":"Martin"}],"date_published":"2017-03-06T00:00:00Z","ec_funded":1,"status":"public","publication":"Scientific Reports","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"publist_id":"7307","related_material":{"record":[{"id":"5449","status":"public","relation":"earlier_version"}]},"year":"2017","quality_controlled":"1","ddc":["004"],"type":"journal_article","_id":"512","date_updated":"2023-02-23T12:26:57Z","publisher":"Nature Publishing Group","article_processing_charge":"No","doi":"10.1038/s41598-017-00107-w"}]