Automatic generation and validation of instruction encoders and decoders

DOI10.1007/978-3-030-81688-9_34zbMATH Open1493.68223OpenAlexW3186771479MaRDI QIDQ832306FDOQ832306

Authors: Xiangzhe Xu, Jinhua Wu, Zhenguo Yin, Pengfei Li, Yu-Ting Wang 

Publication date: 25 March 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-81688-9_34

Recommendations

• Bidirectional grammars for machine-code decoding and encoding
• scientific article; zbMATH DE number 1614684
• Bidirectional grammars for machine-code decoding and encoding
• Deductive binary code verification against source-code-level specifications
• Formal verification of translation validators

zbMATH Keywords

translation validationprogram synthesisformalized instruction formatsproof synthesisverified parsing

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Simple, functional, sound and complete parsing for all context-free grammars
• Verified, Executable Parsing
• Validating LR(1) Parsers
• A trustworthy monadic formalization of the ARMv7 instruction set architecture
• Bidirectional grammars for machine-code decoding and encoding

Cited In (1)

• Bidirectional grammars for machine-code decoding and encoding

Uses Software

• Coq
• z3
• CompCert

This page was built for publication: Automatic generation and validation of instruction encoders and decoders

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832306)