[mmarx]

> Theoretically, we could also go for finding the semantically equivalent C code. However, last time I researched, checking semantic equivalency is a very complex problem. I think it was NP hard.

Already deciding whether two finite automata decide the same (regular) language is PSPACE-complete; it's undecidable for anything that can decide arbitrary context-free languages (which C programs can clearly do).

[farooqkz]

Well I knew that checking if two binary circuits are equivalent is NP hard. Checking semantic equivalency of C code, of course, should be harder.