Our research on binary code deductive verification was presented at the Workshop on Design Automation for Understanding Hardware Designs (DUHDe), a part of the Design Automation and Test in Europe Conference (DATE), held in Florence, Italy on March 29, 2019.
In this work, MicroTESK is used to specify a target instruction set architecture (ISA) and to extract the symbolic representation of a given binary file. Other tools in use include Frama-C, Jessie, and Why3. To demonstrate the approach, we utilize RISC-V, a free and open ISA.
