News

Home > News > Wang Yuting's Team Makes Research Progress in Machine Code Verification

Wang Yuting's Team Makes Research Progress in Machine Code Verification

June 21, 2021      Author:

Recently, Wang Yuting, a tenure-track associate professor from the School of Electronic Information and Electrical Engineering at Shanghai Jiao Tong University, together with his team, has made significant progress in the field of machine code verification in theoretical computing. The research result "Automatic Generation and Validation of Instruction Encoders and Decoders" has been accepted by the 33rd International Conference on Computer-Aided Verification (CAV2021), a top conference in the field of computer science theories. The research is based on the 38th Shanghai Jiao Tong University PRP (Participation in Research Program) project "Formalization of Instruction Encoding and Decoding" supervised by Wang Yuting.

CAV is one of the top conferences in the field of computer science theory and is recommended by the Chinese Computer Federation (CCF) as a Category A conference. The conference is dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems, covering the spectrum from practical verification tools to the algorithms and techniques needed to implement these tools. CAV selects only 2-3 papers each year with Chinese research institutions as the first unit.

The team has developed a framework that automatically generates encoders and decoders and their consistency proofs from a precise instruction specification, providing a logically guaranteed correctness of the encoding and decoding process.  The framework has been successfully applied to a key subset of the x86 instruction set.

This research addresses the important question of how to automatically generate consistent, verified encoders and decoders, which not only removes a key obstacle to the further development of dependable software for manipulating machine code, but has also significantly advanced the study of formalised instruction set architectures.

 

 

Source: School of Electronic Information and Electrical Engineering, SJTU

Translated by Chen Chen

Proofread by Fu Yuhe