A shallow survey of formal methods for C code

Re:A shallow survey of formal methods for C code by axman6 on Tuesday September 09, 2014 @12:00AM (#8288685)

Is that second implementation in Hacker's Delight? Also it'd be interesting to see how z3 handles the examples shown there too (the logarithmic time algorithms using

    x'  = (x  & b10101010) >> 1 + x  & b01010101
    x'' = (x' & b11001100) >> 2 + x' & b00110011

or whatever it is)

[ Parent | on HN ]

Re:A shallow survey of formal methods for C code by pbsd on Tuesday September 09, 2014 @12:29AM (#8288749)

No: Z3 proves the Hacker's Delight* trick almost instantly. The implementation above is not actually faster in practice, so it's rarely used; but its equivalence to popcount relies on Z/2^64Z properties that solvers do not seem familiar with.

* This sort of trick is much older than Hacker's Delight, by the way; Knuth tracks it down to the 1950s in Volume 4A.

[ Parent | on HN ]