Formalizing the concurrency semantics of an LLVM fragment
No abstract available.
Related papers
- Monadic Interpreters for Concurrent Memory Models: Executable Semantics of a Concurrent Subset of LLVM IR CPP 2025
- K-LLVM: A Relatively Complete Semantics of LLVM IR ECOOP 2020
- Modular, compositional, and executable formal semantics for LLVM IR ICFP 2021
- Formalizing the LLVM intermediate representation for verified program transformations POPL 2012
- Semantics of (Resilient) X10 ECOOP 2014
- An Isabelle/HOL formalization of AProVE's termination method for LLVM IR CPP 2021
- An LLVM-based open-source compiler for NVIDIA GPUs PPoPP 2022
- Formal Semantics and Program Logics for a Fragment of OCaml ICFP 2025