MicroTESK @ SYRCoSE 2019

Conferences
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.
Read More

MicroTESK @ DUHDe 2019

New Features
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.  
Read More

MicroTESK for RISC-V 0.0.8 Released

New Features
MicroTESK for RISC-V 0.0.8 has been released. New features are as follows: Specification of address translation (Sv32, Sv39, and Sv48) Demo templates for address translation Test suite based on QEMU4V 0.3.2 MicroTESK for RISC-V 0.0.8 can be downloaded from here.
Read More

MicroTESK 2.4.45 Released

New Features
MicroTESK 2.4.45 has been released New features are as follows: Block-level register allocation constraints; MMU plugin: structures' fields are listed from upper to lower bits. Block-level register allocation constraints This facility is aimed at overriding default settings written in the configuration file. MicroTESK 2.4.45 can be downloaded from here.
Read More