\myheading{Formal verification of population count functions using CBMC}

\leveldown{}

\renewcommand{\CURPATH}{verif/popcount}

This time we'll prove equivalence of several 64-bit functions, a case when bruteforce isn't feasible.

The population count function is the function that counts number of 1 bits in the input word,
\ac{AKA} Hamming weight.

Many of them I've copypasted from
the Wikipedia article\footnote{\url{https://en.wikipedia.org/wiki/Hamming_weight}}
about this function and from
the chessprogramming.org website\footnote{\url{https://www.chessprogramming.org/Population_Count}}.

See also John Regehr's blog post\footnote{\url{https://blog.regehr.org/archives/1667}} about it.

These hackish functions are very arcane, hard to understand and therefore are highly prone to (unnoticed) typos.

I run CBMC and SMT solvers on my ancient Intel Core 2 Duo T9600 clocked at 2.13GHz.

\input{\CURPATH/CBMC}
\input{\CURPATH/SMT}

\myheading{Files used}

Here: \url{\RepoURL/\CURPATH/files}.

\levelup{}