Majority Vote Algorithm Revisited Again

  • Nipkow T
  • 7

    Readers

    Mendeley users who have this article in their library.
  • N/A

    Citations

    Citations of this article.

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.

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document

There are no full text links

Authors

  • Tobias Nipkow

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free