APLAS 2023
Sun 26 - Wed 29 November 2023 Taipei, Taiwan
Tue 28 Nov 2023 15:30 - 16:00 at Room 106 & 107, IIS - Verification Chair(s): Zhong Shao

Most of the existing work on verified compilation leaves unverified the translation of assembly programs into binary code in object file formats (e.g., the Executable and Linkable Format or ELF). The challenges of developing verified assemblers come from the intrinsic complexities in low-level assembling processes caused by the need to support different computer architectures and their details, such as encoding a large number of instructions and verifying its correctness. We present a framework that overcomes the above challenges. It works as a template which may be instantiated to generate verified assemblers for different architectures targeting ELF object files. For this, it is parameterized over the implementation and verification of architecture-dependent assembling processes through well-defined interfaces. By plugging the architecture-dependent parts into the template, we get complete verified assemblers. To manage the complexity in developing and verifying encoding of instructions, we integrate into our framework the CSLED framework for automatically generating verified instruction encoders and decoders from declarative instruction specifications. To show the effectiveness of our framework, we have applied it to generate verified assemblers for the complete X86 and RISC-V assembly languages in CompCert.

Towards a Framework for Developing Verified Assemblers for the ELF Format (main.pdf)553KiB

Tue 28 Nov

Displayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change

15:30 - 17:00
VerificationAPLAS 2023 at Room 106 & 107, IIS
Chair(s): Zhong Shao Yale University
15:30
30m
Talk
Towards a Framework for Developing Verified Assemblers for the ELF Format
APLAS 2023
Jinhua Wu Shanghai Jiao Tong University, Yuting Wang Shanghai Jiao Tong University, Meng Sun Shanghai Jiao Tong University, Xiangzhe Xu Purdue University, Yichen Song Shanghai Jiao Tong University
DOI File Attached
16:00
30m
Talk
Transport via Partial Galois Connections and Equivalences
APLAS 2023
Kevin Kappelmann Technical University of Munich
16:30
30m
Talk
Argument Reduction of Constrained Horn Clauses Using Equality Constraints
APLAS 2023
Ryo Ikeda University of Tokyo, Ryosuke Sato University of Tokyo, Naoki Kobayashi University of Tokyo