Calvin Beck

Modular, compositional, and executable formal semantics for LLVM IR

2021 · Proceedings of the ACM on Programming Languages

This paper presents a novel formal semantics, mechanized in Coq, for a large, sequential subset of the LLVM IR. In contrast to previous approaches, which use relationally-specified operational semantics, this new semantics is based on …