@article{Olmedo:2018:JACM,
  author={Kaminski, Benjamin Lucien and Katoen, Joost-Pieter and Matheja, Christoph and Olmedo, Federico},
  title = {Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms},
  journal = {Journal of the ACM},
  volume = {65},
  number = {5},
  issue_date = {September 2018},
  year = {2018},
  publisher = {ACM}
}