[{"month":"11","corr_author":"1","publisher":"Cambridge University Press","license":"https://creativecommons.org/licenses/by/4.0/","day":"18","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"year":"2020","type":"book_chapter","project":[{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory","call_identifier":"FWF"}],"status":"public","department":[{"_id":"KrCh"}],"has_accepted_license":"1","publication":"Foundations of Probabilistic Programming","article_processing_charge":"No","language":[{"iso":"eng"}],"file":[{"content_type":"application/pdf","file_size":316681,"date_updated":"2025-09-23T12:03:09Z","success":1,"relation":"main_file","checksum":"28ece115e8d2d9263e253a598e7caef2","date_created":"2025-09-23T12:03:09Z","file_name":"2020_ProbProgramming_Chatterjee.pdf","file_id":"20380","creator":"dernst","access_level":"open_access"}],"ddc":["000"],"date_updated":"2025-09-23T12:10:25Z","OA_place":"publisher","_id":"19986","date_created":"2025-07-10T13:28:51Z","doi":"10.1017/9781108770750.008","author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Fu, Hongfei","id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","first_name":"Hongfei","last_name":"Fu"},{"id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotný, Petr","last_name":"Novotný","first_name":"Petr"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"apa":"Chatterjee, K., Fu, H., &#38; Novotný, P. (2020). Termination Analysis of Probabilistic Programs with Martingales. In <i>Foundations of Probabilistic Programming</i> (pp. 221–258). Cambridge University Press. <a href=\"https://doi.org/10.1017/9781108770750.008\">https://doi.org/10.1017/9781108770750.008</a>","ama":"Chatterjee K, Fu H, Novotný P. Termination Analysis of Probabilistic Programs with Martingales. In: <i>Foundations of Probabilistic Programming</i>. Cambridge University Press; 2020:221-258. doi:<a href=\"https://doi.org/10.1017/9781108770750.008\">10.1017/9781108770750.008</a>","chicago":"Chatterjee, Krishnendu, Hongfei Fu, and Petr Novotný. “Termination Analysis of Probabilistic Programs with Martingales.” In <i>Foundations of Probabilistic Programming</i>, 221–58. Cambridge University Press, 2020. <a href=\"https://doi.org/10.1017/9781108770750.008\">https://doi.org/10.1017/9781108770750.008</a>.","mla":"Chatterjee, Krishnendu, et al. “Termination Analysis of Probabilistic Programs with Martingales.” <i>Foundations of Probabilistic Programming</i>, Cambridge University Press, 2020, pp. 221–58, doi:<a href=\"https://doi.org/10.1017/9781108770750.008\">10.1017/9781108770750.008</a>.","short":"K. Chatterjee, H. Fu, P. Novotný, in:, Foundations of Probabilistic Programming, Cambridge University Press, 2020, pp. 221–258.","ieee":"K. Chatterjee, H. Fu, and P. Novotný, “Termination Analysis of Probabilistic Programs with Martingales,” in <i>Foundations of Probabilistic Programming</i>, Cambridge University Press, 2020, pp. 221–258.","ista":"Chatterjee K, Fu H, Novotný P. 2020.Termination Analysis of Probabilistic Programs with Martingales. In: Foundations of Probabilistic Programming. , 221–258."},"date_published":"2020-11-18T00:00:00Z","oa":1,"acknowledgement":"Krishnendu Chatterjee is supported by the Austrian Science Fund (FWF) NFN\r\nGrant No. S11407-N23 (RiSE/SHiNE), and COST Action GAMENET. Hongfei Fu\r\nis supported by the National Natural Science Foundation of China (NSFC) Grant\r\nNo. 61802254. Petr Novotný is supported by the Czech Science Foundation grant\r\nNo. GJ19-15134Y.","publication_identifier":{"eisbn":["9781108770750"],"isbn":["9781108488518"]},"page":"221-258","file_date_updated":"2025-09-23T12:03:09Z","quality_controlled":"1","abstract":[{"text":"For non-probabilistic programs, a key question in static analysis is termination, which asks whether a given program terminates under a given initial condition. In the presence of probabilistic behaviour, there are two fundamental extensions of the termination question: (a) the almost-sure termination question, which asks whether the termination probability is 1; and (b) the bounded-time termination question, which asks whether the expected termination time is bounded. There are many active research directions to address these two questions; one important such direction is the use of martingale theory for termination analysis. In this chapter, we survey the main techniques of the martingale-based approach to the termination analysis of probabilistic programs.","lang":"eng"}],"oa_version":"Published Version","title":"Termination Analysis of Probabilistic Programs with Martingales","publication_status":"published"}]