[{"author":[{"full_name":"Goharshady, Amir Kafshdar","orcid":"0000-0003-1702-6584","last_name":"Goharshady","first_name":"Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87"}],"license":"https://creativecommons.org/publicdomain/zero/1.0/","_id":"8934","title":"Parameterized and algebro-geometric advances in static program analysis","alternative_title":["ISTA Thesis"],"date_created":"2020-12-10T12:17:07Z","article_processing_charge":"No","department":[{"_id":"KrCh"},{"_id":"GradSch"}],"publication_status":"published","file_date_updated":"2021-12-23T23:30:04Z","page":"278","publisher":"Institute of Science and Technology Austria","citation":{"ista":"Goharshady AK. 2021. Parameterized and algebro-geometric advances in static program analysis. Institute of Science and Technology Austria.","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.","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.","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>"},"year":"2021","date_updated":"2025-06-02T08:53:47Z","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","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).","has_accepted_license":"1","month":"01","project":[{"_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"}],"oa_version":"Published Version","language":[{"iso":"eng"}],"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"},"oa":1,"supervisor":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"}],"publication_identifier":{"issn":["2663-337X"]},"status":"public","related_material":{"record":[{"relation":"part_of_dissertation","id":"1386","status":"public"},{"id":"1437","relation":"part_of_dissertation","status":"public"},{"status":"public","id":"639","relation":"part_of_dissertation"},{"status":"public","id":"6918","relation":"part_of_dissertation"},{"status":"public","id":"6490","relation":"part_of_dissertation"},{"id":"7158","relation":"part_of_dissertation","status":"public"},{"id":"6009","relation":"part_of_dissertation","status":"public"},{"status":"public","id":"949","relation":"part_of_dissertation"},{"status":"public","id":"311","relation":"part_of_dissertation"},{"id":"7810","relation":"part_of_dissertation","status":"public"},{"status":"public","relation":"part_of_dissertation","id":"8089"},{"id":"8728","relation":"part_of_dissertation","status":"public"},{"status":"public","id":"5977","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","id":"6056","status":"public"},{"relation":"part_of_dissertation","id":"6175","status":"public"},{"status":"public","relation":"part_of_dissertation","id":"6340"},{"id":"6378","relation":"part_of_dissertation","status":"public"},{"status":"public","relation":"part_of_dissertation","id":"6380"},{"relation":"part_of_dissertation","id":"66","status":"public"},{"status":"public","relation":"part_of_dissertation","id":"6780"},{"id":"7014","relation":"part_of_dissertation","status":"public"}]},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","file":[{"checksum":"d1b9db3725aed34dadd81274aeb9426c","file_size":5251507,"date_created":"2020-12-22T20:08:44Z","embargo":"2021-12-22","content_type":"application/pdf","file_name":"Thesis-pdfa.pdf","date_updated":"2021-12-23T23:30:04Z","access_level":"open_access","relation":"main_file","creator":"akafshda","file_id":"8969"},{"date_updated":"2021-03-04T23:30:04Z","file_name":"source.zip","content_type":"application/zip","date_created":"2020-12-22T20:08:50Z","file_size":10636756,"checksum":"1661df7b393e6866d2460eba3c905130","embargo_to":"open_access","file_id":"8970","creator":"akafshda","relation":"source_file","access_level":"closed"}]},{"acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt), the National Natural Science Foundation of China (NSFC) Grant No. 61802254, the Huawei Innovation Research Program, the Facebook PhD Fellowship Program, and DOC Fellowship No. 24956 of the Austrian Academy of Sciences (ÖAW).","year":"2021","citation":{"chicago":"Asadi, Ali, Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, and Mohammad Mahdavi. “Polynomial Reachability Witnesses via Stellensätze.” In <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, 772–87. Association for Computing Machinery, 2021. <a href=\"https://doi.org/10.1145/3453483.3454076\">https://doi.org/10.1145/3453483.3454076</a>.","ieee":"A. Asadi, K. Chatterjee, H. Fu, A. K. Goharshady, and M. Mahdavi, “Polynomial reachability witnesses via Stellensätze,” in <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, Online, 2021, pp. 772–787.","apa":"Asadi, A., Chatterjee, K., Fu, H., Goharshady, A. K., &#38; Mahdavi, M. (2021). Polynomial reachability witnesses via Stellensätze. In <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i> (pp. 772–787). Online: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3453483.3454076\">https://doi.org/10.1145/3453483.3454076</a>","ama":"Asadi A, Chatterjee K, Fu H, Goharshady AK, Mahdavi M. Polynomial reachability witnesses via Stellensätze. In: <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>. Association for Computing Machinery; 2021:772-787. doi:<a href=\"https://doi.org/10.1145/3453483.3454076\">10.1145/3453483.3454076</a>","ista":"Asadi A, Chatterjee K, Fu H, Goharshady AK, Mahdavi M. 2021. Polynomial reachability witnesses via Stellensätze. Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation.  PLDI: Programming Language Design and Implementation, 772–787.","mla":"Asadi, Ali, et al. “Polynomial Reachability Witnesses via Stellensätze.” <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, Association for Computing Machinery, 2021, pp. 772–87, doi:<a href=\"https://doi.org/10.1145/3453483.3454076\">10.1145/3453483.3454076</a>.","short":"A. Asadi, K. Chatterjee, H. Fu, A.K. Goharshady, M. Mahdavi, in:, Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2021, pp. 772–787."},"date_updated":"2025-07-14T09:10:06Z","external_id":{"isi":["000723661700050"]},"isi":1,"day":"01","doi":"10.1145/3453483.3454076","abstract":[{"lang":"eng","text":"We consider the fundamental problem of reachability analysis over imperative programs with real variables. Previous works that tackle reachability are either unable to handle programs consisting of general loops (e.g. symbolic execution), or lack completeness guarantees (e.g. abstract interpretation), or are not automated (e.g. incorrectness logic). In contrast, we propose a novel approach for reachability analysis that can handle general and complex loops, is complete, and can be entirely automated for a wide family of programs. Through the notion of Inductive Reachability Witnesses (IRWs), our approach extends ideas from both invariant generation and termination to reachability analysis.\r\n\r\nWe first show that our IRW-based approach is sound and complete for reachability analysis of imperative programs. Then, we focus on linear and polynomial programs and develop automated methods for synthesizing linear and polynomial IRWs. In the linear case, we follow the well-known approaches using Farkas' Lemma. Our main contribution is in the polynomial case, where we present a push-button semi-complete algorithm. We achieve this using a novel combination of classical theorems in real algebraic geometry, such as Putinar's Positivstellensatz and Hilbert's Strong Nullstellensatz. Finally, our experimental results show we can prove complex reachability objectives over various benchmarks that were beyond the reach of previous methods."}],"ec_funded":1,"quality_controlled":"1","page":"772-787","publisher":"Association for Computing Machinery","scopus_import":"1","_id":"9645","author":[{"first_name":"Ali","last_name":"Asadi","full_name":"Asadi, Ali"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Hongfei","last_name":"Fu","full_name":"Fu, Hongfei","id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir Kafshdar","last_name":"Goharshady","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar"},{"first_name":"Mohammad","last_name":"Mahdavi","full_name":"Mahdavi, Mohammad"}],"date_created":"2021-07-11T22:01:17Z","article_processing_charge":"No","department":[{"_id":"KrCh"}],"publication_status":"published","title":"Polynomial reachability witnesses via Stellensätze","main_file_link":[{"open_access":"1","url":"https://hal.archives-ouvertes.fr/hal-03183862/"}],"status":"public","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","type":"conference","date_published":"2021-06-01T00:00:00Z","publication_identifier":{"isbn":["9781450383912"]},"oa":1,"language":[{"iso":"eng"}],"conference":{"name":" PLDI: Programming Language Design and Implementation","start_date":"2021-06-20","location":"Online","end_date":"2021-06-26"},"publication":"Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"_id":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies"}],"oa_version":"Submitted Version","month":"06"},{"day":"01","arxiv":1,"doi":"10.1145/3453483.3454102","abstract":[{"lang":"eng","text":"We consider the fundamental problem of deriving quantitative bounds on the probability that a given assertion is violated in a probabilistic program. We provide automated algorithms that obtain both lower and upper bounds on the assertion violation probability. The main novelty of our approach is that we prove new and dedicated fixed-point theorems which serve as the theoretical basis of our algorithms and enable us to reason about assertion violation bounds in terms of pre and post fixed-point functions. To synthesize such fixed-points, we devise algorithms that utilize a wide range of mathematical tools, including repulsing ranking supermartingales, Hoeffding's lemma, Minkowski decompositions, Jensen's inequality, and convex optimization. On the theoretical side, we provide (i) the first automated algorithm for lower-bounds on assertion violation probabilities, (ii) the first complete algorithm for upper-bounds of exponential form in affine programs, and (iii) provably and significantly tighter upper-bounds than the previous approaches. On the practical side, we show our algorithms can handle a wide variety of programs from the literature and synthesize bounds that are remarkably tighter than previous results, in some cases by thousands of orders of magnitude."}],"year":"2021","citation":{"ista":"Wang J, Sun Y, Fu H, Chatterjee K, Goharshady AK. 2021. Quantitative analysis of assertion violations in probabilistic programs. Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI: Programming Language Design and Implementation, 1171–1186.","mla":"Wang, Jinyi, et al. “Quantitative Analysis of Assertion Violations in Probabilistic Programs.” <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, Association for Computing Machinery, 2021, pp. 1171–86, doi:<a href=\"https://doi.org/10.1145/3453483.3454102\">10.1145/3453483.3454102</a>.","short":"J. Wang, Y. Sun, H. Fu, K. Chatterjee, A.K. Goharshady, in:, Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2021, pp. 1171–1186.","chicago":"Wang, Jinyi, Yican Sun, Hongfei Fu, Krishnendu Chatterjee, and Amir Kafshdar Goharshady. “Quantitative Analysis of Assertion Violations in Probabilistic Programs.” In <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, 1171–86. Association for Computing Machinery, 2021. <a href=\"https://doi.org/10.1145/3453483.3454102\">https://doi.org/10.1145/3453483.3454102</a>.","ieee":"J. Wang, Y. Sun, H. Fu, K. Chatterjee, and A. K. Goharshady, “Quantitative analysis of assertion violations in probabilistic programs,” in <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, Online, 2021, pp. 1171–1186.","apa":"Wang, J., Sun, Y., Fu, H., Chatterjee, K., &#38; Goharshady, A. K. (2021). Quantitative analysis of assertion violations in probabilistic programs. In <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i> (pp. 1171–1186). Online: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3453483.3454102\">https://doi.org/10.1145/3453483.3454102</a>","ama":"Wang J, Sun Y, Fu H, Chatterjee K, Goharshady AK. Quantitative analysis of assertion violations in probabilistic programs. In: <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>. Association for Computing Machinery; 2021:1171-1186. doi:<a href=\"https://doi.org/10.1145/3453483.3454102\">10.1145/3453483.3454102</a>"},"date_updated":"2025-07-14T09:10:06Z","external_id":{"arxiv":["2011.14617"],"isi":["000723661700076"]},"isi":1,"acknowledgement":"We are very thankful to the anonymous reviewers for the helpful and valuable comments. The work was partially supported by the National Natural Science Foundation of China (NSFC) Grant No. 61802254, the Huawei Innovation Research Program, the ERC CoG 863818 (ForM-SMArt), the Facebook PhD Fellowship Program and DOC Fellowship #24956 of the Austrian Academy of Sciences (ÖAW).","department":[{"_id":"KrCh"}],"article_processing_charge":"No","date_created":"2021-07-11T22:01:18Z","publication_status":"published","title":"Quantitative analysis of assertion violations in probabilistic programs","scopus_import":"1","_id":"9646","author":[{"full_name":"Wang, Jinyi","first_name":"Jinyi","last_name":"Wang"},{"full_name":"Sun, Yican","first_name":"Yican","last_name":"Sun"},{"id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","last_name":"Fu","first_name":"Hongfei","full_name":"Fu, Hongfei"},{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, 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"}],"publisher":"Association for Computing Machinery","quality_controlled":"1","ec_funded":1,"page":"1171-1186","publication_identifier":{"isbn":["9781450383912"]},"oa":1,"type":"conference","date_published":"2021-06-01T00:00:00Z","main_file_link":[{"url":"https://arxiv.org/abs/2011.14617","open_access":"1"}],"status":"public","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"_id":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies"}],"oa_version":"Preprint","month":"06","publication":"Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","conference":{"location":"Online","end_date":"2021-06-26","start_date":"2021-06-20","name":"PLDI: Programming Language Design and Implementation"},"language":[{"iso":"eng"}]},{"quality_controlled":"1","page":"112-140","file_date_updated":"2020-07-14T12:48:03Z","publisher":"Springer Nature","scopus_import":"1","_id":"7810","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","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar","first_name":"Amir Kafshdar","last_name":"Goharshady"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","last_name":"Ibsen-Jensen"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","first_name":"Andreas","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722"}],"date_created":"2020-05-10T22:00:50Z","article_processing_charge":"No","department":[{"_id":"KrCh"}],"publication_status":"published","intvolume":"     12075","alternative_title":["LNCS"],"title":"Optimal and perfectly parallel algorithms for on-demand data-flow analysis","volume":12075,"ddc":["000"],"citation":{"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.","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>","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>","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.","short":"K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, A. Pavlogiannis, in:, European Symposium on Programming, Springer Nature, 2020, pp. 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>."},"year":"2020","date_updated":"2025-06-02T08:53:42Z","external_id":{"isi":["000681656800005"]},"isi":1,"day":"18","doi":"10.1007/978-3-030-44914-8_5","abstract":[{"lang":"eng","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."}],"language":[{"iso":"eng"}],"conference":{"location":"Dublin, Ireland","end_date":"2020-04-30","name":"ESOP: Programming Languages and Systems","start_date":"2020-04-25"},"has_accepted_license":"1","publication":"European Symposium on Programming","project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"_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"}],"oa_version":"Published Version","month":"04","file":[{"content_type":"application/pdf","file_name":"2020_LNCS_Chatterjee.pdf","date_updated":"2020-07-14T12:48:03Z","checksum":"8618b80f4cf7b39a60e61a6445ad9807","file_size":651250,"date_created":"2020-05-26T13:34:48Z","creator":"dernst","file_id":"7895","access_level":"open_access","relation":"main_file"}],"status":"public","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"8934"}]},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","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":"2020-04-18T00:00:00Z","publication_identifier":{"eissn":["16113349"],"issn":["03029743"],"isbn":["9783030449131"]},"oa":1},{"file":[{"date_updated":"2020-10-19T11:14:20Z","file_name":"2020_ijmsi_Shakiba_accepted.pdf","content_type":"application/pdf","date_created":"2020-10-19T11:14:20Z","checksum":"f299661a6d51cda6d255a76be696f48d","file_size":261688,"file_id":"8676","creator":"dernst","relation":"main_file","access_level":"open_access","success":1}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","publication_identifier":{"issn":["1735-4463"],"eissn":["2008-9473"]},"oa":1,"date_published":"2020-10-01T00:00:00Z","type":"journal_article","language":[{"iso":"eng"}],"oa_version":"Submitted Version","project":[{"_id":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies"}],"month":"10","publication":"Iranian Journal of Mathematical Sciences and Informatics","has_accepted_license":"1","volume":15,"acknowledgement":"We are very grateful to the anonymous reviewer for detailed comments and suggestions that significantly improved the presentation of this paper. The research was partially supported by a DOC fellowship of the Austrian Academy of Sciences.","ddc":["000"],"arxiv":1,"doi":"10.29252/ijmsi.15.2.117","day":"01","abstract":[{"lang":"eng","text":"We study relations between evidence theory and S-approximation spaces. Both theories have their roots in the analysis of Dempsterchr('39')s multivalued mappings and lower and upper probabilities, and have close relations to rough sets. We show that an S-approximation space, satisfying a monotonicity condition, can induce a natural belief structure which is a fundamental block in evidence theory. We also demonstrate that one can induce a natural belief structure on one set, given a belief structure on another set, if the two sets are related by a partial monotone S-approximation space. "}],"date_updated":"2023-10-16T09:25:00Z","citation":{"ieee":"A. Shakiba, A. K. Goharshady, M. R. Hooshmandasl, and M. Alambardar Meybodi, “A note on belief structures and s-approximation spaces,” <i>Iranian Journal of Mathematical Sciences and Informatics</i>, vol. 15, no. 2. Iranian Academic Center for Education, Culture and Research, pp. 117–128, 2020.","chicago":"Shakiba, A., Amir Kafshdar Goharshady, M.R. Hooshmandasl, and M. Alambardar Meybodi. “A Note on Belief Structures and S-Approximation Spaces.” <i>Iranian Journal of Mathematical Sciences and Informatics</i>. Iranian Academic Center for Education, Culture and Research, 2020. <a href=\"https://doi.org/10.29252/ijmsi.15.2.117\">https://doi.org/10.29252/ijmsi.15.2.117</a>.","apa":"Shakiba, A., Goharshady, A. K., Hooshmandasl, M. R., &#38; Alambardar Meybodi, M. (2020). A note on belief structures and s-approximation spaces. <i>Iranian Journal of Mathematical Sciences and Informatics</i>. Iranian Academic Center for Education, Culture and Research. <a href=\"https://doi.org/10.29252/ijmsi.15.2.117\">https://doi.org/10.29252/ijmsi.15.2.117</a>","ama":"Shakiba A, Goharshady AK, Hooshmandasl MR, Alambardar Meybodi M. A note on belief structures and s-approximation spaces. <i>Iranian Journal of Mathematical Sciences and Informatics</i>. 2020;15(2):117-128. doi:<a href=\"https://doi.org/10.29252/ijmsi.15.2.117\">10.29252/ijmsi.15.2.117</a>","ista":"Shakiba A, Goharshady AK, Hooshmandasl MR, Alambardar Meybodi M. 2020. A note on belief structures and s-approximation spaces. Iranian Journal of Mathematical Sciences and Informatics. 15(2), 117–128.","mla":"Shakiba, A., et al. “A Note on Belief Structures and S-Approximation Spaces.” <i>Iranian Journal of Mathematical Sciences and Informatics</i>, vol. 15, no. 2, Iranian Academic Center for Education, Culture and Research, 2020, pp. 117–28, doi:<a href=\"https://doi.org/10.29252/ijmsi.15.2.117\">10.29252/ijmsi.15.2.117</a>.","short":"A. Shakiba, A.K. Goharshady, M.R. Hooshmandasl, M. Alambardar Meybodi, Iranian Journal of Mathematical Sciences and Informatics 15 (2020) 117–128."},"year":"2020","external_id":{"arxiv":["1805.10672"]},"publisher":"Iranian Academic Center for Education, Culture and Research","article_type":"original","page":"117-128","quality_controlled":"1","file_date_updated":"2020-10-19T11:14:20Z","publication_status":"published","date_created":"2020-10-18T22:01:36Z","article_processing_charge":"No","department":[{"_id":"KrCh"}],"title":"A note on belief structures and s-approximation spaces","intvolume":"        15","_id":"8671","scopus_import":"1","author":[{"full_name":"Shakiba, A.","last_name":"Shakiba","first_name":"A."},{"full_name":"Goharshady, Amir Kafshdar","orcid":"0000-0003-1702-6584","last_name":"Goharshady","first_name":"Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Hooshmandasl, M.R.","last_name":"Hooshmandasl","first_name":"M.R."},{"full_name":"Alambardar Meybodi, M.","first_name":"M.","last_name":"Alambardar Meybodi"}],"issue":"2"},{"file":[{"file_id":"8729","creator":"dernst","access_level":"open_access","relation":"main_file","success":1,"date_updated":"2020-11-06T07:41:03Z","content_type":"application/pdf","file_name":"2020_LNCS_ATVA_Asadi_accepted.pdf","date_created":"2020-11-06T07:41:03Z","checksum":"ae83f27e5b189d5abc2e7514f1b7e1b5","file_size":726648}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","related_material":{"record":[{"id":"8934","relation":"dissertation_contains","status":"public"}]},"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"eisbn":["9783030591526"],"isbn":["9783030591519"]},"oa":1,"date_published":"2020-10-12T00:00:00Z","type":"conference","conference":{"start_date":"2020-10-19","name":"ATVA: Automated Technology for Verification and Analysis","location":"Hanoi, Vietnam","end_date":"2020-10-23"},"language":[{"iso":"eng"}],"oa_version":"Submitted 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":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies"}],"month":"10","publication":"Automated Technology for Verification and Analysis","has_accepted_license":"1","volume":12302,"ddc":["000"],"doi":"10.1007/978-3-030-59152-6_14","day":"12","abstract":[{"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.","lang":"eng"}],"date_updated":"2025-06-02T08:53:43Z","year":"2020","citation":{"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>.","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>","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>","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>.","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."},"isi":1,"external_id":{"isi":["000723555700014"]},"publisher":"Springer Nature","page":"253-270","quality_controlled":"1","file_date_updated":"2020-11-06T07:41:03Z","publication_status":"published","date_created":"2020-11-06T07:30:05Z","article_processing_charge":"No","department":[{"_id":"KrCh"}],"alternative_title":["LNCS"],"title":"Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth","intvolume":"     12302","_id":"8728","scopus_import":"1","author":[{"last_name":"Asadi","first_name":"Ali","full_name":"Asadi, Ali"},{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"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":"Mohammadi","first_name":"Kiarash","full_name":"Mohammadi, Kiarash"},{"first_name":"Andreas","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"}]},{"conference":{"name":"OOPSLA: Object-oriented Programming, Systems, Languages and Applications","start_date":"2019-10-23","location":"Athens, Greece","end_date":"2019-10-25"},"language":[{"iso":"eng"}],"month":"10","article_number":"129","oa_version":"Published Version","project":[{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"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"}],"publication":"Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications ","has_accepted_license":"1","status":"public","related_material":{"record":[{"id":"8934","relation":"dissertation_contains","status":"public"}]},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","file":[{"file_id":"6807","creator":"akafshda","relation":"main_file","access_level":"open_access","date_updated":"2020-07-14T12:47:40Z","content_type":"application/pdf","file_name":"oopsla-2019.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"}],"oa":1,"date_published":"2019-10-01T00:00:00Z","type":"conference","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"},"publisher":"ACM","file_date_updated":"2020-07-14T12:47:40Z","ec_funded":1,"quality_controlled":"1","title":"Modular verification for almost-sure termination of probabilistic programs","intvolume":"         3","publication_status":"published","department":[{"_id":"KrCh"}],"article_processing_charge":"No","date_created":"2019-08-09T09:54:20Z","author":[{"last_name":"Huang","first_name":"Mingzhang","full_name":"Huang, Mingzhang"},{"last_name":"Fu","first_name":"Hongfei","full_name":"Fu, Hongfei"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","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"}],"_id":"6780","ddc":["000"],"volume":3,"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"}],"doi":"10.1145/3360555","arxiv":1,"day":"01","external_id":{"arxiv":["1901.06087"]},"date_updated":"2025-06-02T08:53:47Z","citation":{"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.","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>.","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>","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>","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.","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.","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>."},"year":"2019"},{"issue":"4","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Fu, Hongfei","last_name":"Fu","first_name":"Hongfei"},{"last_name":"Goharshady","first_name":"Amir Kafshdar","full_name":"Goharshady, Amir Kafshdar","orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87"}],"scopus_import":"1","_id":"7014","intvolume":"        41","title":"Non-polynomial worst-case analysis of recursive programs","department":[{"_id":"KrCh"}],"article_processing_charge":"No","date_created":"2019-11-13T08:33:43Z","publication_status":"published","quality_controlled":"1","ec_funded":1,"article_type":"original","publisher":"ACM","external_id":{"isi":["000564108400001"],"arxiv":["1705.00317"]},"isi":1,"year":"2019","citation":{"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.","short":"K. Chatterjee, H. Fu, A.K. Goharshady, ACM Transactions on Programming Languages and Systems 41 (2019).","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>.","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>"},"date_updated":"2025-06-02T08:53:47Z","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"}],"day":"01","arxiv":1,"doi":"10.1145/3339984","volume":41,"publication":"ACM Transactions on Programming Languages and Systems","article_number":"20","month":"10","project":[{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","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"},{"name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts","_id":"266EEEC0-B435-11E9-9278-68D0E5697425"}],"oa_version":"Preprint","language":[{"iso":"eng"}],"type":"journal_article","date_published":"2019-10-01T00:00:00Z","oa":1,"status":"public","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","related_material":{"record":[{"relation":"earlier_version","id":"639","status":"public"},{"status":"public","relation":"dissertation_contains","id":"8934"}]},"main_file_link":[{"url":"https://arxiv.org/abs/1705.00317","open_access":"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":{"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>","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>.","short":"K. Chatterjee, A.K. Goharshady, A. Pourdamghani, in:, IEEE International Conference on Blockchain and Cryptocurrency, IEEE, 2019.","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>.","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."},"year":"2019","title":"Probabilistic smart contracts: Secure randomness on the blockchain","publication_status":"published","department":[{"_id":"KrCh"}],"date_created":"2019-02-26T09:03:15Z","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 Kafshdar","last_name":"Goharshady","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar"},{"full_name":"Pourdamghani, Arash","first_name":"Arash","last_name":"Pourdamghani"}],"_id":"6056","scopus_import":1,"publisher":"IEEE","ec_funded":1,"quality_controlled":"1","oa":1,"date_published":"2019-05-01T00:00:00Z","type":"conference","related_material":{"record":[{"id":"8934","relation":"dissertation_contains","status":"public"}]},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","status":"public","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1902.07986"}],"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"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","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"},{"_id":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies"}],"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"}]}]