[{"issue":"4","publication":"ACM Transactions on Programming Languages and Systems","file_date_updated":"2020-10-08T12:58:10Z","day":"01","type":"journal_article","intvolume":"        41","status":"public","has_accepted_license":"1","department":[{"_id":"KrCh"}],"date_created":"2019-12-09T08:33:33Z","file":[{"relation":"main_file","content_type":"application/pdf","creator":"dernst","file_id":"8632","success":1,"access_level":"open_access","date_updated":"2020-10-08T12:58:10Z","file_size":667357,"file_name":"2019_ACMTransactions_Chatterjee.pdf","checksum":"291cc86a07bd010d4815e177dac57b70","date_created":"2020-10-08T12:58:10Z"}],"month":"11","article_type":"original","date_published":"2019-11-01T00:00:00Z","publisher":"ACM","scopus_import":"1","language":[{"iso":"eng"}],"volume":41,"oa":1,"date_updated":"2024-03-25T23:30:19Z","article_processing_charge":"No","_id":"7158","publication_identifier":{"issn":["0164-0925"]},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","call_identifier":"FWF"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"}],"quality_controlled":"1","oa_version":"Submitted Version","publication_status":"published","citation":{"ieee":"K. Chatterjee, A. K. Goharshady, P. Goyal, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth,” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 41, no. 4. ACM, 2019.","apa":"Chatterjee, K., Goharshady, A. K., Goyal, P., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2019). Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth. <i>ACM Transactions on Programming Languages and Systems</i>. ACM. <a href=\"https://doi.org/10.1145/3363525\">https://doi.org/10.1145/3363525</a>","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Prateesh Goyal, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Faster Algorithms for Dynamic Algebraic Queries in Basic RSMs with Constant Treewidth.” <i>ACM Transactions on Programming Languages and Systems</i>. ACM, 2019. <a href=\"https://doi.org/10.1145/3363525\">https://doi.org/10.1145/3363525</a>.","mla":"Chatterjee, Krishnendu, et al. “Faster Algorithms for Dynamic Algebraic Queries in Basic RSMs with Constant Treewidth.” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 41, no. 4, 23, ACM, 2019, doi:<a href=\"https://doi.org/10.1145/3363525\">10.1145/3363525</a>.","ama":"Chatterjee K, Goharshady AK, Goyal P, Ibsen-Jensen R, Pavlogiannis A. Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth. <i>ACM Transactions on Programming Languages and Systems</i>. 2019;41(4). doi:<a href=\"https://doi.org/10.1145/3363525\">10.1145/3363525</a>","ista":"Chatterjee K, Goharshady AK, Goyal P, Ibsen-Jensen R, Pavlogiannis A. 2019. Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth. ACM Transactions on Programming Languages and Systems. 41(4), 23.","short":"K. Chatterjee, A.K. Goharshady, P. Goyal, R. Ibsen-Jensen, A. Pavlogiannis, ACM Transactions on Programming Languages and Systems 41 (2019)."},"abstract":[{"text":"Interprocedural analysis is at the heart of numerous applications in programming languages, such as alias analysis, constant propagation, and so on. Recursive state machines (RSMs) are standard models for interprocedural analysis. We consider a general framework with RSMs where the transitions are labeled from a semiring and path properties are algebraic with semiring operations. RSMs with algebraic path properties can model interprocedural dataflow analysis problems, the shortest path problem, the most probable path problem, and so on. The traditional algorithms for interprocedural analysis focus on path properties where the starting point is fixed as the entry point of a specific method. In this work, we consider possible multiple queries as required in many applications such as in alias analysis. The study of multiple queries allows us to bring in an important algorithmic distinction between the resource usage of the one-time preprocessing vs for each individual query. The second aspect we consider is that the control flow graphs for most programs have constant treewidth.\r\n\r\nOur main contributions are simple and implementable algorithms that support multiple queries for algebraic path properties for RSMs that have constant treewidth. Our theoretical results show that our algorithms have small additional one-time preprocessing but can answer subsequent queries significantly faster as compared to the current algorithmic solutions for interprocedural dataflow analysis. We have also implemented our algorithms and evaluated their performance for performing on-demand interprocedural dataflow analysis on various domains, such as for live variable analysis and reaching definitions, on a standard benchmark set. Our experimental results align with our theoretical statements and show that after a lightweight preprocessing, on-demand queries are answered much faster than the standard existing algorithmic approaches.\r\n","lang":"eng"}],"author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Goharshady, Amir Kafshdar","last_name":"Goharshady","orcid":"0000-0003-1702-6584","first_name":"Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Goyal","full_name":"Goyal, Prateesh","first_name":"Prateesh"},{"full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"article_number":"23","isi":1,"related_material":{"record":[{"relation":"dissertation_contains","id":"8934","status":"public"}]},"ddc":["000"],"year":"2019","doi":"10.1145/3363525","ec_funded":1,"external_id":{"isi":["000564108400004"]},"title":"Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth"},{"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"1438"}]},"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1510.08517"}],"article_number":"7","isi":1,"external_id":{"isi":["000434634500003"],"arxiv":["1510.08517"]},"title":"Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs","year":"2018","doi":"10.1145/3174800","ec_funded":1,"publication_identifier":{"issn":["0164-0925"]},"_id":"5993","oa_version":"Submitted Version","quality_controlled":"1","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23"},{"grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"},{"call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","arxiv":1,"article_processing_charge":"No","date_updated":"2023-09-19T14:38:42Z","oa":1,"volume":40,"abstract":[{"lang":"eng","text":"In this article, we consider the termination problem of probabilistic programs with real-valued variables. Thequestions concerned are: qualitative ones that ask (i) whether the program terminates with probability 1(almost-sure termination) and (ii) whether the expected termination time is finite (finite termination); andquantitative ones that ask (i) to approximate the expected termination time (expectation problem) and (ii) tocompute a boundBsuch that the probability not to terminate afterBsteps decreases exponentially (con-centration problem). To solve these questions, we utilize the notion of ranking supermartingales, which isa powerful approach for proving termination of probabilistic programs. In detail, we focus on algorithmicsynthesis of linear ranking-supermartingales over affine probabilistic programs (Apps) with both angelic anddemonic non-determinism. An important subclass of Apps is LRApp which is defined as the class of all Appsover which a linear ranking-supermartingale exists.Our main contributions are as follows. Firstly, we show that the membership problem of LRApp (i) canbe decided in polynomial time for Apps with at most demonic non-determinism, and (ii) isNP-hard and inPSPACEfor Apps with angelic non-determinism. Moreover, theNP-hardness result holds already for Appswithout probability and demonic non-determinism. Secondly, we show that the concentration problem overLRApp can be solved in the same complexity as for the membership problem of LRApp. Finally, we show thatthe expectation problem over LRApp can be solved in2EXPTIMEand isPSPACE-hard even for Apps withoutprobability and non-determinism (i.e., deterministic programs). Our experimental results demonstrate theeffectiveness of our approach to answer the qualitative and quantitative questions over Apps with at mostdemonic non-determinism."}],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"full_name":"Fu, Hongfei","last_name":"Fu","first_name":"Hongfei","id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87"},{"id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotný, Petr","last_name":"Novotný","first_name":"Petr"},{"first_name":"Rouzbeh","last_name":"Hasheminezhad","full_name":"Hasheminezhad, Rouzbeh"}],"citation":{"ista":"Chatterjee K, Fu H, Novotný P, Hasheminezhad R. 2018. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. ACM Transactions on Programming Languages and Systems. 40(2), 7.","short":"K. Chatterjee, H. Fu, P. Novotný, R. Hasheminezhad, ACM Transactions on Programming Languages and Systems 40 (2018).","mla":"Chatterjee, Krishnendu, et al. “Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs.” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 40, no. 2, 7, Association for Computing Machinery (ACM), 2018, doi:<a href=\"https://doi.org/10.1145/3174800\">10.1145/3174800</a>.","ama":"Chatterjee K, Fu H, Novotný P, Hasheminezhad R. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. <i>ACM Transactions on Programming Languages and Systems</i>. 2018;40(2). doi:<a href=\"https://doi.org/10.1145/3174800\">10.1145/3174800</a>","chicago":"Chatterjee, Krishnendu, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad. “Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs.” <i>ACM Transactions on Programming Languages and Systems</i>. Association for Computing Machinery (ACM), 2018. <a href=\"https://doi.org/10.1145/3174800\">https://doi.org/10.1145/3174800</a>.","ieee":"K. Chatterjee, H. Fu, P. Novotný, and R. Hasheminezhad, “Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs,” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 40, no. 2. Association for Computing Machinery (ACM), 2018.","apa":"Chatterjee, K., Fu, H., Novotný, P., &#38; Hasheminezhad, R. (2018). Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. <i>ACM Transactions on Programming Languages and Systems</i>. Association for Computing Machinery (ACM). <a href=\"https://doi.org/10.1145/3174800\">https://doi.org/10.1145/3174800</a>"},"publication_status":"published","date_created":"2019-02-14T12:29:10Z","department":[{"_id":"KrCh"}],"scopus_import":"1","publisher":"Association for Computing Machinery (ACM)","language":[{"iso":"eng"}],"month":"06","date_published":"2018-06-01T00:00:00Z","publication":"ACM Transactions on Programming Languages and Systems","issue":"2","intvolume":"        40","status":"public","day":"01","type":"journal_article"},{"date_published":"2018-08-01T00:00:00Z","month":"08","language":[{"iso":"eng"}],"publisher":"Association for Computing Machinery (ACM)","scopus_import":"1","department":[{"_id":"KrCh"}],"date_created":"2019-02-14T14:31:52Z","type":"journal_article","day":"01","status":"public","intvolume":"        40","issue":"3","publication":"ACM Transactions on Programming Languages and Systems","ec_funded":1,"year":"2018","doi":"10.1145/3210257","title":"Algorithms for algebraic path properties in concurrent systems of constant treewidth components","external_id":{"isi":["000444694800001"],"arxiv":["1510.07565"]},"main_file_link":[{"url":"https://arxiv.org/abs/1510.07565","open_access":"1"}],"isi":1,"article_number":"9","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"1437"},{"relation":"earlier_version","id":"5441","status":"public"},{"relation":"earlier_version","id":"5442","status":"public"},{"status":"public","relation":"dissertation_contains","id":"8934"}]},"publication_status":"published","citation":{"chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Amir Kafshdar Goharshady, and Andreas Pavlogiannis. “Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components.” <i>ACM Transactions on Programming Languages and Systems</i>. Association for Computing Machinery (ACM), 2018. <a href=\"https://doi.org/10.1145/3210257\">https://doi.org/10.1145/3210257</a>.","apa":"Chatterjee, K., Ibsen-Jensen, R., Goharshady, A. K., &#38; Pavlogiannis, A. (2018). Algorithms for algebraic path properties in concurrent systems of constant treewidth components. <i>ACM Transactions on Programming Languages and Systems</i>. Association for Computing Machinery (ACM). <a href=\"https://doi.org/10.1145/3210257\">https://doi.org/10.1145/3210257</a>","ieee":"K. Chatterjee, R. Ibsen-Jensen, A. K. Goharshady, and A. Pavlogiannis, “Algorithms for algebraic path properties in concurrent systems of constant treewidth components,” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 40, no. 3. Association for Computing Machinery (ACM), 2018.","ista":"Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. 2018. Algorithms for algebraic path properties in concurrent systems of constant treewidth components. ACM Transactions on Programming Languages and Systems. 40(3), 9.","short":"K. Chatterjee, R. Ibsen-Jensen, A.K. Goharshady, A. Pavlogiannis, ACM Transactions on Programming Languages and Systems 40 (2018).","mla":"Chatterjee, Krishnendu, et al. “Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components.” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 40, no. 3, 9, Association for Computing Machinery (ACM), 2018, doi:<a href=\"https://doi.org/10.1145/3210257\">10.1145/3210257</a>.","ama":"Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. Algorithms for algebraic path properties in concurrent systems of constant treewidth components. <i>ACM Transactions on Programming Languages and Systems</i>. 2018;40(3). doi:<a href=\"https://doi.org/10.1145/3210257\">10.1145/3210257</a>"},"author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389"},{"orcid":"0000-0003-1702-6584","last_name":"Goharshady","full_name":"Goharshady, Amir Kafshdar","first_name":"Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","first_name":"Andreas"}],"abstract":[{"lang":"eng","text":"We study algorithmic questions wrt algebraic path properties in concurrent systems, where the transitions of the system are labeled from a complete, closed semiring. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural problems that arise in program analysis. We consider that each component of the concurrent system is a graph with constant treewidth, a property satisfied by the controlflow graphs of most programs. We allow for multiple possible queries, which arise naturally in demand driven dataflow analysis. The study of multiple queries allows us to consider the tradeoff between the resource usage of the one-time preprocessing and for each individual query. The traditional approach constructs the product graph of all components and applies the best-known graph algorithm on the product. In this approach, even the answer to a single query requires the transitive closure (i.e., the results of all possible queries), which provides no room for tradeoff between preprocessing and query time.\r\nOur main contributions are algorithms that significantly improve the worst-case running time of the traditional approach, and provide various tradeoffs depending on the number of queries. For example, in a concurrent system of two components, the traditional approach requires hexic time in the worst case for answering one query as well as computing the transitive closure, whereas we show that with one-time preprocessing in almost cubic time, each subsequent query can be answered in at most linear time, and even the transitive closure can be computed in almost quartic time. Furthermore, we establish conditional optimality results showing that the worst-case running time of our algorithms cannot be improved without achieving major breakthroughs in graph algorithms (i.e., improving the worst-case bound for the shortest path problem in general graphs). Preliminary experimental results show that our algorithms perform favorably on several benchmarks.\r\n"}],"volume":40,"date_updated":"2024-03-25T23:30:19Z","oa":1,"article_processing_charge":"No","arxiv":1,"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23"},{"grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","oa_version":"Preprint","_id":"6009","publication_identifier":{"issn":["0164-0925"]}},{"language":[{"iso":"eng"}],"scopus_import":"1","publisher":"ACM","date_published":"2002-01-01T00:00:00Z","article_type":"original","month":"01","date_created":"2018-12-11T12:09:02Z","status":"public","intvolume":"        24","type":"journal_article","day":"01","page":"51 - 64","publication":"ACM Transactions on Programming Languages and Systems (TOPLAS)","issue":"1","title":"An assume-guarantee rule for checking simulation","doi":"10.1145/509705.509707","year":"2002","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A"},{"last_name":"Qadeer","full_name":"Qadeer, Shaz","first_name":"Shaz"},{"full_name":"Rajamani, Sriram","last_name":"Rajamani","first_name":"Sriram"},{"first_name":"Serdar","last_name":"Tasiran","full_name":"Tasiran, Serdar"}],"abstract":[{"lang":"eng","text":"The simulation preorder on state transition systems is widely accepted as a useful notion of refinement, both in its own right and as an efficiently checkable sufficient condition for trace containment. For composite systems, due to the exponential explosion of the state space, there is a need for decomposing a simulation check of the form P ≤s Q, denoting &quot;P is simulated by Q,&quot; into simpler simulation checks on the components of P and Q. We present an assume-guarantee rule that enables such a decomposition. To the best of our knowledge, this is the first assume-guarantee rule that applies to a refinement relation different from trace containment. Our rule is circular, and its soundness proof requires induction on trace trees. The proof is constructive: given simulation relations that witness the simulation preorder between corresponding components of P and Q, we provide a procedure for constructing a witness relation for P ≤s Q. We also extend our assume-guarantee rule to account for fairness constraints on transition systems."}],"citation":{"mla":"Henzinger, Thomas A., et al. “An Assume-Guarantee Rule for Checking Simulation.” <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>, vol. 24, no. 1, ACM, 2002, pp. 51–64, doi:<a href=\"https://doi.org/10.1145/509705.509707\">10.1145/509705.509707</a>.","ama":"Henzinger TA, Qadeer S, Rajamani S, Tasiran S. An assume-guarantee rule for checking simulation. <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>. 2002;24(1):51-64. doi:<a href=\"https://doi.org/10.1145/509705.509707\">10.1145/509705.509707</a>","short":"T.A. Henzinger, S. Qadeer, S. Rajamani, S. Tasiran, ACM Transactions on Programming Languages and Systems (TOPLAS) 24 (2002) 51–64.","ista":"Henzinger TA, Qadeer S, Rajamani S, Tasiran S. 2002. An assume-guarantee rule for checking simulation. ACM Transactions on Programming Languages and Systems (TOPLAS). 24(1), 51–64.","ieee":"T. A. Henzinger, S. Qadeer, S. Rajamani, and S. Tasiran, “An assume-guarantee rule for checking simulation,” <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>, vol. 24, no. 1. ACM, pp. 51–64, 2002.","apa":"Henzinger, T. A., Qadeer, S., Rajamani, S., &#38; Tasiran, S. (2002). An assume-guarantee rule for checking simulation. <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>. ACM. <a href=\"https://doi.org/10.1145/509705.509707\">https://doi.org/10.1145/509705.509707</a>","chicago":"Henzinger, Thomas A, Shaz Qadeer, Sriram Rajamani, and Serdar Tasiran. “An Assume-Guarantee Rule for Checking Simulation.” <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>. ACM, 2002. <a href=\"https://doi.org/10.1145/509705.509707\">https://doi.org/10.1145/509705.509707</a>."},"publication_status":"published","quality_controlled":"1","oa_version":"None","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","extern":"1","publication_identifier":{"issn":["0164-0925"]},"_id":"4473","article_processing_charge":"No","publist_id":"256","volume":24,"date_updated":"2023-06-05T07:59:47Z"}]