<p>i just discovered some really good software: SENinja <a href="https://github.com/borzacchiello/seninja" target="_blank" rel="nofollow noopener" translate="no"><span class="invisible">https://</span><span class="ellipsis">github.com/borzacchiello/senin</span><span class="invisible">ja</span></a></p><p>it lifts Binary Ninja's intermediate representation to a symbolic form and lifts it to an SMT2 representation, then feeds it to Z3</p><p>the user interface is like a debugger, except you get things like symbolic expression, or you can ask for which inputs will result in reaching a specific branch</p><p>this is so so so cool</p><p><a href="https://doi.org/10.1016/j.softx.2022.101219" target="_blank" rel="nofollow noopener" translate="no"><span class="invisible">https://</span><span class="ellipsis">doi.org/10.1016/j.softx.2022.1</span><span class="invisible">01219</span></a></p>
