Automatic generation and validation of instruction encoders and decoders

DOI10.1007/978-3-030-81688-9_34MaRDI QIDQ832306zbMATH OpenOpenAlexFDO

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

Publication date 25 March 2022

Copyright license Creative Commons Attribution 4.0 International

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

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)

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

Cites work

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

Cited in

(1)

• Bidirectional grammars for machine-code decoding and encoding

Describes a project that uses

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)