20-Apr-2015: Using Z3 theorem prover to prove equivalence of some bizarre alternative to XOR operation.

The text has been moved into: //yurichev.com/tmp/SAT_SMT_DRAFT.pdf

Update2: some of discussions:

http://www.reddit.com/r/programming/comments/33830f/using_z3_theorem_prover_to_prove_equivalence_of/

http://www.reddit.com/r/ReverseEngineering/comments/33815w/using_z3_theorem_prover_to_prove_equivalence_of/

http://www.reddit.com/r/Python/comments/3384bt/using_z3_theorem_prover_to_prove_equivalence_of/

https://news.ycombinator.com/item?id=9407366

http://vk.com/wall-30666517_1127706 (Russian social networking site)


This open sourced site and this page in particular is hosted on GitHub. Patches, suggestions and comments are welcome.


→ [list of blog posts, my twitter/facebook]

The page last updated on 16-September-2016