In this spring and summer, we wrote two papers on deductive verification of binary code against source-code-level specifications: one of them was published in Proceedings of the 14th International Conference of Tests and Proofs (TAP 2020); the other was presented at the 14th Spring/Summer Young Researchers’ Colloquium on Software Engineering (SYRCoSE 2020) and published in Proceedings of ISP RAS. In both works, we used MicroTESK to extract semantics of binary code and build the intermediate representation. The TAP conference promotes research in verification and formal methods that targets the interplay of proofs and testing: the advancement of techniques of each kind and their combination, with the ultimate goal of improving software and system dependability. SYRCoSE is an annual colloquium on software engineering targeted at young researchers. The main goal of…
The MicroTESK framework and the MicroTESK-based test suite for RISC-V microprocessors (so called RISC-V AVS) were presented at DVCon Europe (Design and Verification Conference and Exhibition) held in Munich, Germany on October 29-30, 2019. MicroTESK for RISC-V: https://forge.ispras.ru/projects/microtesk-riscv RISC-V AVS: https://github.com/ispras/riscv-avs
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.
MicroTESK was presented at the All-Russia Science & Technology Conference "Problems of Advanced Micro- and Nanoelectronic Systems Development" (MES) held in Zelenograd, Moscow on October 1-5, 2018. MES is a biennial conference in design automation of micro-and nanoelectronics. It is a biggest Russian event in the area that provides a unique opportunity, bringing together hardware designers, CAD developers, and researchers.
MicroTESK (more precisely, an experimental part aimed at online test program generation) was demonstrated at DATE 2018’s University Booth exhibition held in Dresden, Germany on March 20-22, 2018. Alexander Kamkin and Mikhail Chupilko demonstrated the MicroTESK framework and its experimental facilities for automating online test program generation. DATE is the main European event bringing together designers and design automation users, researchers and vendors, as well as specialists in the hardware and software design, test and manufacturing of electronic circuits and systems.
MicroTESK was presented at the tool demo session of the Haifa Verification Conference (HVC) held in Haifa, Israel on November 13-15, 2017. HVC 2017 is the 13th in the series of annual conferences dedicated to advancing the state-of the art and state-of-the-practice in verification and testing. The conference provides a forum for researchers and practitioners from academia and industry to share their work, exchange ideas, and discuss the future directions of testing and verification for hardware, software, and complex hybrid systems. The common underlying goal of these techniques is to ensure the correct functionality and performance of complex systems. HVC is the only conference that brings together researchers and practitioners from all verification and testing sub-fields, thereby encouraging the migration of methods and ideas among domains.
MicroTESK was presented at the Digital Design and Computer Architecture workshop, a part of the Nano and Giga Challenges in Electronics (NGC) conference held in Tomsk, Russia on September 18-22, 2017. It was a Russian-speaking forum divided into two tracks: a student school and a meeting on digital design education. Alexander Kamkin made a presentation at the second track. We think that MicroTESK is a good option for teaching computer design and verification. Here are some reasons for that. Test program generators (TPGs) are essential verification tools. MicroTESK is an open-source TPG, while other similar tools are closed. MicroTESK includes a set of pre-defined ISA specifications, e.g., MIPS. MicroTESK is being used in real-life CPU design projects.
MicroTESK together with a Spin-based extension for verifying cache coherency mechanisms was presented at the University Booth exhibition of the Design, Automation and Test in Europe Conference (DATE) held in Lausanne, Switzerland on March 27-31, 2017. DATE is the main European event bringing together designers and design automation users, researchers and vendors, as well as specialists in the hardware and software design, test and manufacturing of electronic circuits and systems.