Semantic foundations of intermediate program representations
type: Dataset
description: An end-to-end guarantee of software correctness by formal verification must consider two sources of bugs. First, the verification tool must be correct. Second, programs are often verified at the source level, before being compiled. Hence, compilers should also be trustworthy. Verifiers and compilers' complexity is increasing. To simplify code analysis and manipulation, these tools rely on intermediate representations (IR) of programs, that provide structural and semantic properties. This thesis gives a formal, semantic account on IRs, so that they can also be leveraged in the formal proof of such tools. We first study a register-based IR of Java bytecode used in compilers and verifiers. We specify the IR generation by a semantic theorem stating what the transformation preserves, e.g. object initialization or exceptions, but also what it modifies and how, e.g. object allocation. We implement this IR in Sawja, a Java static analysis toolbench. Then, we study the Static Single Assignment (SSA) form, an IR widely used in modern compilers and verifiers. We implement and prove in Coq an SSA middle-end for the CompCert C compiler. For the proof of SSA optimizations, we identify a key semantic property of SSA, allowing for equational reasoning. Finally, we study the semantics of concurrent Java IRs. Due to instruction reorderings performed by the compiler and the hardware, the current definition of the Java Memory Model (JMM) is complex, and unfortunately formally flawed. Targetting x86 architectures, we identify a subset of the JMM that is intuitive and tractable in formal proofs. We characterize the reorderings it allows, and factor out a proof common to the IRs of a compiler.
identifier: NNT: 2012DENS0053
issued: 2026-05-08T04:24:59.539858
language: en
modified: 2026-05-08T04:24:59.539863
contact point: Organization
  fn: CCSD
keyword: certified-compilation
keyword: compilation-certifiee
keyword: formal-semantics
keyword: infoeu-reposemanticsdoctoralthesis
keyword: infoinfo-ohcomputer-science-csother-csoh
keyword: intermediate-representations
keyword: representations-intermediaires
keyword: semantique-formelle
keyword: theses
landing page: https://theses.hal.science/tel-00905442

Semantic foundations of intermediate program representations
type: Distribution
format: HTML
issued: 2026-05-08T04:24:59.543475
modified: 2026-05-08T04:24:59.528601
access URL: https://theses.hal.science/tel-00905442

test_moissonnage_selune
type: Agent