MicroTESK for Binary Code Verification
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…