Probabilistic Hoare-like Logics in Comparison
| Title | Probabilistic Hoare-like Logics in Comparison |
| Publication Type | Report |
| Year of Publication | 2004 |
| Authors | Vásquez, MD, Wolovick, N, D'Argenio, PR |
| Series Title | Unpublished Technical Report |
| Institution | Universidad Nacional de Córdoba |
| Abstract | Probabilisticalgorithmsarerecognizedfortheirsimplicityandspeed. 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. |
PDF (Full text):
