problem

[cctv130]

Hello, I am currently aware that formal verification can be performed based on semantics. However, after reading your paper, I have a few questions. Besides symbolic execution, what else can we do? 1、Can we elevate a single disassembled instruction to a high-level programming language based on its semantics， for example c or c++? Semantic incompleteness of indirect replacement remill 2、Is it possible to convert binary file based on ISA semantics into the corresponding LLVM IR, or other SSA (Static Single Assignment forms) , for binary reverse engineering analysis? Thank you very much for such an excellent paper.