SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
Events (75 results)

All Languages are Dynamic

DLS 2023 When: Tue 24 Oct 2023 11:00 - 11:30 People: James Noble

… will be true: that all languages will be dynamic. …

All the Languages Together

OOPSLA When: Fri 27 Oct 2023 09:30 - 10:30 People: Amal Ahmed

… …

Rhombus: A New Spin on Macros without All the Parentheses

OOPSLA When: Thu 26 Oct 2023 12:12 - 12:30 People: Matthew Flatt, Taylor Allred, Nia Angle, Stephen De Gabrielle, Robert Bruce Findler, Jack Firth, Kiran Gopinathan, Ben Greenman, Siddhartha Kasivajhula, Alex Knauth, Jay McCarthy, Sam Phillips, Sorawee Porncharoenwase, Jens Axel Søgaard, Sam Tobin-Hochstadt

… and expressions. The Rhombus implementation demonstrates that all of these pieces can …

Exceptions all Over the Shop: Modular, Customizable, Language-independent Exception Handling Layer

SLE 2023 When: Mon 23 Oct 2023 09:00 - 09:30 People: Walter Cazzola, Luca Favalli

… …

Branching Compositional Data Transformations in jq, Visually

PAINT When: Mon 23 Oct 2023 09:30 - 10:00 People: Michael Homer

… invisibly, implicit output flattening obscures all these effects, and most users … filters, all the while common debugging techniques are also obstructed …

A silent semantics for isorecursive session types

ST30 When: Sun 22 Oct 2023 09:00 - 09:30 People: Janek Spaderna, Peter Thiemann, Vasco T. Vasconcelos

… Almost all formalizations of recursive session types rely on equirecursion because the explicit isomorphism to roll/unroll the recursive type is said to give rise to additional communication and synchronization. We examine …

Opening, Keynote: Bounded STL Model Checking for Hybrid Systems

FTSCS 2023 When: Sun 22 Oct 2023 09:15 - 10:30 People: Kyungmin Bae

… that continuously change over time. For hybrid systems, checking whether all

Creed for Speed: Comprehensive Infrastructure as Code Testing

CONFLANG23 When: Tue 24 Oct 2023 16:22 - 16:45 People: Daniel Sokolowski, David Spielmann, Guido Salvaneschi

… slow integration testing—if they test at all. As a result, even simple bugs …. ProTI mocks all cloud resources, replacing them with pluggable oracles that validate all resources’ configurations and a generator for realistic test inputs. We …

Toward Studying Example-based Live Programming in CS/SE Education

PAINT When: Mon 23 Oct 2023 09:00 - 09:30 People: Eva Krebs, Toni Mattis, Patrick Rein, Robert Hirschfeld

all three criteria by introducing concrete values, moving them as close …

Live & Local Schema Change: Challenge Problems

LIVE 2023 When: Mon 23 Oct 2023 11:00 - 11:30 People: Jonathan Edwards, Tomas Petricek, Tijs van der Storm

… and the code colocated with it. In all of these situations the problem …

CloudJIT: A Just-in-Time FaaS Optimizer (Work in Progress)

MPLR 2023 When: Sun 22 Oct 2023 10:15 - 10:30 People: Serhii Ivanenko, Rodrigo Bruno, Jovan Stevanovic, Luís Veiga, Vojin Jovanovic

… detects which functions will benefit from it the most, performs all prerequisite … that optimizing a small fraction of all functions positively affects a vast majority of all cold starts. …

Embark: a computational outliner for travel

LIVE 2023 When: Mon 23 Oct 2023 15:00 - 15:30 People: Paul Sonnentag, Alexander Obenauer, Geoffrey Litt

… short weekend trips to sprawling RV roadtrips, all within a single medium. More …

Unfolding State Changes via Live State-First Debugging

LIVE 2023 When: Mon 23 Oct 2023 16:00 - 16:30 People: Ruanqianqian (Lisa) Huang, Philip Guo, Sorin Lerner

… changes relate to code, all without requiring any logging or breakpoints. We …

Keeping the asm in Wasm – Running high-level languages on a low-level VM

DLS 2023 When: Tue 24 Oct 2023 14:30 - 15:00 People: Andreas Rossberg

… performance for them often requires every dirty trick from the books. Not all

Strongly-Typed Multi-View Stack-Based Computations

PPDP 2023 When: Mon 23 Oct 2023 14:00 - 14:30 People: Pieter Koopman, Mart Lubbers

… by all basic stack instructions and the functions implemented with those … is unchanged. However, standard typing restrictions impose that all function …

Mechanising Multiparty Session Types: A Sound and Complete Projection

ST30 When: Sun 22 Oct 2023 09:30 - 10:00 People: Marco Carbone, Dawit Tirore, Jesper Bengtson

… that given a global type and a role erases all details irrelevant to this role … expressive. All results have been mechanised in the Coq proof assistant …

Reverse Template Processing using Abstract Interpretation

SAS 2023 When: Sun 22 Oct 2023 14:30 - 15:00 People: Matthieu Lemerre

… Template languages transform tree-structured data into text. We study the reverse problem, transforming the template into a parser that returns all the tree …, exactness, or reduction, to reason about the precision and the recovery of all

The importance of facing outwards: why dynamic languages can and should address the world

DLS 2023 When: Tue 24 Oct 2023 09:30 - 10:00 People: Stephen Kell

… representation at all); enabling interaction with system objects symmetrically …

Welcome from the Chairs

MPLR 2023 When: Sun 22 Oct 2023 09:00 - 09:05 People: Rodrigo Bruno, Eliot Moss

… for presenting and discussing novel results in all aspects of managed programming …

Local-first at Actyx

PLF When: Tue 24 Oct 2023 14:30 - 15:00 People: Roland Kuhn, José Duarte

… -first fashion. The reasons span all of the above motivations, including data …

Embedding Quantitative Properties of Call-by-Name and Call-by-Value in a Unifying Framework

PPDP 2023 When: Sun 22 Oct 2023 11:00 - 12:30 People: Delia Kesner

… the inhabitation problem. In all these cases, explained and discussed in the talk …

Data-Dependent Confidentiality in DCR Graphs

PPDP 2023 When: Sun 22 Oct 2023 16:30 - 17:00 People: Eduardo Geraldo, João Costa Seco, Thomas T. Hildebrandt

… property, and transparency in all traces of DCRSec processes. …

Multi-Stage Vertex-Centric Programming for Agent-Based Simulations

GPCE 2023 When: Sun 22 Oct 2023 12:00 - 12:30 People: Zilu Tian

… In vertex-centric programming, users express a graph algorithm as a vertex program and specify the iterative behavior of a vertex in a ${compute}$ function, which is executed by all vertices in a graph in parallel, synchronously …

Nanopass Attribute Grammars

SLE 2023 When: Mon 23 Oct 2023 15:00 - 15:30 People: Nathan Ringo, Lucas Kramer, Eric Van Wyk

… grammars, by (i) identifying a collection of all language constructs and analyses … compositions of transformations to form nanopass compilers. The collection of all features …

Beehive SPIR-V Toolkit: A Composable and Functional API for Runtime SPIR-V Code Generation

VMIL When: Mon 23 Oct 2023 16:25 - 16:50 People: Juan Fumero, György Rethy, Athanasios Stratikopoulos, Nikos Foutris, Christos Kotselidis

… ecosystem. However, not all programming environments, runtime systems …

Closure Conversion in Little Pieces

PPDP 2023 When: Mon 23 Oct 2023 14:30 - 15:00 People: Zachary Sullivan, Paul Downen, Zena M. Ariola

… (IL) where all the properties of the source program are still known … these three approaches to closure conversion and optimizations thereof, by combining all

A Formal Framework to Measure the Incompleteness of Abstract Interpretations

SAS 2023 When: Sun 22 Oct 2023 12:00 - 12:30 People: Marco Campion, Caterina Urban, Mila Dalla Preda, Roberto Giacobazzi

… precise. Regrettably, as for all approximation methods, the presence of false-alarms …-metric, which can be defined on all domains equipped with a pre-order relation …

Don’t Trust Your Profiler: An Empirical Study on the Precision and Accuracy of Java Profilers (Poster Abstract)

MPLR 2023 When: Sun 22 Oct 2023 18:10 - 18:50 People: Humphrey Burchell, Octave Larose, Sophie Kaleba, Stefan Marr

… Flight Recorder, JProfiler, perf, and YourKit, which are all actively maintained. We …. Unfortunately, this is not true for all benchmarks, which suggests …

Don’t Trust Your Profiler: An Empirical Study on the Precision and Accuracy of Java Profilers

MPLR 2023 When: Sun 22 Oct 2023 14:45 - 15:07 People: Humphrey Burchell, Octave Larose, Sophie Kaleba, Stefan Marr

… Flight Recorder, JProfiler, perf, and YourKit, which are all actively maintained … method. Unfortunately, this is not true for all benchmarks, which suggests …

Termination in Concurrency, Revisited

PPDP 2023 When: Mon 23 Oct 2023 09:30 - 10:00 People: Joseph Paulus, Daniele Nantes-Sobrinho, Jorge A. Pérez

… Termination (also known as \emph{strong normalization}) is a fundamental property in sequential programming models. A process is terminating if all its reduction sequences are of finite length. Termination is also important …

Evolving a configuration language in place at Google scale

CONFLANG23 When: Tue 24 Oct 2023 11:45 - 12:07 People: Marcos Lara-Reinhold

… GCL, an internal configuration language used at Google, was created in 2003, and after a few years of improvements it got to a point where it was impossible to change it. Its usage had grown too fast and users were depending on nearly all

An Executable Semantics for Faster Development of Optimizing Python Compilers

SLE 2023 When: Mon 23 Oct 2023 09:30 - 10:00 People: Olivier Melancon, Marc Feeley, Manuel Serrano

… boxing and unboxing, and function calls which are all known sources of overhead. We …

Seamless Code Generator Synchronization in the Composition of Heterogeneous Modeling Languages

SLE 2023 When: Tue 24 Oct 2023 12:00 - 12:20 People: Nico Jansen, Bernhard Rumpe

… techniques for code generation is essential to enable language composition in all

Generalized Program Sketching by Abstract Interpretation and Logical Abduction

SAS 2023 When: Sun 22 Oct 2023 14:00 - 14:30 People: Aleksandar S. Dimovski

… and the weakest among all possible that guarantee the validity of assertions …

Verifying Infinitely Many Programs at Once

SAS 2023 When: Tue 24 Oct 2023 11:00 - 12:00 People: Loris D'Antoni

… , a property φ, one needs to verify that all programs in the search space …

A reference GLL implementation

SLE 2023 When: Mon 23 Oct 2023 14:00 - 14:30 People: Adrian Johnstone

… form.

This paper presents a reference GLL implementation shorn of all

Sharing Trees and Contextual Information: Re-imagining Forwarding in Attribute Grammars

SLE 2023 When: Mon 23 Oct 2023 14:30 - 15:00 People: Lucas Kramer, Eric Van Wyk

… and limited language extensibility. This avoided all instances in which …

Evaluating YJIT’s Performance in a Production Context: A Pragmatic Approach

MPLR 2023 When: Sun 22 Oct 2023 11:00 - 11:22 People: Maxime Chevalier-Boisvert, Takashi Kokubun, Noah Gibbs, Si Xing "Alan" Wu, Aaron Patterson, Jemma Issroff

… and warm-up time.

On all of our benchmarks, YJIT is able to consistently …

Symbolic transformation of expressions in modular arithmetic

SAS 2023 When: Mon 23 Oct 2023 11:00 - 11:30 People: Jérôme Boillot, Jerome Feret

… the soundness of the transformation.

All these methods have been incorporated within …

Scaling up Roundoff Analysis of Functional Data Structure Programs

SAS 2023 When: Mon 23 Oct 2023 15:00 - 15:30 People: Anastasia Isychev, Eva Darulova

… and loops over these. To analyze such programs today, all data structure …

Boosting Multi-Neuron Convex Relaxation for Neural Network Verification

SAS 2023 When: Sun 22 Oct 2023 16:30 - 17:00 People: Xuezhou Tang, Ye Zheng, Jiaxiang Liu

… approximate the volumes of convex hulls for all group candidates, without calculating …

Unified Shared Memory: Friend or Foe? Understanding the Implications of Unified Memory on Managed Heaps

MPLR 2023 When: Sun 22 Oct 2023 16:22 - 16:45 People: Juan Fumero, Florin Blanaru, Athanasios Stratikopoulos, Steve Dohrmann, Sandhya Viswanathan, Christos Kotselidis

… Virtual Machine's object heap in unified memory which is visible to all

Cross-Level Debugging for Static Analysers

SLE 2023 When: Tue 24 Oct 2023 09:30 - 10:00 People: Mats Van Molle, Bram Vandenbogaerde, Coen De Roover

… , meaning that its answers account for all possible program behavior …

Mutual Refinements of Context-Free Language Reachability

SAS 2023 When: Tue 24 Oct 2023 12:00 - 12:30 People: Shuo Ding, Qirun Zhang

… straightforwardly intersect all reachability results $bigcap_{i=1}^n P_i$ to achieve …

Goal-Directed Abstract Interpretation and Event-Driven Frameworks

SAS 2023 When: Sun 22 Oct 2023 09:05 - 10:05 People: Bor-Yuh Evan Chang

… it to be arbitrary or attempt to eagerly specify all possible callback control flow …

programmingLanguage as Language;

Onward! Essays When: Wed 25 Oct 2023 16:45 - 17:30 People: James Noble, Robert Biddle

… , programming languages are “human” languages above all.

Programming languages …: conversations, stories, and documents of all kinds. Language supports both cognitive …

Whither Problem-Solving Environments?

Onward! Essays When: Thu 26 Oct 2023 14:45 - 15:30 People: Matthew Dinmore

… During the 1990s and first decade of the 2000s, problem-solving environments (PSEs) were a topic of research among a community with the vision to create software systems “with all of the computational facilities necessary to solve a target …

Pushing the Limit of 1-Minimality of Language-Agnostic Program Reduction

OOPSLA When: Wed 25 Oct 2023 12:12 - 12:30 People: Zhenyang Xu, Yongqiang Tian, Mengxiao Zhang, Gaosen Zhao, Yu Jiang, Chengnian Sun

… problem: finding the globally minimal program is usually infeasible. Thus all … transformations in all existing program reducers including SPRs are not diverse … the state-of-the-art language-agnostic program reducer Perses in size in all

Exploiting the Sparseness of Control-Flow and Call Graphs for Efficient and On-Demand Algebraic Program Analysis

OOPSLA When: Thu 26 Oct 2023 16:18 - 16:36 People: Giovanna Kobus Conrado, Amir Kafshdar Goharshady, Kerim Kochekov, Yun Chen Tsai, Ahmed Khaled Zaher

… expression $\regexp$ capturing all program paths of interest. In case of intraprocedural analysis, $\regexp$ models all paths from $s$ to $t$, whereas in the interprocedural case it models all interprocedurally-valid paths, i.e.~paths that go …

Greedy Implicit Bounded Quantification

OOPSLA When: Thu 26 Oct 2023 14:00 - 14:18 People: Chen Cui, Shengyi Jiang, Bruno C. d. S. Oliveira

… to kernel $F_{\le}$, showing that all the well-typed kernel $F_{\le}$ programs can … system is shown to be sound, complete, and decidable. All the results have been …

User-Customizable Transpilation of Scripting Languages

OOPSLA When: Fri 27 Oct 2023 17:12 - 17:30 People: Bo Wang, Aashish Kolluri, Ivica Nikolić, Teodora Baluta, Prateek Saxena

… of a given program, but not necessarily for all parts of it. We propose a new …%$ translation accuracy and so it outperforms all existing translators (both handcrafted …

Concrete Type Inference for Code Optimization using Machine Learning with SMT Solving

OOPSLA When: Wed 25 Oct 2023 11:36 - 11:54 People: Fangke Ye, Jisheng Zhao, Jun Shirako, Vivek Sarkar

… of concrete type options, while also including a catch-all untyped version … speedup across all benchmarks compared to standard Python, when using 3) is $26.4 …

Accelerating Fuzzing through Prefix-Guided Execution

OOPSLA When: Fri 27 Oct 2023 11:54 - 12:12 People: Shaohua Li, Zhendong Su

… Coverage-guided fuzzing is one of the most effective approaches for discovering software defects and vulnerabilities. It executes all mutated tests from seed inputs to expose coverage-increasing tests. However, executing all mutated tests …

Adventure of a Lifetime: Extract Method Refactoring for Rust

OOPSLA When: Fri 27 Oct 2023 16:18 - 16:36 People: Sewen Thy, Andreea Costea, Kiran Gopinathan, Ilya Sergey

… well-studied and widely used in practice automated refactorings, featured in all major IDEs for all popular programming languages, implementing it soundly …

Algebro-geometric Algorithms for Template-Based Synthesis of Polynomial Programs

OOPSLA When: Wed 25 Oct 2023 14:54 - 15:12 People: Amir Kafshdar Goharshady, S. Hitarth, Fatemeh Mohammadi, Harshit Jitendra Motwani

… imperative programs with real variables, i.e. imperative programs in which all … and not at all applicable to this use-case.

In contrast, our main contribution …

Partial Gradual Dependent Type Theory

Student Research Competition When: Thu 26 Oct 2023 18:23 - 18:36 People: Zhan Shi

… , while all of them are important and desirable.

This ongoing work proposes …

Trustworthy Formal Natural Language Specifications

Onward! Papers When: Wed 25 Oct 2023 15:00 - 15:30 People: Colin Gordon, Sergey Matskevich

… formalizations; all can be translated correctly with a modest lexicon with only minor …

Aliasing Limits on Translating C to Safe Rust

OOPSLA When: Fri 27 Oct 2023 16:00 - 16:18 People: Mehmet Emre, Peter Boyland, Aesha Parekh, Ryan Schroeder, Kyle Dewey, Ben Hardekopf

… % to 21% of all pointers). …

MemPerf: Profiling Allocator-Induced Performance Slowdowns

OOPSLA When: Fri 27 Oct 2023 12:12 - 12:30 People: Jin Zhou, Sam Silvestro, Steven (Jiaxun) Tang, Hanmei Yang, Hongyu Liu, Guangming Zeng, Bo Wu, Cong Liu, Tongping Liu

… . For slow memory accesses, MemPerf utilizes a top-down approach to identify all

AtomiS: Data-Centric Synchronization Made Practical

OOPSLA When: Fri 27 Oct 2023 11:54 - 12:12 People: Hervé Paulino, Ana Almeida Matos, Jan Cederquist, Marco Giunti, João Batista Pereira Matos Júnior, António Ravara

… that are consistent with the specification, and performs code generation for all

Fat Pointers for Temporal Memory Safety of C

OOPSLA When: Fri 27 Oct 2023 14:18 - 14:36 People: Jie Zhou, John Criswell, Michael Hicks

… solutions retrofit temporal memory safety to C, but they all either incur high …

A Pretty Expressive Printer

OOPSLA When: Wed 25 Oct 2023 16:18 - 16:36 People: Sorawee Porncharoenwase, Justin Pombrio, Emina Torlak

… expressive than all pretty printers in the literature and provably minimizes …

Toward Programming Languages for Reasoning -- Humans, Symbolic Systems, and AI Agents

Onward! Papers When: Wed 25 Oct 2023 14:30 - 15:00 People: Mark Marron

… resolved, enables us to make radical progress in all of these areas.

Our …

Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic

OOPSLA When: Fri 27 Oct 2023 16:54 - 17:12 People: Jaehwang Jung, Janggun Lee, Jaemin Choi, Jaewoo Kim, Sunho Park, Jeehoon Kang

… the Coq mechanization of all our results in the Iris separation logic framework. …

Reference Capabilities for Flexible Memory Management

OOPSLA When: Thu 26 Oct 2023 11:00 - 11:18 People: Ellen Arvidsson, Elias Castegren, Sylvan Clebsch, Sophia Drossopoulou, James Noble, Matthew J. Parkinson, Tobias Wrigstad

… Verona is a concurrent object-oriented programming language that organises all the objects in a program into a forest of isolated regions. Memory is managed locally for each region, so programmers can control a program's memory use …

Asparagus: Automated Synthesis of Parametric Gas Upper-Bounds for Smart Contracts

OOPSLA When: Wed 25 Oct 2023 11:00 - 11:18 People: Zhuo Cai, Soroush Farokhnia, Amir Kafshdar Goharshady, S. Hitarth

… such consensus necessarily requires every node on the network to execute all …. To avoid this, following Ethereum, virtually all programmable blockchains have …

Clearing the Trail: Motivations for Maintenance Work in Open Source

Student Research Competition When: Thu 26 Oct 2023 17:43 - 17:56 People: Katrina Wilson

… Almost all software development projects rely heavily on open-source infrastructure. For instance, 94% of respondents surveyed in the 2017 GitHub Open Source Survey reported using open source software (OSS) professionally. Despite …

Building Dynamic System Call Sandbox with Partial Order Analysis

OOPSLA When: Thu 26 Oct 2023 16:54 - 17:12 People: Quan Zhang, Chijin Zhou, Yiwen Xu, Zijing Yin, Mingzhe Wang, Zhuo Su, Chengnian Sun, Yu Jiang, Jiaguang Sun

… with program execution. Thus, they need to permit all system calls required for program …

Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols

OOPSLA When: Fri 27 Oct 2023 14:54 - 15:12 People: Orr Tamir, Marcelo Taube, Kenneth L. McMillan, Sharon Shoham, Jon Howell, Guy Gueta, Mooly Sagiv

all spurious counter-models, making the approach complete.

We applied …

Synthesizing Precise Static Analyzers for Automatic Differentiation

OOPSLA When: Thu 26 Oct 2023 14:36 - 14:54 People: Jacob Laurel, Siyuan Brant Qian, Gagandeep Singh, Sasa Misailovic

… computations for Automatic Differentiation in a way that abstracts all

Proof Automation for Linearizability in Separation Logic

OOPSLA When: Fri 27 Oct 2023 16:36 - 16:54 People: Ike Mulder, Robbert Krebbers

… -of-the-art tools such as Iris, FCSL, and Voila all require a form of interactive …

An Explanation Method for Models of Code

OOPSLA When: Wed 25 Oct 2023 11:54 - 12:12 People: Yu Wang, Ke Wang, Linzhang Wang

… -to-end fashion (i.e., including model prediction time); (2) the wheat that all

Improving Oracle-Guided Inductive Synthesis by Efficient Question Selection

OOPSLA When: Thu 26 Oct 2023 17:12 - 17:30 People: Ruyi Ji, Chaozhe Kong, Yingfei Xiong, Zhenjiang Hu

… if it is not only effective for reducing iterations but also efficient. However, all

Live Pattern Matching with Typed Holes

OOPSLA When: Fri 27 Oct 2023 11:18 - 11:36 People: Yongwei Yuan, Scott Guest, Eric Griffis, Hannah Potter, David Moon, Cyrus Omar

… conservatively about all possible hole
fillings. We develop a typed lambda …

Historia: Refuting Callback Reachability with Message-History Logics

OOPSLA When: Thu 26 Oct 2023 16:00 - 16:18 People: Shawn Meier, Sergio Mover, Gowtham Kaki, Bor-Yuh Evan Chang

… implementation or attempting to eagerly specify all possible callback control flow …