Automatic generation and validation of instruction encoders and decoders

DOI10.1007/978-3-030-81688-9_34zbMath1493.68223OpenAlexW3186771479MaRDI QIDQ832306

Jinhua Wu, Zhenguo Yin, Xiangzhe Xu, Peng-Fei 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

zbMATH Keywords

program synthesisproof synthesistranslation validationformalized instruction formatsverified parsing

Mathematics Subject Classification ID

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

Uses Software

• Coq
• z3
• CompCert

Cites Work

• Validating LR(1) Parsers
• Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars
• Verified, Executable Parsing
• A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture
• Bidirectional grammars for machine-code decoding and encoding

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