Majority Vote Algorithm Revisited Again
    Download PDF
Tobias Nipkow. Majority Vote Algorithm Revisited Again. International Journal of Software and Informatics, 2011,5(1-2Part1):21~28
Hits: 3557
Download times: 1759
Abstract:In his article Experience with Software Specification and Verification Using LP, the Larch Proof Assistant, Manfred Broy verified (as one of his smaller case studies) the Majority Vote Algorithm by Boyer and Moore. LP requires that all user theories are expressed axiomatically. I reworked the example in Isabelle/HOL and turned it into a definitional development, thus proving its consistency. In the end, a short alternative proof is given.
keywords:majority vote algorithm  verification
View Full Text  View/Add Comment  Download reader

 

 

more>>  
Visitor:1778825
Top Paper  |  FAQ  |  Guest Editors  |  Email Alert  |  Links  |  Copyright  |  Contact Us

© Copyright by Institute of Software, the Chinese Academy of Sciences
ICP: Jing ICP Bei No.10016592

京公网安备 11040202500065号