Year: 2020

MicroTESK framework and our ongoing research on online test program generation were presented at RISC-V Summit held online on December 8-10, 2020. The idea is that a generator (at least some part of it) works inside the design under test and constructs test programs on the fly. Each test is supplied with an equivalent mutant, and the CPU is checked by comparing their results. RISC-V is a free and open ISA enabling a new era of processor innovation through open standard collaboration. Each year, the RISC-V Foundation hosts RISC-V Summit and other events to bring the expansive ecosystem together to discuss current and prospective RISC-V projects and implementations, as well as collectively drive the future evolution of the ISA forward. https://riscv.org/ https://tmt.knect365.com/risc-v-summit/

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…