4 ms·
Could this be used to show that two programs (with only instructions from the covered subset) are equivalent?
by weinzierl 3y ago
Could this be used to show that two programs (with only instructions from the covered subset) are equivalent?
- boomanaiden154 3y agoYou can use it to (mostly) validate small snippets are the same. See Alive2 for the application of Z3/formalization of programs as SMT for that [1]. As far as I'm aware there are some problems scaling up to arbitrarily sized programs due to a lack of formalization in higher level languages in addition to computational constraints. With a lot of time and effort it can be done though [2]. 1. https://github.com/AliveToolkit/alive2 https://github.com/AliveToolkit/alive2 2. https://sel4.systems/ https://sel4.systems/