[{"dini_type":"doc-type:conferenceObject","citation":{"apa":"Huang, M., Fu, H., Chatterjee, K., & Goharshady, A. K. (2019). Modular verification for almost-sure termination of probabilistic programs. In Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications (Vol. 3). Athens, Greece: ACM. https://doi.org/10.1145/3360555","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.","ieee":"M. Huang, H. Fu, K. Chatterjee, and A. K. Goharshady, “Modular verification for almost-sure termination of probabilistic programs,” in Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications , Athens, Greece, 2019, vol. 3.","mla":"Huang, Mingzhang, et al. “Modular Verification for Almost-Sure Termination of Probabilistic Programs.” Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications , vol. 3, 129, ACM, 2019, doi:10.1145/3360555.","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.","chicago":"Huang, Mingzhang, Hongfei Fu, Krishnendu Chatterjee, and Amir Kafshdar Goharshady. “Modular Verification for Almost-Sure Termination of Probabilistic Programs.” In Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications , Vol. 3. ACM, 2019. https://doi.org/10.1145/3360555."},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","external_id":{"arxiv":[]},"article_processing_charge":"No","author":[{"last_name":"Huang","first_name":"Mingzhang"},{"last_name":"Fu","first_name":"Hongfei"},{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0003-1702-6584","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir Kafshdar"}],"article_number":"129","project":[{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","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"}],"has_accepted_license":"1","publication":"Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications ","dc":{"date":["2019"],"type":["info:eu-repo/semantics/conferenceObject","doc-type:conferenceObject","text","http://purl.org/coar/resource_type/c_5794"],"publisher":["ACM"],"relation":["info:eu-repo/semantics/altIdentifier/doi/10.1145/3360555","info:eu-repo/semantics/altIdentifier/arxiv/1901.06087","info:eu-repo/grantAgreement/FWF//ICT15-003","info:eu-repo/grantAgreement/FWF//S11407","info:eu-repo/grantAgreement/EC/FP7/279307"],"source":["Huang M, Fu H, Chatterjee K, Goharshady AK. Modular verification for almost-sure termination of probabilistic programs. In: Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications . Vol 3. ACM; 2019. doi:10.1145/3360555"],"description":["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"],"identifier":["https://research-explorer.ista.ac.at/record/6780","https://research-explorer.ista.ac.at/download/6780/6807","https://research-explorer.ista.ac.at/download/6780/7821"],"title":["Modular verification for almost-sure termination of probabilistic programs"],"creator":["Huang, Mingzhang","Fu, Hongfei","Chatterjee, Krishnendu","Goharshady, Amir Kafshdar"],"language":["eng"],"rights":["https://creativecommons.org/licenses/by-nc/4.0/","info:eu-repo/semantics/openAccess"],"subject":["ddc:000"]},"day":"01","uri_base":"https://research-explorer.ista.ac.at","date_created":"2019-08-09T09:54:20Z","date_published":"2019-10-01T00:00:00Z","oa":1,"quality_controlled":"1","date_updated":"2024-03-27T23:30:33Z","ddc":[],"creator":{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","login":"akafshda"},"department":[{"_id":"KrCh","tree":[{"_id":"ResearchGroups"},{"_id":"IST"}]}],"file_date_updated":"2020-07-14T12:47:40Z","_id":"6780","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nc/4.0/legalcode","image":"/images/cc_by_nc.png","name":"Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)","short":"CC BY-NC (4.0)"},"conference":{"name":"OOPSLA: Object-oriented Programming, Systems, Languages and Applications","end_date":"2019-10-25","location":"Athens, Greece","start_date":"2019-10-23"},"type":"conference","status":"public","publication_status":"published","language":[{}],"file":[{"content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"3482d8ace6fb4991eb7810e3b70f1b9f","file_id":"6807","date_updated":"2020-07-14T12:47:40Z","file_size":1024643,"creator":"akafshda","date_created":"2019-08-12T15:40:57Z","file_name":"oopsla-2019.pdf"},{"creator":"dernst","file_size":538579,"date_updated":"2020-07-14T12:47:40Z","file_name":"2019_ACM_Huang.pdf","date_created":"2020-05-12T15:15:14Z","relation":"main_file","access_level":"open_access","content_type":"application/pdf","checksum":"4e5a6fb2b59a75222a4e8335a5a60eac","file_id":"7821"}],"ec_funded":1,"volume":3,"related_material":{"record":[{"relation":"dissertation_contains","id":"8934","status":"public"}]},"abstract":[{"lang":"eng"}],"oa_version":"Published Version","intvolume":" 3","month":"10"}]