ICFP/SPLASH 2025 (series) / SPLASH 2025 (series) / OOPSLA /
Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice
This program is tentative and subject to change.
Sat 18 Oct 2025 15:15 - 15:30 at Orchid East - Memory
We present the first thin-air free memory model that admits compiler optimisations that aggressively leverage knowledge from alias analysis, an assumption of freedom from undefined behaviour, and from the extrinsic choices of real implementations such as over-alignment. Our model has tooling support with state-of-the-art performance, executing a battery of tests orders of magnitude quicker than other executable thin-air free semantics. The model integrates with the C/C++ memory model through an exportable semantic dependency relation, it allows standard compilation mappings for atomics, and it matches all tests in the recently published desiderata for C/C++ from the ISO.
This program is tentative and subject to change.
Sat 18 OctDisplayed time zone: Perth change
Sat 18 Oct
Displayed time zone: Perth change
13:45 - 15:30 | |||
13:45 15mTalk | Compositional Symbolic Execution for the Next 700 Memory Models OOPSLA Andreas Lööw Imperial College London, Seung Hoon Park Imperial College London, Daniele Nantes-Sobrinho Imperial College London, Sacha-Élie Ayoun Imperial College London, Opale Sjöstedt Imperial College London, Philippa Gardner Imperial College London Pre-print | ||
14:00 15mTalk | Destination calculus: A linear λ-calculus for purely functional memory writes OOPSLA | ||
14:15 15mTalk | Divining Profiler Accuracy: An Approach to Approximate Profiler Accuracy Through Machine Code-Level Slowdown OOPSLA | ||
14:30 15mTalk | HeapBuffers: Why not just using a binary serialization format for your managed memory? OOPSLA Daniele Bonetta VU Amsterdam, Júnior Löff Università della Svizzera italiana, Matteo Basso Università della Svizzera italiana (USI), Walter Binder USI Lugano | ||
14:45 15mTalk | im2im: Automatically Converting In-Memory Image Representations using A Knowledge Graph Approach OOPSLA Fei Chen German Research Center for Artificial Intelligence (DFKI), Saarland University, Sunita Saha German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany, Manuela Schuler German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany; Saarland University, Saarbrücken, Germany, Philipp Slusallek DFKI, Germany, Tim Dahmen Aalen University, Aalen, Germany; German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany | ||
15:00 15mTalk | SafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races OOPSLA Reese Levine , Ashley Lee University of California, Santa Cruz, Neha Abbas University of California, Santa Cruz, Kyle Little University of Utah, Tyler Sorensen Microsoft Research and University of California at Santa Cruz | ||
15:15 15mTalk | Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice OOPSLA Jay Richards University of Kent, Daniel Wright University of Surrey, Simon Cooksey , Mark Batty University of Kent |