Probabilistic Hoare-like Logics in Comparison

Abstract. Probabilistic algorithms are recognized for their simplicity and speed. A canonical example is the Miller-Rabin primality test algorithm. It is simple and achieves high accuracy with a small amount of computation. In this pa-per, we present two verification exercises of this algorithm using two different approaches: one being a probabilistic extension of the weakest precondition calculus [17, 15]. and the other, a probabilistic extension of Hoare logic [6, 7] We define verification strategies/patterns and establish comparisons between the logics, stressing their strengths and weaknesses