ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Sun 7 Apr 2019 11:30 - 12:00 at S7 - Session II

In this paper we present an algorithm for the automatic synthesis of polynomial invariants for probabilistic transition systems. Our approach is based on martingale theory. We construct invariants in the form of polynomials over program variables, which give rise to martingales. These polynomials are program invariants in the sense that their expected value upon termination is the same as their value at the start of the computation. By exploiting geometric persistence properties of the system, we show that suitable polynomials can be automatically inferred using sum-of-squares optimisation techniques.

Sun 7 Apr
Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

qapl-2019-papers
11:00 - 12:30: QAPL - Session II at S7
qapl-2019-papers11:00 - 11:30
Talk
Mathias Ruggaard PedersenAalborg University, Giorgio BacciAalborg University, Kim LarsenAalborg University
Pre-print
qapl-2019-papers11:30 - 12:00
Talk
Anne SchreuderTechnischen Universität Kaiserslautern, C.-H. Luke OngUniversity of Oxford
Pre-print
qapl-2019-papers12:00 - 12:30
Talk
Jan Olaf BlechAalto University
Pre-print