[{"ddc":["005"],"acknowledgement":"The research was partially supported by an IBM PhD fellowship, a Facebook PhD fellowship, and DOC fellowship #24956 of the Austrian Academy of Sciences (OeAW).","abstract":[{"text":"In this thesis, we consider several of the most classical and fundamental problems in static analysis and formal verification, including invariant generation, reachability analysis, termination analysis of probabilistic programs, data-flow analysis, quantitative analysis of Markov chains and Markov decision processes, and the problem of data packing in cache management.\r\nWe use techniques from parameterized complexity theory, polyhedral geometry, and real algebraic geometry to significantly improve the state-of-the-art, in terms of both scalability and completeness guarantees, for the mentioned problems. In some cases, our results are the first theoretical improvements for the respective problems in two or three decades.","lang":"eng"}],"day":"01","doi":"10.15479/AT:ISTA:8934","degree_awarded":"PhD","year":"2021","citation":{"mla":"Goharshady, Amir Kafshdar. <i>Parameterized and Algebro-Geometric Advances in Static Program Analysis</i>. Institute of Science and Technology Austria, 2021, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:8934\">10.15479/AT:ISTA:8934</a>.","short":"A.K. Goharshady, Parameterized and Algebro-Geometric Advances in Static Program Analysis, Institute of Science and Technology Austria, 2021.","ista":"Goharshady AK. 2021. Parameterized and algebro-geometric advances in static program analysis. Institute of Science and Technology Austria.","ama":"Goharshady AK. Parameterized and algebro-geometric advances in static program analysis. 2021. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:8934\">10.15479/AT:ISTA:8934</a>","apa":"Goharshady, A. K. (2021). <i>Parameterized and algebro-geometric advances in static program analysis</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:8934\">https://doi.org/10.15479/AT:ISTA:8934</a>","chicago":"Goharshady, Amir Kafshdar. “Parameterized and Algebro-Geometric Advances in Static Program Analysis.” Institute of Science and Technology Austria, 2021. <a href=\"https://doi.org/10.15479/AT:ISTA:8934\">https://doi.org/10.15479/AT:ISTA:8934</a>.","ieee":"A. K. Goharshady, “Parameterized and algebro-geometric advances in static program analysis,” Institute of Science and Technology Austria, 2021."},"date_updated":"2025-06-02T08:53:47Z","publisher":"Institute of Science and Technology Austria","file_date_updated":"2021-12-23T23:30:04Z","page":"278","title":"Parameterized and algebro-geometric advances in static program analysis","alternative_title":["ISTA Thesis"],"article_processing_charge":"No","date_created":"2020-12-10T12:17:07Z","department":[{"_id":"KrCh"},{"_id":"GradSch"}],"publication_status":"published","author":[{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir Kafshdar","last_name":"Goharshady","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar"}],"_id":"8934","related_material":{"record":[{"status":"public","relation":"part_of_dissertation","id":"1386"},{"id":"1437","relation":"part_of_dissertation","status":"public"},{"relation":"part_of_dissertation","id":"639","status":"public"},{"relation":"part_of_dissertation","id":"6918","status":"public"},{"relation":"part_of_dissertation","id":"6490","status":"public"},{"status":"public","id":"7158","relation":"part_of_dissertation"},{"id":"6009","relation":"part_of_dissertation","status":"public"},{"status":"public","id":"949","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","id":"311","status":"public"},{"status":"public","relation":"part_of_dissertation","id":"7810"},{"id":"8089","relation":"part_of_dissertation","status":"public"},{"status":"public","id":"8728","relation":"part_of_dissertation"},{"status":"public","relation":"part_of_dissertation","id":"5977"},{"id":"6056","relation":"part_of_dissertation","status":"public"},{"status":"public","id":"6175","relation":"part_of_dissertation"},{"status":"public","relation":"part_of_dissertation","id":"6340"},{"status":"public","relation":"part_of_dissertation","id":"6378"},{"id":"6380","relation":"part_of_dissertation","status":"public"},{"id":"66","relation":"part_of_dissertation","status":"public"},{"status":"public","id":"6780","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","id":"7014","status":"public"}]},"status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","file":[{"access_level":"open_access","relation":"main_file","creator":"akafshda","file_id":"8969","file_size":5251507,"checksum":"d1b9db3725aed34dadd81274aeb9426c","date_created":"2020-12-22T20:08:44Z","embargo":"2021-12-22","file_name":"Thesis-pdfa.pdf","content_type":"application/pdf","date_updated":"2021-12-23T23:30:04Z"},{"date_created":"2020-12-22T20:08:50Z","embargo_to":"open_access","checksum":"1661df7b393e6866d2460eba3c905130","file_size":10636756,"date_updated":"2021-03-04T23:30:04Z","file_name":"source.zip","content_type":"application/zip","relation":"source_file","access_level":"closed","file_id":"8970","creator":"akafshda"}],"oa":1,"supervisor":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"}],"publication_identifier":{"issn":["2663-337X"]},"type":"dissertation","date_published":"2021-01-01T00:00:00Z","tmp":{"legal_code_url":"https://creativecommons.org/publicdomain/zero/1.0/legalcode","short":"CC0 (1.0)","name":"Creative Commons Public Domain Dedication (CC0 1.0)","image":"/images/cc_0.png"},"language":[{"iso":"eng"}],"month":"01","project":[{"name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies","_id":"267066CE-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts","_id":"266EEEC0-B435-11E9-9278-68D0E5697425"}],"oa_version":"Published Version","has_accepted_license":"1"},{"oa":1,"publication_identifier":{"issn":["03029743"],"eissn":["16113349"],"isbn":["9783030449131"]},"date_published":"2020-04-18T00:00:00Z","type":"conference","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"status":"public","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"8934"}]},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","file":[{"access_level":"open_access","relation":"main_file","creator":"dernst","file_id":"7895","checksum":"8618b80f4cf7b39a60e61a6445ad9807","file_size":651250,"date_created":"2020-05-26T13:34:48Z","file_name":"2020_LNCS_Chatterjee.pdf","content_type":"application/pdf","date_updated":"2020-07-14T12:48:03Z"}],"month":"04","oa_version":"Published Version","project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_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"}],"publication":"European Symposium on Programming","has_accepted_license":"1","conference":{"location":"Dublin, Ireland","end_date":"2020-04-30","start_date":"2020-04-25","name":"ESOP: Programming Languages and Systems"},"language":[{"iso":"eng"}],"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"}],"doi":"10.1007/978-3-030-44914-8_5","day":"18","isi":1,"external_id":{"isi":["000681656800005"]},"date_updated":"2025-06-02T08:53:42Z","year":"2020","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.","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>.","short":"K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, A. Pavlogiannis, in:, European Symposium on Programming, Springer Nature, 2020, pp. 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>.","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.","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>","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>"},"ddc":["000"],"volume":12075,"title":"Optimal and perfectly parallel algorithms for on-demand data-flow analysis","alternative_title":["LNCS"],"intvolume":"     12075","publication_status":"published","date_created":"2020-05-10T22:00:50Z","article_processing_charge":"No","department":[{"_id":"KrCh"}],"author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Goharshady","first_name":"Amir Kafshdar","full_name":"Goharshady, Amir Kafshdar","orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Ibsen-Jensen","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Andreas","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"_id":"7810","scopus_import":"1","publisher":"Springer Nature","file_date_updated":"2020-07-14T12:48:03Z","page":"112-140","quality_controlled":"1"},{"author":[{"first_name":"Amir Kafshdar","last_name":"Goharshady","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Mohammadi, Fatemeh","first_name":"Fatemeh","last_name":"Mohammadi"}],"_id":"6918","scopus_import":"1","title":"An efficient algorithm for computing network reliability in small treewidth","intvolume":"       193","publication_status":"published","department":[{"_id":"KrCh"}],"article_processing_charge":"No","date_created":"2019-09-29T22:00:44Z","quality_controlled":"1","article_type":"original","publisher":"Elsevier","isi":1,"external_id":{"arxiv":["1712.09692"],"isi":["000501641400050"]},"date_updated":"2024-03-25T23:30:18Z","year":"2020","citation":{"ieee":"A. K. Goharshady and F. Mohammadi, “An efficient algorithm for computing network reliability in small treewidth,” <i>Reliability Engineering and System Safety</i>, vol. 193. Elsevier, 2020.","chicago":"Goharshady, Amir Kafshdar, and Fatemeh Mohammadi. “An Efficient Algorithm for Computing Network Reliability in Small Treewidth.” <i>Reliability Engineering and System Safety</i>. Elsevier, 2020. <a href=\"https://doi.org/10.1016/j.ress.2019.106665\">https://doi.org/10.1016/j.ress.2019.106665</a>.","apa":"Goharshady, A. K., &#38; Mohammadi, F. (2020). An efficient algorithm for computing network reliability in small treewidth. <i>Reliability Engineering and System Safety</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ress.2019.106665\">https://doi.org/10.1016/j.ress.2019.106665</a>","ama":"Goharshady AK, Mohammadi F. An efficient algorithm for computing network reliability in small treewidth. <i>Reliability Engineering and System Safety</i>. 2020;193. doi:<a href=\"https://doi.org/10.1016/j.ress.2019.106665\">10.1016/j.ress.2019.106665</a>","ista":"Goharshady AK, Mohammadi F. 2020. An efficient algorithm for computing network reliability in small treewidth. Reliability Engineering and System Safety. 193, 106665.","mla":"Goharshady, Amir Kafshdar, and Fatemeh Mohammadi. “An Efficient Algorithm for Computing Network Reliability in Small Treewidth.” <i>Reliability Engineering and System Safety</i>, vol. 193, 106665, Elsevier, 2020, doi:<a href=\"https://doi.org/10.1016/j.ress.2019.106665\">10.1016/j.ress.2019.106665</a>.","short":"A.K. Goharshady, F. Mohammadi, Reliability Engineering and System Safety 193 (2020)."},"abstract":[{"lang":"eng","text":"We consider the classic problem of Network Reliability. A network is given together with a source vertex, one or more target vertices, and probabilities assigned to each of the edges. Each edge of the network is operable with its associated probability and the problem is to determine the probability of having at least one source-to-target path that is entirely composed of operable edges. This problem is known to be NP-hard.\r\n\r\nWe provide a novel scalable algorithm to solve the Network Reliability problem when the treewidth of the underlying network is small. We also show our algorithm’s applicability for real-world transit networks that have small treewidth, including the metro networks of major cities, such as London and Tokyo. Our algorithm leverages tree decompositions to shrink the original graph into much smaller graphs, for which reliability can be efficiently and exactly computed using a brute force method. To the best of our knowledge, this is the first exact algorithm for Network Reliability that can scale to handle real-world instances of the problem."}],"doi":"10.1016/j.ress.2019.106665","arxiv":1,"day":"01","volume":193,"acknowledgement":"We are grateful to the anonymous reviewers for their comments, which significantly improved the present work. The research was partially supported by the EPSRC Early Career Fellowship EP/R023379/1, grant no. SC7-1718-01 of the London Mathematical Society, an IBM PhD Fellowship, and a DOC Fellowship of the Austrian Academy of Sciences (ÖAW).","publication":"Reliability Engineering and System Safety","month":"01","article_number":"106665","oa_version":"Preprint","project":[{"name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts","_id":"266EEEC0-B435-11E9-9278-68D0E5697425"}],"language":[{"iso":"eng"}],"date_published":"2020-01-01T00:00:00Z","type":"journal_article","oa":1,"publication_identifier":{"issn":["09518320"]},"related_material":{"record":[{"id":"8934","relation":"dissertation_contains","status":"public"}]},"status":"public","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","main_file_link":[{"url":"https://arxiv.org/abs/1712.09692","open_access":"1"}]},{"publication":"Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications ","has_accepted_license":"1","oa_version":"Published Version","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies"},{"_id":"266EEEC0-B435-11E9-9278-68D0E5697425","name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts"}],"month":"10","article_number":"129","language":[{"iso":"eng"}],"conference":{"start_date":"2019-10-23","name":"OOPSLA: Object-oriented Programming, Systems, Languages and Applications","location":"Athens, Greece","end_date":"2019-10-25"},"tmp":{"name":"Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)","image":"/images/cc_by_nc.png","short":"CC BY-NC (4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc/4.0/legalcode"},"date_published":"2019-10-01T00:00:00Z","type":"conference","oa":1,"file":[{"file_id":"6807","creator":"akafshda","relation":"main_file","access_level":"open_access","date_updated":"2020-07-14T12:47:40Z","file_name":"oopsla-2019.pdf","content_type":"application/pdf","date_created":"2019-08-12T15:40:57Z","file_size":1024643,"checksum":"3482d8ace6fb4991eb7810e3b70f1b9f"},{"file_size":538579,"checksum":"4e5a6fb2b59a75222a4e8335a5a60eac","date_created":"2020-05-12T15:15:14Z","file_name":"2019_ACM_Huang.pdf","content_type":"application/pdf","date_updated":"2020-07-14T12:47:40Z","relation":"main_file","access_level":"open_access","creator":"dernst","file_id":"7821"}],"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","status":"public","related_material":{"record":[{"relation":"dissertation_contains","id":"8934","status":"public"}]},"_id":"6780","license":"https://creativecommons.org/licenses/by-nc/4.0/","author":[{"first_name":"Mingzhang","last_name":"Huang","full_name":"Huang, Mingzhang"},{"last_name":"Fu","first_name":"Hongfei","full_name":"Fu, Hongfei"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"last_name":"Goharshady","first_name":"Amir Kafshdar","full_name":"Goharshady, Amir Kafshdar","orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87"}],"publication_status":"published","date_created":"2019-08-09T09:54:20Z","department":[{"_id":"KrCh"}],"article_processing_charge":"No","title":"Modular verification for almost-sure termination of probabilistic programs","intvolume":"         3","quality_controlled":"1","ec_funded":1,"file_date_updated":"2020-07-14T12:47:40Z","publisher":"ACM","date_updated":"2025-06-02T08:53:47Z","citation":{"apa":"Huang, M., Fu, H., Chatterjee, K., &#38; Goharshady, A. K. (2019). Modular verification for almost-sure termination of probabilistic programs. 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/3360555\">https://doi.org/10.1145/3360555</a>","ama":"Huang M, Fu H, Chatterjee K, Goharshady AK. Modular verification for almost-sure termination of probabilistic programs. 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/3360555\">10.1145/3360555</a>","chicago":"Huang, Mingzhang, Hongfei Fu, Krishnendu Chatterjee, and Amir Kafshdar Goharshady. “Modular Verification for Almost-Sure Termination of Probabilistic Programs.” 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/3360555\">https://doi.org/10.1145/3360555</a>.","ieee":"M. Huang, H. Fu, K. Chatterjee, and A. K. Goharshady, “Modular verification for almost-sure termination of probabilistic programs,” in <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications </i>, Athens, Greece, 2019, vol. 3.","mla":"Huang, Mingzhang, et al. “Modular Verification for Almost-Sure Termination of Probabilistic Programs.” <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications </i>, vol. 3, 129, ACM, 2019, doi:<a href=\"https://doi.org/10.1145/3360555\">10.1145/3360555</a>.","short":"M. Huang, H. Fu, K. Chatterjee, A.K. Goharshady, in:, Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications , ACM, 2019.","ista":"Huang M, Fu H, Chatterjee K, Goharshady AK. 2019. Modular verification for almost-sure termination of probabilistic programs. 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, 129."},"year":"2019","external_id":{"arxiv":["1901.06087"]},"doi":"10.1145/3360555","arxiv":1,"day":"01","abstract":[{"lang":"eng","text":"In this work, we consider the almost-sure termination problem for probabilistic programs that asks whether a\r\ngiven probabilistic program terminates with probability 1. Scalable approaches for program analysis often\r\nrely on modularity as their theoretical basis. In non-probabilistic programs, the classical variant rule (V-rule)\r\nof Floyd-Hoare logic provides the foundation for modular analysis. Extension of this rule to almost-sure\r\ntermination of probabilistic programs is quite tricky, and a probabilistic variant was proposed in [16]. While the\r\nproposed probabilistic variant cautiously addresses the key issue of integrability, we show that the proposed\r\nmodular rule is still not sound for almost-sure termination of probabilistic programs.\r\nBesides establishing unsoundness of the previous rule, our contributions are as follows: First, we present a\r\nsound modular rule for almost-sure termination of probabilistic programs. Our approach is based on a novel\r\nnotion of descent supermartingales. Second, for algorithmic approaches, we consider descent supermartingales\r\nthat are linear and show that they can be synthesized in polynomial time. Finally, we present experimental\r\nresults on a variety of benchmarks and several natural examples that model various types of nested while\r\nloops in probabilistic programs and demonstrate that our approach is able to efficiently prove their almost-sure\r\ntermination property"}],"volume":3,"ddc":["000"]},{"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1705.00317"}],"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"639"},{"id":"8934","relation":"dissertation_contains","status":"public"}]},"status":"public","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","date_published":"2019-10-01T00:00:00Z","type":"journal_article","oa":1,"language":[{"iso":"eng"}],"publication":"ACM Transactions on Programming Languages and Systems","oa_version":"Preprint","project":[{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-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","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies","_id":"267066CE-B435-11E9-9278-68D0E5697425"},{"_id":"266EEEC0-B435-11E9-9278-68D0E5697425","name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts"}],"month":"10","article_number":"20","volume":41,"date_updated":"2025-06-02T08:53:47Z","citation":{"ieee":"K. Chatterjee, H. Fu, and A. K. Goharshady, “Non-polynomial worst-case analysis of recursive programs,” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 41, no. 4. ACM, 2019.","chicago":"Chatterjee, Krishnendu, Hongfei Fu, and Amir Kafshdar Goharshady. “Non-Polynomial Worst-Case Analysis of Recursive Programs.” <i>ACM Transactions on Programming Languages and Systems</i>. ACM, 2019. <a href=\"https://doi.org/10.1145/3339984\">https://doi.org/10.1145/3339984</a>.","apa":"Chatterjee, K., Fu, H., &#38; Goharshady, A. K. (2019). Non-polynomial worst-case analysis of recursive programs. <i>ACM Transactions on Programming Languages and Systems</i>. ACM. <a href=\"https://doi.org/10.1145/3339984\">https://doi.org/10.1145/3339984</a>","ama":"Chatterjee K, Fu H, Goharshady AK. Non-polynomial worst-case analysis of recursive programs. <i>ACM Transactions on Programming Languages and Systems</i>. 2019;41(4). doi:<a href=\"https://doi.org/10.1145/3339984\">10.1145/3339984</a>","ista":"Chatterjee K, Fu H, Goharshady AK. 2019. Non-polynomial worst-case analysis of recursive programs. ACM Transactions on Programming Languages and Systems. 41(4), 20.","mla":"Chatterjee, Krishnendu, et al. “Non-Polynomial Worst-Case Analysis of Recursive Programs.” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 41, no. 4, 20, ACM, 2019, doi:<a href=\"https://doi.org/10.1145/3339984\">10.1145/3339984</a>.","short":"K. Chatterjee, H. Fu, A.K. Goharshady, ACM Transactions on Programming Languages and Systems 41 (2019)."},"year":"2019","isi":1,"external_id":{"isi":["000564108400001"],"arxiv":["1705.00317"]},"doi":"10.1145/3339984","arxiv":1,"day":"01","abstract":[{"text":"We study the problem of developing efficient approaches for proving\r\nworst-case bounds of non-deterministic recursive programs. Ranking functions\r\nare sound and complete for proving termination and worst-case bounds of\r\nnonrecursive programs. First, we apply ranking functions to recursion,\r\nresulting in measure functions. We show that measure functions provide a sound\r\nand complete approach to prove worst-case bounds of non-deterministic recursive\r\nprograms. Our second contribution is the synthesis of measure functions in\r\nnonpolynomial forms. We show that non-polynomial measure functions with\r\nlogarithm and exponentiation can be synthesized through abstraction of\r\nlogarithmic or exponentiation terms, Farkas' Lemma, and Handelman's Theorem\r\nusing linear programming. While previous methods obtain worst-case polynomial\r\nbounds, our approach can synthesize bounds of the form $\\mathcal{O}(n\\log n)$\r\nas well as $\\mathcal{O}(n^r)$ where $r$ is not an integer. We present\r\nexperimental results to demonstrate that our approach can obtain efficiently\r\nworst-case bounds of classical recursive algorithms such as (i) Merge-Sort, the\r\ndivide-and-conquer algorithm for the Closest-Pair problem, where we obtain\r\n$\\mathcal{O}(n \\log n)$ worst-case bound, and (ii) Karatsuba's algorithm for\r\npolynomial multiplication and Strassen's algorithm for matrix multiplication,\r\nwhere we obtain $\\mathcal{O}(n^r)$ bound such that $r$ is not an integer and\r\nclose to the best-known bounds for the respective algorithms.","lang":"eng"}],"ec_funded":1,"quality_controlled":"1","publisher":"ACM","article_type":"original","_id":"7014","scopus_import":"1","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"first_name":"Hongfei","last_name":"Fu","full_name":"Fu, Hongfei"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","full_name":"Goharshady, Amir Kafshdar","orcid":"0000-0003-1702-6584","last_name":"Goharshady","first_name":"Amir Kafshdar"}],"issue":"4","publication_status":"published","date_created":"2019-11-13T08:33:43Z","article_processing_charge":"No","department":[{"_id":"KrCh"}],"title":"Non-polynomial worst-case analysis of recursive programs","intvolume":"        41"},{"month":"05","article_number":"8751326","oa_version":"Preprint","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"266EEEC0-B435-11E9-9278-68D0E5697425","name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts"},{"name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies","_id":"267066CE-B435-11E9-9278-68D0E5697425"}],"publication":"IEEE International Conference on Blockchain and Cryptocurrency","conference":{"end_date":"2019-05-17","location":"Seoul, Korea","name":"IEEE International Conference on Blockchain and Cryptocurrency","start_date":"2019-05-14"},"language":[{"iso":"eng"}],"oa":1,"date_published":"2019-05-01T00:00:00Z","type":"conference","status":"public","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"status":"public","id":"8934","relation":"dissertation_contains"}]},"main_file_link":[{"url":"https://arxiv.org/abs/1902.07986","open_access":"1"}],"title":"Probabilistic smart contracts: Secure randomness on the blockchain","publication_status":"published","department":[{"_id":"KrCh"}],"date_created":"2019-02-26T09:03:15Z","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","full_name":"Goharshady, Amir Kafshdar","orcid":"0000-0003-1702-6584","last_name":"Goharshady","first_name":"Amir Kafshdar"},{"last_name":"Pourdamghani","first_name":"Arash","full_name":"Pourdamghani, Arash"}],"_id":"6056","scopus_import":1,"publisher":"IEEE","quality_controlled":"1","ec_funded":1,"abstract":[{"text":"In today's programmable blockchains, smart contracts are limited to being deterministic and non-probabilistic. This lack of randomness is a consequential limitation, given that a wide variety of real-world financial contracts, such as casino games and lotteries, depend entirely on randomness. As a result, several ad-hoc random number generation approaches have been developed to be used in smart contracts. These include ideas such as using an oracle or relying on the block hash. However, these approaches are manipulatable, i.e. their output can be tampered with by parties who might not be neutral, such as the owner of the oracle or the miners.We propose a novel game-theoretic approach for generating provably unmanipulatable pseudorandom numbers on the blockchain. Our approach allows smart contracts to access a trustworthy source of randomness that does not rely on potentially compromised miners or oracles, hence enabling the creation of a new generation of smart contracts that are not limited to being non-probabilistic and can be drawn from the much more general class of probabilistic programs.","lang":"eng"}],"doi":"10.1109/BLOC.2019.8751326","arxiv":1,"day":"01","external_id":{"arxiv":["1902.07986"]},"date_updated":"2024-03-25T23:30:18Z","citation":{"ieee":"K. Chatterjee, A. K. Goharshady, and A. Pourdamghani, “Probabilistic smart contracts: Secure randomness on the blockchain,” in <i>IEEE International Conference on Blockchain and Cryptocurrency</i>, Seoul, Korea, 2019.","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, and Arash Pourdamghani. “Probabilistic Smart Contracts: Secure Randomness on the Blockchain.” In <i>IEEE International Conference on Blockchain and Cryptocurrency</i>. IEEE, 2019. <a href=\"https://doi.org/10.1109/BLOC.2019.8751326\">https://doi.org/10.1109/BLOC.2019.8751326</a>.","ama":"Chatterjee K, Goharshady AK, Pourdamghani A. Probabilistic smart contracts: Secure randomness on the blockchain. In: <i>IEEE International Conference on Blockchain and Cryptocurrency</i>. IEEE; 2019. doi:<a href=\"https://doi.org/10.1109/BLOC.2019.8751326\">10.1109/BLOC.2019.8751326</a>","apa":"Chatterjee, K., Goharshady, A. K., &#38; Pourdamghani, A. (2019). Probabilistic smart contracts: Secure randomness on the blockchain. In <i>IEEE International Conference on Blockchain and Cryptocurrency</i>. Seoul, Korea: IEEE. <a href=\"https://doi.org/10.1109/BLOC.2019.8751326\">https://doi.org/10.1109/BLOC.2019.8751326</a>","ista":"Chatterjee K, Goharshady AK, Pourdamghani A. 2019. Probabilistic smart contracts: Secure randomness on the blockchain. IEEE International Conference on Blockchain and Cryptocurrency. IEEE International Conference on Blockchain and Cryptocurrency, 8751326.","mla":"Chatterjee, Krishnendu, et al. “Probabilistic Smart Contracts: Secure Randomness on the Blockchain.” <i>IEEE International Conference on Blockchain and Cryptocurrency</i>, 8751326, IEEE, 2019, doi:<a href=\"https://doi.org/10.1109/BLOC.2019.8751326\">10.1109/BLOC.2019.8751326</a>.","short":"K. Chatterjee, A.K. Goharshady, A. Pourdamghani, in:, IEEE International Conference on Blockchain and Cryptocurrency, IEEE, 2019."},"year":"2019"},{"file_date_updated":"2020-07-14T12:47:20Z","page":"204-220","ec_funded":1,"quality_controlled":"1","publisher":"Association for Computing Machinery","author":[{"full_name":"Wang, Peixin","last_name":"Wang","first_name":"Peixin"},{"id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","last_name":"Fu","first_name":"Hongfei","full_name":"Fu, Hongfei"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir Kafshdar","last_name":"Goharshady","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar"},{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Qin","first_name":"Xudong","full_name":"Qin, Xudong"},{"full_name":"Shi, Wenjun","first_name":"Wenjun","last_name":"Shi"}],"_id":"6175","scopus_import":"1","title":"Cost analysis of nondeterministic probabilistic programs","publication_status":"published","department":[{"_id":"KrCh"}],"date_created":"2019-03-25T10:13:25Z","article_processing_charge":"No","ddc":["000"],"isi":1,"external_id":{"arxiv":["1902.04659"],"isi":["000523190300014"]},"date_updated":"2025-06-02T08:53:45Z","year":"2019","citation":{"short":"P. Wang, H. Fu, A.K. Goharshady, K. Chatterjee, X. Qin, W. Shi, in:, PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2019, pp. 204–220.","mla":"Wang, Peixin, et al. “Cost Analysis of Nondeterministic Probabilistic Programs.” <i>PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation</i>, Association for Computing Machinery, 2019, pp. 204–20, doi:<a href=\"https://doi.org/10.1145/3314221.3314581\">10.1145/3314221.3314581</a>.","ista":"Wang P, Fu H, Goharshady AK, Chatterjee K, Qin X, Shi W. 2019. Cost analysis of nondeterministic probabilistic programs. PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI: Conference on Programming Language Design and Implementation, 204–220.","apa":"Wang, P., Fu, H., Goharshady, A. K., Chatterjee, K., Qin, X., &#38; Shi, W. (2019). Cost analysis of nondeterministic probabilistic programs. In <i>PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation</i> (pp. 204–220). Phoenix, AZ, United States: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3314221.3314581\">https://doi.org/10.1145/3314221.3314581</a>","ama":"Wang P, Fu H, Goharshady AK, Chatterjee K, Qin X, Shi W. Cost analysis of nondeterministic probabilistic programs. In: <i>PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation</i>. Association for Computing Machinery; 2019:204-220. doi:<a href=\"https://doi.org/10.1145/3314221.3314581\">10.1145/3314221.3314581</a>","ieee":"P. Wang, H. Fu, A. K. Goharshady, K. Chatterjee, X. Qin, and W. Shi, “Cost analysis of nondeterministic probabilistic programs,” in <i>PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation</i>, Phoenix, AZ, United States, 2019, pp. 204–220.","chicago":"Wang, Peixin, Hongfei Fu, Amir Kafshdar Goharshady, Krishnendu Chatterjee, Xudong Qin, and Wenjun Shi. “Cost Analysis of Nondeterministic Probabilistic Programs.” In <i>PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation</i>, 204–20. Association for Computing Machinery, 2019. <a href=\"https://doi.org/10.1145/3314221.3314581\">https://doi.org/10.1145/3314221.3314581</a>."},"abstract":[{"text":"We consider the problem of expected cost analysis over nondeterministic probabilistic programs,\r\nwhich aims at automated methods for analyzing the resource-usage of such programs.\r\nPrevious approaches for this problem could only handle nonnegative bounded costs.\r\nHowever, in many scenarios, such as queuing networks or analysis of cryptocurrency protocols,\r\nboth positive and negative costs are necessary and the costs are unbounded as well.\r\n\r\nIn this work, we present a sound and efficient approach to obtain polynomial bounds on the\r\nexpected accumulated cost of nondeterministic probabilistic programs.\r\nOur approach can handle (a) general positive and negative costs with bounded updates in\r\nvariables; and (b) nonnegative costs with general updates to variables.\r\nWe show that several natural examples which could not be\r\nhandled by previous approaches are captured in our framework.\r\n\r\nMoreover, our approach leads to an efficient polynomial-time algorithm, while no\r\nprevious approach for cost analysis of probabilistic programs could guarantee polynomial runtime.\r\nFinally, we show the effectiveness of our approach using experimental results on a variety of programs for which we efficiently synthesize tight resource-usage bounds.","lang":"eng"}],"arxiv":1,"doi":"10.1145/3314221.3314581","day":"08","language":[{"iso":"eng"}],"keyword":["Program Cost Analysis","Program Termination","Probabilistic Programs","Martingales"],"conference":{"name":"PLDI: Conference on Programming Language Design and Implementation","start_date":"2019-06-22","location":"Phoenix, AZ, United States","end_date":"2019-06-26"},"publication":"PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation","has_accepted_license":"1","month":"06","oa_version":"Submitted Version","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"grant_number":"S11407","name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"266EEEC0-B435-11E9-9278-68D0E5697425","name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts"}],"status":"public","related_material":{"record":[{"status":"public","id":"5457","relation":"earlier_version"},{"relation":"dissertation_contains","id":"8934","status":"public"}]},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","file":[{"relation":"main_file","access_level":"open_access","creator":"akafshda","file_id":"6176","file_size":4051066,"checksum":"703a5e9b8c8587f2a44085ffd9a4db64","date_created":"2019-03-25T10:11:22Z","file_name":"paper.pdf","content_type":"application/pdf","date_updated":"2020-07-14T12:47:20Z"}],"date_published":"2019-06-08T00:00:00Z","type":"conference","oa":1},{"author":[{"first_name":"Amir Kafshdar","last_name":"Goharshady","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Behrouz","first_name":"Ali","full_name":"Behrouz, Ali"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"}],"license":"https://creativecommons.org/licenses/by-nc-nd/4.0/","scopus_import":"1","_id":"6340","title":"Secure Credit Reporting on the Blockchain","date_created":"2019-04-18T10:37:35Z","article_processing_charge":"No","department":[{"_id":"KrCh"}],"publication_status":"published","file_date_updated":"2020-07-14T12:47:27Z","ec_funded":1,"quality_controlled":"1","page":"1343-1348","publisher":"IEEE","external_id":{"isi":["000481634500196"],"arxiv":["1805.09104"]},"isi":1,"citation":{"ieee":"A. K. Goharshady, A. Behrouz, and K. Chatterjee, “Secure Credit Reporting on the Blockchain,” in <i>Proceedings of the IEEE International Conference on Blockchain</i>, Halifax, Canada, 2018, pp. 1343–1348.","chicago":"Goharshady, Amir Kafshdar, Ali Behrouz, and Krishnendu Chatterjee. “Secure Credit Reporting on the Blockchain.” In <i>Proceedings of the IEEE International Conference on Blockchain</i>, 1343–48. IEEE, 2018. <a href=\"https://doi.org/10.1109/Cybermatics_2018.2018.00231\">https://doi.org/10.1109/Cybermatics_2018.2018.00231</a>.","ama":"Goharshady AK, Behrouz A, Chatterjee K. Secure Credit Reporting on the Blockchain. In: <i>Proceedings of the IEEE International Conference on Blockchain</i>. IEEE; 2018:1343-1348. doi:<a href=\"https://doi.org/10.1109/Cybermatics_2018.2018.00231\">10.1109/Cybermatics_2018.2018.00231</a>","apa":"Goharshady, A. K., Behrouz, A., &#38; Chatterjee, K. (2018). Secure Credit Reporting on the Blockchain. In <i>Proceedings of the IEEE International Conference on Blockchain</i> (pp. 1343–1348). Halifax, Canada: IEEE. <a href=\"https://doi.org/10.1109/Cybermatics_2018.2018.00231\">https://doi.org/10.1109/Cybermatics_2018.2018.00231</a>","ista":"Goharshady AK, Behrouz A, Chatterjee K. 2018. Secure Credit Reporting on the Blockchain. Proceedings of the IEEE International Conference on Blockchain. IEEE International Conference on Blockchain, 1343–1348.","mla":"Goharshady, Amir Kafshdar, et al. “Secure Credit Reporting on the Blockchain.” <i>Proceedings of the IEEE International Conference on Blockchain</i>, IEEE, 2018, pp. 1343–48, doi:<a href=\"https://doi.org/10.1109/Cybermatics_2018.2018.00231\">10.1109/Cybermatics_2018.2018.00231</a>.","short":"A.K. Goharshady, A. Behrouz, K. Chatterjee, in:, Proceedings of the IEEE International Conference on Blockchain, IEEE, 2018, pp. 1343–1348."},"year":"2018","date_updated":"2025-06-02T08:53:45Z","abstract":[{"text":"We  present  a  secure  approach  for  maintaining  andreporting  credit  history  records  on  the  Blockchain.  Our  ap-proach  removes  third-parties  such  as  credit  reporting  agen-cies  from  the  lending  process  and  replaces  them  with  smartcontracts.  This  allows  customers  to  interact  directly  with  thelenders  or  banks  while  ensuring  the  integrity,  unmalleabilityand  privacy  of  their  credit  data.  Additionally,  each  customerhas  full  control  over  complete  or  selective  disclosure  of  hercredit records, eliminating the risk of privacy violations or databreaches. Moreover, our approach provides strong guaranteesfor the lenders as well. A lender can check both correctness andcompleteness of the credit data disclosed to her. This is the firstapproach  that  can  perform  all  credit  reporting  tasks  withouta  central  authority  or  changing  the  financial  mechanisms*.","lang":"eng"}],"day":"01","doi":"10.1109/Cybermatics_2018.2018.00231","arxiv":1,"ddc":["000"],"has_accepted_license":"1","publication":"Proceedings of the IEEE International Conference on Blockchain","month":"09","project":[{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts","_id":"266EEEC0-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"oa_version":"Submitted Version","language":[{"iso":"eng"}],"conference":{"start_date":"2018-07-30","name":"IEEE International Conference on Blockchain","location":"Halifax, Canada","end_date":"2018-08-03"},"type":"conference","date_published":"2018-09-01T00:00:00Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","short":"CC BY-NC-ND (4.0)","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","image":"/images/cc_by_nc_nd.png"},"oa":1,"publication_identifier":{"isbn":["978-1-5386-7975-3 "]},"related_material":{"record":[{"relation":"dissertation_contains","id":"8934","status":"public"}]},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","file":[{"relation":"main_file","access_level":"open_access","creator":"akafshda","file_id":"6341","file_size":624338,"checksum":"b25c9bb7cf6e7e6634e692d26d41ead8","date_created":"2019-04-18T10:36:39Z","content_type":"application/pdf","file_name":"blockchain2018.pdf","date_updated":"2020-07-14T12:47:27Z"}]},{"volume":118,"ddc":["000"],"day":"01","arxiv":1,"doi":"10.4230/LIPIcs.CONCUR.2018.11","abstract":[{"lang":"eng","text":"Crypto-currencies are digital assets designed to work as a medium of exchange, e.g., Bitcoin, but they are susceptible to attacks (dishonest behavior of participants). A framework for the analysis of attacks in crypto-currencies requires (a) modeling of game-theoretic aspects to analyze incentives for deviation from honest behavior; (b) concurrent interactions between participants; and (c) analysis of long-term monetary gains. Traditional game-theoretic approaches for the analysis of security protocols consider either qualitative temporal properties such as safety and termination, or the very special class of one-shot (stateless) games. However, to analyze general attacks on protocols for crypto-currencies, both stateful analysis and quantitative objectives are necessary. In this work our main contributions are as follows: (a) we show how a class of concurrent mean-payo games, namely ergodic games, can model various attacks that arise naturally in crypto-currencies; (b) we present the first practical implementation of algorithms for ergodic games that scales to model realistic problems for crypto-currencies; and (c) we present experimental results showing that our framework can handle games with thousands of states and millions of transitions."}],"citation":{"ama":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Velner Y. Ergodic mean-payoff games for the analysis of attacks in crypto-currencies. In: Vol 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2018. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2018.11\">10.4230/LIPIcs.CONCUR.2018.11</a>","apa":"Chatterjee, K., Goharshady, A. K., Ibsen-Jensen, R., &#38; Velner, Y. (2018). Ergodic mean-payoff games for the analysis of attacks in crypto-currencies (Vol. 118). Presented at the CONCUR: Conference on Concurrency Theory, Beijing, China: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2018.11\">https://doi.org/10.4230/LIPIcs.CONCUR.2018.11</a>","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, and Yaron Velner. “Ergodic Mean-Payoff Games for the Analysis of Attacks in Crypto-Currencies,” Vol. 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2018.11\">https://doi.org/10.4230/LIPIcs.CONCUR.2018.11</a>.","ieee":"K. Chatterjee, A. K. Goharshady, R. Ibsen-Jensen, and Y. Velner, “Ergodic mean-payoff games for the analysis of attacks in crypto-currencies,” presented at the CONCUR: Conference on Concurrency Theory, Beijing, China, 2018, vol. 118.","mla":"Chatterjee, Krishnendu, et al. <i>Ergodic Mean-Payoff Games for the Analysis of Attacks in Crypto-Currencies</i>. Vol. 118, 11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2018.11\">10.4230/LIPIcs.CONCUR.2018.11</a>.","short":"K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, Y. Velner, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.","ista":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Velner Y. 2018. Ergodic mean-payoff games for the analysis of attacks in crypto-currencies. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 118, 11."},"year":"2018","date_updated":"2025-06-02T08:53:46Z","external_id":{"arxiv":["1806.03108"]},"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","ec_funded":1,"quality_controlled":"1","file_date_updated":"2020-07-14T12:47:34Z","department":[{"_id":"KrCh"}],"article_processing_charge":"No","date_created":"2018-12-11T11:44:27Z","publication_status":"published","intvolume":"       118","alternative_title":["LIPIcs"],"title":"Ergodic mean-payoff games for the analysis of attacks in crypto-currencies","scopus_import":"1","_id":"66","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir","last_name":"Goharshady","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","last_name":"Ibsen-Jensen"},{"full_name":"Velner, Yaron","last_name":"Velner","first_name":"Yaron"}],"file":[{"access_level":"open_access","relation":"main_file","file_id":"5696","creator":"dernst","date_created":"2018-12-17T12:08:00Z","file_size":1078309,"checksum":"68a055b1aaa241cc38375083cf832a7d","date_updated":"2020-07-14T12:47:34Z","content_type":"application/pdf","file_name":"2018_CONCUR_Chatterjee.pdf"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"status":"public","id":"8934","relation":"dissertation_contains"}]},"status":"public","publication_identifier":{"isbn":["978-3-95977-087-3"]},"publist_id":"7988","oa":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"type":"conference","date_published":"2018-09-01T00:00:00Z","conference":{"end_date":"2018-09-07","location":"Beijing, China","name":"CONCUR: Conference on Concurrency Theory","start_date":"2018-09-04"},"language":[{"iso":"eng"}],"project":[{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"266EEEC0-B435-11E9-9278-68D0E5697425","name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts"}],"oa_version":"Published Version","article_number":"11","month":"09","has_accepted_license":"1"}]