Our research-in-progress on binary code deductive verification was presented at the Spring/Summer Young Researchers’ Colloquium on Software Engineering (SYRCoSE) held in Saratov, Russia on May 29-31, 2019.
MicroTESK is used to specify a target instruction set architecture (ISA) and to extract the symbolic representation of a given binary file.