SPLASH 2023 (series) /
SPLASH 2023 Program
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
This program is tentative and subject to change.
Sun 22 OctDisplayed time zone: Lisbon change
Sun 22 Oct
Displayed time zone: Lisbon change
09:00 - 10:30 | |||
09:00 30mPaper | A Calculus of Delayed Reductions PPDP | ||
09:30 30mPaper | Typed Equivalence of Labeled Effect Handlers and Labeled Delimited Control Operators PPDP Kazuki Ikemori Tokyo Institute of Technology, Youyou Cong Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of Technology | ||
10:00 30mPaper | Comprehending queries over finite maps PPDP Wilmer Ricciotti University of Edinburgh, UK | ||
09:00 - 10:30 | |||
09:00 5m | Opening SAS Manuel Hermenegildo Technical University of Madrid (UPM) and IMDEA Software Institute, José Morales IMDEA Software Institute, Marc Chevalier | ||
09:05 60mKeynote | Goal-Directed Abstract Interpretation and Event-Driven FrameworksKeynote SAS | ||
10:05 30mTalk | A Product of Shape and Sequence Abstractions SAS Josselin Giet Ecole Normale Supérieure, Félix Ridoux Univ Rennes / IMDEA Software Institute, Xavier Rival Inria; ENS; CNRS; PSL University | ||
09:00 - 10:30 | |||
09:00 5mDay opening | Welcome from the organizers MPLR Eliot Moss University of Massachusetts Amherst | ||
09:05 55mKeynote | Is Wasm becoming garbage? MPLR | ||
10:00 15mTalk | On the Applicability of Annotation-based Source Code Modification in Kotlin MPLR Daniel Pfeffer Institute for System Software; Johannes Kepler University Linz, Austria, Markus Weninger Institute for System Software; Johannes Kepler University Linz, Austria | ||
10:15 15mTalk | CloudJIT: a Just-in-Time FaaS Optimizer MPLR Serhii Ivanenko INESC-ID / Técnico, ULisboa, Rodrigo Bruno INESC-ID / Técnico, ULisboa, Jovan Stevanovic Oracle Labs, Luís Veiga INESC-ID, IST, ULisboa, Vojin Jovanovic Oracle Labs | ||
09:00 - 10:30 | |||
09:15 75mTalk | Opening, Keynote: Bounded STL Model Checking for Hybrid Systems FTSCS Kyungmin Bae POSTECH | ||
09:00 - 10:30 | |||
09:00 30mTalk | A silent semantics for isorecursive session types ST30 Janek Spaderna University of Freiburg, Germany, Peter Thiemann University of Freiburg, Germany, Vasco T. Vasconcelos LASIGE, University of Lisbon | ||
09:30 30mTalk | Mechanising Multiparty Session Types: A Sound and Complete Projection ST30 Marco Carbone IT University of Copenhagen | ||
10:00 30mTalk | The Concurrent Calculi Formalisation Benchmark ST30 Marco Carbone IT University of Copenhagen, David Castro-Perez University of Kent, Francisco Ferreira Royal Holloway, University of London, Lorenzo Gheri University of Oxford, Frederik Krogsdal Jacobsen , Alberto Momigliano Università degli Studi di Milano, Luca Padovani University of Camerino, Alceste Scalas Technical University of Denmark, Martin Vassor Imperial College London, Nobuko Yoshida University of Oxford | ||
10:30 - 11:00 | |||
11:00 - 12:30 | |||
11:00 90mTalk | Embedding Quantitative Properties of Call-by-Name and Call-by-Value in a Unified Framework PPDP Delia Kesner Université Paris Cité - CNRS - IRIF; Institut Universitaire de France | ||
11:00 - 12:30 | |||
11:00 30mTalk | How fitting is your abstract domain? SAS Roberto Giacobazzi University of Arizona, Isabella Mastroeni University of Verona, Italy, Elia Perantoni University of Verona | ||
11:30 30mTalk | Domain Precision in Galois Connection-less Abstract Interpretation SAS | ||
12:00 30mTalk | A Formal Framework to Measure the Incompleteness of Abstract Interpretations SAS Marco Campion INRIA & École Normale Supérieure | Université PSL, Paris, Caterina Urban INRIA & École Normale Supérieure | Université PSL, Mila Dalla Preda University of Verona, Roberto Giacobazzi University of Arizona | ||
11:00 - 12:30 | |||
11:00 22mTalk | Evaluating YJIT’s Performance in a Production Context: A Pragmatic Approach MPLR Maxime Chevalier-Boisvert Shopify, Takashi Kokubun Shopify, Noah Giibbs Shopify, Si Xing "Alan" Wu Shopify, Aaron Patterson Shopify, Jemma Issroff Shopify | ||
11:22 22mTalk | CacheIR: The Benefits of a Structured Representation for Inline Caches MPLR Jan de Mooij Mozilla, Matthew Gaudet Mozilla, Iain Ireland Mozilla, Nathan Henderson University of Alberta, Jose Nelson Amaral University of Alberta | ||
11:45 22mTalk | Diagnosing Compiler Performance by Comparing Optimization Decisions MPLR | ||
12:07 22mTalk | Morello MicroPython: A Python Interpreter for CHERI MPLR Duncan Lowther School of Computing Science, University of Glasgow, Dejice Jacob University of Glasgow, UK, Jeremy Singer University of Glasgow DOI Pre-print | ||
11:00 - 12:30 | |||
11:00 30mTalk | Probabilistic Risk Assessment of an Obstacle Detection System for GoA 4 Freight Trains FTSCS | ||
11:30 30mTalk | Solving Queries for Boolean Fault Tree Logic via Quantified SAT FTSCS Caz Saaltink , Stefano M. Nicoletti , Matthias Volk , Ernst Moritz Hahn , Marielle Stoelinga University of Twente and Radboud University, Nijmegen | ||
12:00 30mTalk | Symbolic analysis by using folding narrowing with irreducibility and SMT constraints FTSCS | ||
11:00 - 12:30 | ST30 Day 1 Session 2 - Invited talkST30 at Room XIII Chair(s): Vasco T. Vasconcelos LASIGE, University of Lisbon | ||
11:00 90mTalk | Beyond Types for Dyadic Interaction ST30 Nobuko Yoshida University of Oxford | ||
11:00 - 12:30 | |||
11:00 30mTalk | Diagrammatic notations for interactive theorem proving HATRA Link to publication | ||
11:30 30mTalk | Exploratory Study on Multi-User Program Synthesis: A Multi-Wizard Approach HATRA | ||
12:00 30mTalk | Latte: Lightweight Aliasing Tracking for Java HATRA Conrad Zimmerman Brown University, Catarina Gamboa Carnegie Mellon University and LASIGE, University of Lisbon, Alcides Fonseca LASIGE, University of Lisbon, Jonathan Aldrich Carnegie Mellon University Link to publication | ||
12:30 - 14:00 | |||
14:00 - 15:30 | |||
14:00 90mTalk | Coq: the world's best macro assembler? PPDP Andrew Kennedy Facebook London, Nick Benton Microsoft Research, Cambridge, Jonas Jensen Semmle, Pierre-Evariste Dagand IRIF / CNRS | ||
14:00 - 15:30 | |||
14:00 30mTalk | Generalized Program Sketching by Abstract Interpretation and Logical Abduction SAS Aleksandar S. Dimovski Mother Teresa University, Skopje | ||
14:30 30mTalk | Reverse Template Processing using Abstract Interpretation SAS Matthieu Lemerre Université Paris-Saclay - CEA LIST | ||
15:00 30mTalk | BREWasm: A General Static Binary Rewriting Framework for WebAssembly SAS Shangtong Cao Beijing University of Posts and Telecommunications, Ningyu He Peking University, Yao Guo Peking University, Haoyu Wang Huazhong University of Science and Technology | ||
14:00 - 15:30 | |||
14:00 22mTalk | A Multifaceted Memory Analysis of Java Benchmarks MPLR Orion Papadakis The University of Manchester, Andreas Andronikakis The University of Manchester, Nikos Foutris The University of Manchester, Michail Papadimitriou OctoML, Athanasios Stratikopoulos The University of Manchester, Foivos S. Zakkak Red Hat, Inc., Polychronis Xekalakis Nvidia, Christos Kotselidis Pierer Innovation / The University of Manchester | ||
14:22 22mTalk | Improving Garbage Collection Observability with Performance Tracing MPLR Claire Huang Australian National University, Stephen M. Blackburn Google, Australian National University, Zixian Cai Australian National University DOI Media Attached | ||
14:45 22mTalk | Don't Trust Your Profiler: An Empirical Study on the Precision and Accuracy of Java Profilers MPLR Humphrey Burchell University of Kent, Octave Larose University of Kent, Sophie Kaleba University of Kent, Stefan Marr University of Kent DOI Pre-print | ||
15:07 22mTalk | Heap Size Adjustment with CPU Control MPLR Sanaz Tavakolisomeh University of Oslo, Marina Shimchenko Uppsala University, Erik Österlund Oracle, Sweden, Rodrigo Bruno INESC-ID / Técnico, ULisboa, Paulo Ferreira University of Oslo / INESC-ID, Tobias Wrigstad Uppsala University, Sweden | ||
14:00 - 15:30 | |||
14:00 30mTalk | Does Rust SPARK Joy? Safe Bindings from Rust to SPARK, Applied to the BBQueue Library FTSCS Aïssata Maiga , Cyrille Artho KTH Royal Institute of Technology, Sweden, Florian Gilcher , Yannick Moy AdaCore | ||
14:30 30mTalk | Formal Verification of a Mechanical Ventilator using UPPAAL FTSCS Jaime Cuartas Universidad del Valle, David Cortés , Joan S Betancourt , Jesus Aranda Universidad del Valle, Jose Garcia , Andres Valencia , James Ortiz Université de Namur | ||
15:00 30mTalk | Discussions, Closing FTSCS | ||
14:00 - 15:30 | |||
14:00 30mTalk | CAPABLE: A Mechanised Imperative Language with Native Multiparty Session Types ST30 Jan de Muijnck-Hughes University of Strathclyde, Cristian Urlea , Adriana Laura Voinea , Wim Vanderbauwhede University of Glasgow | ||
14:30 30mTalk | Complete Multiparty Session Type Projection with Automata ST30 | ||
15:00 30mTalk | Multiparty Reactive Sessions ST30 Ilaria Castellani INRIA Sophia Antipolis, France, Cinzia Di Giusto Université Côte d'Azur; CNRS, Jorge A. Pérez University of Groningen | ||
14:00 - 15:30 | |||
14:00 30mTalk | A pred-LL(*) Parsable Typed Higher-Order Macro System for Architecture Description Languages GPCE Christoph Hochrainer Technical University of Vienna, Andreas Krall Vienna University of Technology, Austria | ||
14:30 30mTalk | A Monadic Framework for Name Resolution in Multi-Phased Type Checkers GPCE Casper Bach Poulsen Delft University of Technology, Aron Zwaan Delft University of Technology, Paul Hübner Delft University of Technology | ||
15:00 30mTalk | PC report GPCE Amir Shaikhha University of Edinburgh | ||
14:00 - 15:30 | |||
14:00 30mTalk | Debugging Trait Errors as Logic Programs HATRA Link to publication | ||
14:30 30mTalk | Totally Live Programming with Hazel (Progress Report) HATRA Cyrus Omar University of Michigan, Andrew Blinn University of Michigan, David Moon University of Michigan Link to publication | ||
15:00 30mTalk | REVIS: An Error Visualization Tool for Rust HATRA Ruochen Wang University of California, San Diego, Molly MacLaren University of California, San Diego, Michael Coblenz University of California, San Diego Link to publication | ||
15:30 - 16:00 | |||
16:00 - 17:30 | |||
16:00 30mPaper | Type-directed Program Transformation for Constant-Time Enforcement PPDP | ||
16:30 30mPaper | Data-Dependent Confidentiality in DCR Graphs PPDP Eduardo Geraldo , João Costa Seco NOVA-LINCS; Nova University of Lisbon, Thomas T. Hildebrandt University of Copenhagen | ||
17:00 30mBreak | --- PPDP | ||
16:00 - 17:30 | |||
16:00 30mTalk | Quantum Constant Propagation SAS Yanbin Chen TUM School of Computation, Information and Technology, Technical University of Munich, Yannick Stade TUM School of Computation, Information and Technology, Technical University of Munich | ||
16:30 30mTalk | Boosting Multi-Neuron Convex Relaxation for Neural Network Verification SAS | ||
16:00 - 17:30 | |||
16:00 30mTalk | The Expressiveness of Session Types ST30 Jorge A. Pérez University of Groningen Pre-print | ||
16:30 30mTalk | What we learned from writing a book about session types ST30 | ||
17:00 30mTalk | So what's the difference between a session type and an ordinary type anyway? ST30 Frank Pfenning Carnegie Mellon University, USA | ||
16:00 - 17:30 | |||
16:00 45mTalk | Goals of the Luau Type System, Two Years On HATRA Link to publication | ||
16:45 45mMeeting | Discussion HATRA Michael Coblenz University of California, San Diego, Luke Church University of Cambridge | Lund University | Lark Systems, Jonathan Aldrich Carnegie Mellon University, Will Crichton Brown University | ||
Mon 23 OctDisplayed time zone: Lisbon change
Mon 23 Oct
Displayed time zone: Lisbon change
09:00 - 10:30 | |||
09:00 30mPaper | Multicompatibility for Multiparty-Session Composition PPDP Franco Barbanera , Mariangiola Dezani Università di Torino, Lorenzo Gheri University of Oxford, Nobuko Yoshida University of Oxford | ||
09:30 30mPaper | Termination in Concurrency, Revisited PPDP Joseph Paulus , Daniele Nantes-Sobrinho Imperial College London, Jorge A. Pérez University of Groningen | ||
10:00 30mPaper | Polymorphic Typestate for Session Types PPDP | ||
09:00 - 10:30 | |||
09:00 60mKeynote | Abstract Interpretation in Industry - Experience and Lessons LearnedKeynote SAS | ||
10:00 30mTalk | Lifting On-Demand Analysis to Higher-Order Languages SAS Daniel Schoepe Amazon, David Seekatz Unaffiliated, Ilina Stoilkovska Amazon, Sandro Stucki Amazon, Daniel Tattersall Amazon, US, Pauline Bolignano Amazon, Franco Raimondi Amazon, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon | ||
09:00 - 10:30 | |||
09:00 30mTalk | Toward Studying Example-based Live Programming in CS/SE Education PAINT Eva Krebs Hasso Plattner Institute (HPI), University of Potsdam, Germany, Toni Mattis University of Potsdam; Hasso Plattner Institute, Patrick Rein University of Potsdam; Hasso Plattner Institute, Robert Hirschfeld University of Potsdam; Hasso Plattner Institute | ||
09:30 30mTalk | Branching Compositional Data Transformations in jq, VisuallyRemote PAINT Michael Homer Victoria University of Wellington | ||
10:00 30mTalk | PescaJ: A projectional editor for Java featuring scattered code aggregation PAINT José Lopes Instituto Universitário de Lisboa (ISCTE-IUL), André L. Santos University Institute of Lisbon, Portugal | ||
09:00 - 10:30 | |||
09:00 30mTalk | Exceptions all Over the Shop: Modular, Customizable, Language-independent Exception Handling LayerResearch Paper SLE | ||
09:30 30mTalk | An Executable Semantics for Faster Development of Optimizing Python CompilersResearch Paper SLE Olivier Melancon Université de Montréal, Marc Feeley Université de Montréal, Manuel Serrano Inria; University of Côte d'Azur | ||
10:00 30mTalk | Adaptive Structural Operational SemanticsResearch Paper SLE Gwendal Jouneaux University of Rennes; Inria; IRISA, Damian Frölich University of Amsterdam, Olivier Barais University of Rennes; Inria; CNRS; IRISA, Benoit Combemale University of Rennes, Inria, CNRS, IRISA, Gurvan LE GUERNIC DGA MI & Université de Rennes 1, Gunter Mussbacher McGill University, L. Thomas van Binsbergen University of Amsterdam | ||
09:00 - 10:30 | |||
09:00 60mKeynote | (TBA) LIVE | ||
10:00 30mTalk | Live & Local Schema Change: Challenge Problems LIVE Jonathan Edwards Independent, Tomas Petricek Charles University, Tijs van der Storm CWI & University of Groningen DOI Pre-print | ||
09:00 - 10:30 | |||
09:00 10mDay opening | Welcome PLMW | ||
09:10 30mSocial Event | Ice Breaker PLMW | ||
09:40 50mTalk | Mentoring Talk 1 PLMW Nate Foster Cornell University | ||
09:00 - 10:30 | |||
09:00 30mTalk | Behavioural up/down casting for statically typed languages ST30 Lorenzo Bacchiani , Mario Bravetti Università di Bologna, Marco Giunti NOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa, João Mota NOVA School of Science and Technology, Antonio Ravara NOVA LINCS & FCT, NOVA University of Lisbon | ||
09:30 30mTalk | Session-Based Typechecking for Elixir Modules Using ElixirST ST30 | ||
10:00 30mTalk | A Semantic Framework for Automatic Composition of Decentralised Industrial Control Schemes ST30 | ||
09:00 - 10:30 | |||
09:00 30mTalk | Generating Constraint Programs for Variability Model Reasoning: A DSL and Solver-Agnostic Approach GPCE Camilo Correa Restrepo University of Paris 1 Pantheon-Sorbonne, Paris, France, Jacques Robin ESIEA, Paris, France, Raúl Mazo ENSTA Bretagne | ||
09:30 30mTalk | C2TACO: Lifting Tensor Code to TACO GPCE José Wesley De Souza Magalhães University of Edinburgh, Jackson Woodruff University of Edinburgh, Elizabeth Polgreen University of Edinburgh, Michael F. P. O'Boyle University of Edinburgh | ||
10:00 30mTalk | Generating Conforming Programs With Xsmith GPCE William G Hatch University of Utah, Pierce Darragh University of Utah, Sorawee Porncharoenwase University of Washington, Guy Watson University of Utah, Eric Eide University of Utah | ||
09:00 - 10:30 | |||
09:00 10mDay opening | Opening Remarks VMIL Andrea Rosà USI Lugano | ||
09:10 25mPaper | CHERI Performance Enhancement for a Bytecode Interpreter VMIL Duncan Lowther School of Computing Science, University of Glasgow, Dejice Jacob University of Glasgow, UK, Jeremy Singer University of Glasgow DOI Pre-print | ||
09:35 25mPaper | Revisiting Dynamic Dispatch for Modern Architectures VMIL Dave Mason Toronto Metropolitan University (formerly Ryerson University) | ||
10:00 15mShort-paper | Approximating Type Stability in the Julia JIT VMIL Artem Pelenitsyn Northeastern University | ||
10:15 15mShort-paper | Transpiling Slang Methods to C Functions: An Example of Static Polymorphism for Smalltalk VM Objects VMIL Tom Braun Hasso Plattner Institute, University of Potsdam, Germany, Marcel Taeumel University of Potsdam; Hasso Plattner Institute, Eliot Miranda Cadence Design Systems, Robert Hirschfeld University of Potsdam; Hasso Plattner Institute | ||
10:30 - 11:00 | |||
11:00 - 12:30 | |||
11:00 10mDay opening | OPENING LOPSTR | ||
11:10 60mKeynote | Unification Modulo Equational Theories in Languages with Binding Operators LOPSTR Maribel Fernandez King's College London | ||
12:10 20mShort-paper | Towards a Certified Proof Checker for Deep Neural Network Verification LOPSTR Remi Desmartin Heriot-Watt University, Omri Isac The Hebrew University of Jerusalem, Grant Passmore Imandra Inc., Kathrin Stark Heriot-Watt University, Guy Katz Hebrew University, Ekaterina Komandantskaya Heriot-Watt University, UK | ||
11:00 - 12:30 | |||
11:00 90mTalk | Unification modulo equational theories in languages with binding operators PPDP Maribel Fernandez King's College London | ||
11:00 - 12:30 | |||
11:00 30mTalk | Symbolic transformation of expressions in modular arithmetic SAS | ||
11:30 30mTalk | Polynomial Analysis of Modular Arithmetic SAS | ||
12:00 30mTalk | Octagons Revisited - Elegant Proofs and Simplified Algorithms SAS | ||
11:00 - 12:30 | |||
11:00 45mTalk | Periodic and Aperiodic Task Description Mechanisms in an FRP Language for Small-Scale Embedded Systems REBLS Kento Sogo Tokyo Institute of Technology, Yuta Tsuji Tokyo Institute of Technology, Sosuke Moriguchi Tokyo Institute of Technology, Takuo Watanabe Tokyo Institute of Technology | ||
11:45 45mTalk | Thorium: Verifiable, Dynamic, Reactive Software REBLS Kevin Baldor The University of Texas at San Antonio, Jianwei Niu University of Texas at San Antonio, Xiaoyin Wang University of Texas at San Antonio | ||
11:00 - 12:30 | |||
11:00 30mTalk | Visual Replacements: Cross-language Domain-specific Representations in Structured Editors PAINT Tom Beckmann Hasso Plattner Institute, Daniel Stachnik Hasso Plattner Institute, Jens Lincke University of Potsdam; Hasso Plattner Institute, Robert Hirschfeld University of Potsdam; Hasso Plattner Institute | ||
11:30 30mResearch paper | Game Engine Wizardry for Programming Mischief PAINT Riemer van Rozen CWI | ||
12:00 30mTalk | Transforming an internal textual DSL into a Blended Modelling Environment PAINT Aleandro Mifsud University of Amsterdam & Axini BV, Georgia Samaritaki University of Amsterdam, Ulyana Tikhonova Axini, Jouke Stoel Axini BV | ||
11:00 - 12:30 | |||
11:00 90mKeynote | SLE/GPCE Keynote SLE | ||
11:00 - 12:30 | |||
11:00 30mTalk | CodeProber: Live Compiler Exploration LIVE | ||
11:30 30mTalk | Language Model Agents Enable Semi-Formal Programming LIVE | ||
12:00 30mTalk | Lude - build video games quickly LIVE | ||
11:00 - 12:30 | |||
11:00 30mTalk | Mentoring Talk 2 PLMW Magnus Madsen Aarhus University | ||
11:30 60mPanel | PhD Panel PLMW | ||
11:00 - 12:30 | |||
11:00 30mTalk | Asynchronous and Synchronous Mixed Sessions ST30 | ||
11:30 30mTalk | Classical Processes in modern dress ST30 | ||
12:00 30mTalk | Labelled Tensor Types in Session Based Programming ST30 Luís Caires INESC-ID / Instituto Superior Tecnico, University of Lisbon | ||
11:00 - 12:30 | |||
11:00 60mKeynote | Keynote VMIL Shigeru Chiba The University of Tokyo | ||
12:30 - 14:00 | |||
14:00 - 15:30 | |||
14:00 35mResearch paper | A Reusable Machine-Calculus for Automated Resource Analyses LOPSTR | ||
14:35 35mResearch paper | A Logical Interpretation of Asynchronous Multiparty Compatibility LOPSTR Marco Carbone IT University of Copenhagen, Sonia Marin University of Birmingham, Carsten Schürmann IT University of Copenhagen | ||
15:10 20mShort-paper | Relational Solver for Java Generics Type System LOPSTR Petr Lozov Sain Petersburg State University, SPbGU, Dmitry Kosarev Saint-Petersburg State University, Dmitry Ivanov TomTom, Dmitri Boulytchev Saint Petersburg State University | ||
14:00 - 15:30 | |||
14:00 30mPaper | Strongly-Typed Multi-View Stack-Based Computations PPDP | ||
14:30 30mPaper | Closure Conversion in Little Pieces PPDP Zachary Sullivan University of Oregon, Paul Downen University of Massachusetts Lowell, Zena M. Ariola University of Oregon | ||
15:00 30mPaper | Additive Cellular Automata Graded-Monadically PPDP | ||
14:00 - 15:30 | |||
14:00 30mTalk | Error Invariants for Fault Localization via Abstract Interpretation SAS Aleksandar S. Dimovski Mother Teresa University, Skopje | ||
14:30 30mTalk | Error Localization for Sequential Effect Systems SAS | ||
15:00 30mTalk | Scaling up Roundoff Analysis of Functional Data Structure Programs SAS | ||
14:00 - 15:30 | |||
14:00 30mTalk | ComPOS: a DSL for Composing IoT Systems With Weak Connectivity REBLS | ||
14:30 30mTalk | Actix-Telepathy REBLS Phillip Wenig Hasso Plattner Institute, University of Potsdam, Thorsten Papenbrock Philipps-Universität Marburg | ||
15:00 30mTalk | Realizing Persistent Signals in JavaScript REBLS | ||
14:00 - 15:30 | |||
14:00 30mTalk | A Penny a Function: Towards Cost Transparent Cloud Programming PAINT Lukas Böhme Hasso Plattner Institute, University of Potsdam, Tom Beckmann Hasso Plattner Institute, Sebastian Baltes SAP SE & University of Adelaide, Robert Hirschfeld University of Potsdam; Hasso Plattner Institute | ||
14:30 30mTalk | Beginning Student Tables PAINT Samuel Maginot Indiana University Bloomington, Chung-chieh Shan Indiana University, Sam Tobin-Hochstadt Indiana University | ||
14:00 - 15:30 | |||
14:00 30mTalk | A reference GLL implementationResearch Paper SLE Adrian Johnstone Royal Holloway University of London, UK | ||
14:30 30mTalk | Sharing Trees and Contextual Information: Re-imagining Forwarding in Attribute GrammarsResearch Paper SLE Lucas Kramer University of Minnesota, Eric Van Wyk Department of Computer Science and Engineering, University of Minnesota, USA | ||
15:00 30mTalk | Nanopass Attribute GrammarsResearch Paper SLE Nathan Ringo University of Minnesota, Lucas Kramer University of Minnesota, Eric Van Wyk Department of Computer Science and Engineering, University of Minnesota, USA | ||
14:00 - 15:30 | |||
14:00 30mTalk | TypeCell: End-User Programming in Block-Based rich text documents LIVE Yousef El-Dardiry TypeCell | ||
14:30 30mTalk | Document-oriented programming based on edit history LIVE | ||
15:00 30mTalk | Unfolding State Changes via Live State-First Debugging LIVE Ruanqianqian (Lisa) Huang University of California, San Diego, Philip Guo University of California at San Diego, Sorin Lerner University of California at San Diego | ||
14:00 - 15:30 | |||
14:00 90mPanel | Career Panel PLMW | ||
14:00 - 15:30 | |||
14:00 30mTalk | Benchmarks for Multiparty Session Types ST30 | ||
14:30 30mTalk | Towards Session-Typed Consensus ST30 | ||
15:00 30mTalk | Using Event Structures to model Multiparty Session Types: results and open problems ST30 | ||
14:00 - 15:30 | |||
14:00 30mTalk | Multi-Stage Vertex-Centric Programming for Agent-Based Simulations GPCE Zilu Tian EPFL | ||
14:30 30mTalk | Crossover: Towards Compiler-enabled COBOL-C Interoperability GPCE Mart van Assen University of Twente, Manzi Aimé Ntagengerwa University of Twente, Ömer Faruk Sayilir University of Twente, Vadim Zaytsev University of Twente, Netherlands | ||
15:00 30mTalk | Partial Evaluation of Automatic Differentiation for Differential-Algebraic Equations Solvers GPCE Oscar Eriksson KTH Royal Institute of Technology, Viktor Palmkvist KTH Royal Institute of Technology, David Broman KTH Royal Institute of Technology | ||
14:00 - 15:30 | |||
14:00 25mPaper | Debugging Dynamic Language Features in a Multi-Tier Virtual Machine VMIL Anmolpreet Singh Indian Institute of Technology Mandi, Aayush Sharma Indian Institute of Technology Mandi, Meetesh Kalpesh Mehta Indian Institute of Technology Bombay, Manas Thakur Indian Institute of Technology Bombay | ||
14:25 25mPaper | Array Bytecode Support in MicroJIT VMIL Shubham Verma University of New Brunswick, Harpreet Kaur University of New Brunswick, Kenneth Kent University of New Brunswick, Marius Pirvu IBM | ||
14:50 25mPaper | Hybrid Execution: Combining Ahead-of-Time and Just-in-Time Compilation VMIL Christoph Pichler Johannes Kepler University Linz, Paley Li Oracle, Roland Schatz Johannes Kepler University Linz, Hanspeter Mössenböck JKU Linz | ||
15:15 15mShort-paper | Extraction of Virtual Machine Execution Traces VMIL | ||
15:30 - 16:00 | |||
16:00 - 17:30 | |||
16:00 35mResearch paper | A Rule-Based Approach for Designing and Composing Abstract Domains LOPSTR Daniel Jurjo Rivas IMDEA Software Institute and T.U. of Madrid (UPM), José Morales IMDEA Software Institute, Pedro López-García IMDEA Software Institute, Manuel Hermenegildo Technical University of Madrid (UPM) and IMDEA Software Institute | ||
16:35 35mResearch paper | Design Datalog Templates for Synthesizing Bidirectional Programs from Tabular Examples LOPSTR Bach Nguyen Trong , Kanae Tsushima National Institute of Informatics, Japan, Zhenjiang Hu Peking University | ||
17:10 10mAwards | Best Paper Award LOPSTR | ||
16:00 - 17:30 | |||
16:00 30mPaper | Intuitionistic Metric Temporal Logic PPDP Luiz de Sá , Bernardo Toninho NOVA-LINCS; Nova University of Lisbon, Frank Pfenning Carnegie Mellon University, USA | ||
16:30 30mPaper | stablekanren: Integrating Stable Model Semantics with miniKanren PPDP | ||
17:00 30mBreak | Closing of PPDP PPDP | ||
16:00 - 17:30 | |||
16:00 60mKeynote | Building Trust and Safety in Artificial Intelligence with Abstract InterpretationKeynote SAS | ||
17:00 30mAwards | Radhia Cousot Award and PC report SAS C: Manuel Hermenegildo Technical University of Madrid (UPM) and IMDEA Software Institute, C: José Morales IMDEA Software Institute | ||
16:00 - 17:30 | |||
16:00 30mTalk | Automated extraction of grammar optimization rule configurations in a metamodel-grammar co-evolution scenarioResearch Paper SLE Weixing Zhang Chalmers | University of Gothenburg, Regina Hebig Chalmers University of Technology & University of Gothenburg, Daniel Strüber Chalmers | University of Gothenburg / Radboud University, Jan-Philipp Steghöfer XITASO GmbH IT & Software Solutions Pre-print | ||
16:30 30mTalk | Reuse and Automated Integration of Recommenders for Modelling LanguagesResearch Paper SLE Lissette Almonte Universidad Autónoma de Madrid, Antonio Garmendia Universidad Autónoma de Madrid, Esther Guerra Universidad Autónoma de Madrid, Juan de Lara Autonomous University of Madrid Pre-print | ||
17:00 30mTalk | GPT-3-Powered Type Error Debugging: Investigating the Use of Large Language Models for Code RepairResearch Paper SLE Francisco Ribeiro HASLab/INESC TEC & Universidade do Minho, José Nuno Macedo University of Minho, Kanae Tsushima National Institute of Informatics, Japan, Rui Abreu Faculty of Engineering, University of Porto, João Saraiva University of Minho, Portugal | ||
16:00 - 17:30 | |||
16:00 30mTalk | Embark: a computational outliner for travel LIVE | ||
16:30 30mTalk | PAW: a programmable and visual audio workstation LIVE | ||
17:00 30mTalk | CellPond: Spatial programming without escape LIVE Lu Wilson tldraw | ||
16:00 - 17:30 | |||
16:00 10mDay closing | Wrap-up PLMW | ||
16:10 10mTalk | SIGPLAN-M Introduction PLMW | ||
16:20 70mSocial Event | Mentoring Sessions PLMW | ||
16:00 - 17:30 | |||
16:00 90mPanel | Future Directions for Session Types ST30 Stephanie Balzer Carnegie Mellon University, Luís Caires INESC-ID / Instituto Superior Tecnico, University of Lisbon, Ornela Dardha University of Glasgow, Raymond Hu Queen Mary University of London | ||
16:00 - 17:30 | |||
16:00 30mTalk | Virtual Domain Specific Languages via Embedded Projectional Editing GPCE | ||
16:30 30mTalk | Unleashing the Power of Implicit Feedback in Software Product Lines: Benefits ahead GPCE Raul Medeiros University of the Basque Country (UPV/EHU), Oscar Diaz University of the Basque Country, Spain, David Benavides Universidad de Sevilla | ||
17:00 30mTalk | Automatically Generated Supernodes for AST Interpreters Improve Virtual-machine Performance GPCE Matteo Basso Università della Svizzera italiana (USI), Switzerland, Daniele Bonetta Oracle Labs, Walter Binder USI Lugano | ||
16:00 - 17:30 | |||
16:00 25mPaper | Collecting Garbage on the Blockchain VMIL Luc Bläser DFINITY Foundation, Claudio Russo Microsoft Research, Ulan Degenbaev Google, Omer S. Agacan Indiana University, Gabor Greif DFINITY, Jason Ibrahim DFINITY Foundation | ||
16:25 25mPaper | Beehive SPIR-V Toolkit: A Composable and Functional API for Runtime SPIR-V Code Generation VMIL Juan Fumero University of Manchester, UK, György Rethy ETH Zurich, Athanasios Stratikopoulos The University of Manchester, Nikos Foutris The University of Manchester, Christos Kotselidis Pierer Innovation / The University of Manchester DOI Pre-print | ||
16:50 25mPaper | Gigue: A JIT Code Binary Generator for Hardware Testing VMIL Quentin DUCASSE Lab-STICC, Pascal Cotret Lab-STICC CNRS UMR 6285, ENSTA Bretagne, Loïc Lagadec Lab-STICC CNRS UMR 6285, ENSTA Bretagne | ||
17:15 10mDay closing | Closing Remarks VMIL Andrea Rosà USI Lugano | ||
Tue 24 OctDisplayed time zone: Lisbon change
Tue 24 Oct
Displayed time zone: Lisbon change
09:00 - 10:30 | |||
09:00 60mKeynote | On-The-Fly Verification via Incremental, Interactive Abstract Interpretation with CiaoPP and VeriFly LOPSTR Manuel Hermenegildo Technical University of Madrid (UPM) and IMDEA Software Institute | ||
10:00 30mResearch paper | A Term Matching Algorithm and Substitution Generality LOPSTR Marija Kulaš Fernuniversität in Hagen | ||
09:00 - 10:30 | |||
09:00 60mKeynote | Verifying Infinitely Many Programs at OnceKeynote SAS | ||
10:00 30mTalk | Mutual Refinements of Context-Free Language Reachability SAS | ||
09:00 - 10:30 | |||
09:00 30mTalk | Temporal Breakpoints for Multiverse DebuggingResearch Paper SLE Matthias Pasquier Ertosgener, Ciprian Teodorov ENSTA Bretagne, Frédéric Jouault ERIS Team, ESEO , France, Matthias Brun , Luka Le Roux Lab-STICC CNRS UMR 6285, ENSTA Bretagne, Loïc Lagadec Lab-STICC CNRS UMR 6285, ENSTA Bretagne | ||
09:30 30mTalk | Cross-Level Debugging for Static AnalysersResearch Paper SLE Mats Van Molle Vrije Universiteit Brussel, Bram Vandenbogaerde Vrije Universiteit Brussel, Coen De Roover Vrije Universiteit Brussel | ||
10:00 30mResearch paper | Cascade: a Meta-Language for Change, Cause and EffectResearch Paper SLE Riemer van Rozen CWI | ||
09:00 - 10:30 | |||
09:00 15mDay opening | Welcome to IWACO! IWACO | ||
09:15 75mKeynote | Capture Tracking in Scala IWACO Martin Odersky EPFL | ||
09:00 - 10:30 | |||
09:00 10mDay opening | Introduction and Welcome Doctoral Symposium Michael Coblenz University of California, San Diego | ||
09:10 60mKeynote | Keynote: Jonathan Aldrich Doctoral Symposium Jonathan Aldrich Carnegie Mellon University | ||
10:10 20mTalk | Lightning talks Doctoral Symposium | ||
09:00 - 10:30 | |||
09:00 90mTalk | Keynote: Feeling the Local-First Elephant: A Roadmap, Hidden Gems, and New Puzzles from the Field PLF | ||
09:00 - 10:30 | |||
09:00 30mTalk | Is Polyglot Programming Really a Thing? DLS Walter Cazzola Università degli Studi di Milano | ||
09:30 30mTalk | The importance of facing outwards: why dynamic languages can and should address the world DLS Stephen Kell King's College London | ||
10:00 30mTalk | Going Static, Gradually: Semantic Soundness and Telling the Truth at Scale DLS Maxwell Heiber Meta | ||
09:00 - 10:30 | |||
09:00 22mTalk | Empirical Study of the Docker Smell Impact CONFLANG Thomas Durieux TU Delft | ||
09:22 22mTalk | Measuring Configuration in Code CONFLANG David Newell Google | ||
09:45 22mTalk | Yes, Configuring is Good, But Have You Ever Tried Justifying? CONFLANG Sébastien Mosser McMaster University, Corinne Pulgar École de Technologie Supérieure (ETS), Mireille Blay-Fornarino , Deesha Patel McMaster University, Canada, Aaron Loh McMaster University, Jean-Michel Bruel Université de Toulouse, France | ||
10:07 22mLive Q&A | Configuration analysis Q&A/Discussion CONFLANG | ||
10:30 - 11:00 | |||
11:00 - 12:30 | |||
11:00 35mResearch paper | Predicate Anti-unification in (Constraint) Logic Programming LOPSTR | ||
11:35 35mResearch paper | A Novel EGs-Based Framework for Systematic Propositional-Formula Simplification LOPSTR Jordina Francès de Mas University of St Andrews, St Andrews, UK, Juliana Bowles University of St Andrews, St Andrews, UK | ||
12:10 20mShort-paper | From Static to Dynamic Access Control Policies via Attribute-Based Category Mining LOPSTR | ||
11:00 - 12:30 | |||
11:00 30mTalk | ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses SAS | ||
11:30 30mTalk | Unconstrained Variable Oracles for Faster Static Analyses SAS Vincenzo Arceri University of Parma, Italy, Greta Dolcetti University of Parma - Department of Mathematical, Physical, and Computer Sciences, Enea Zaffanella University of Parma, Italy | ||
12:00 30mTalk | Modular Optimization-Based Roundoff Error Analysis of Floating-Point Programs SAS | ||
11:00 - 12:30 | |||
11:00 60mKeynote | SLE KeynoteKeynote SLE | ||
12:00 20mTalk | Seamless Code Generator Synchronization in the Composition of Heterogeneous Modeling LanguagesNew ideas / Vision paper SLE | ||
11:00 - 12:30 | |||
11:00 30mTalk | Borrow checking Hylo IWACO File Attached | ||
11:30 30mTalk | Degrees of Separation: A Flexible Type System for Data Race Prevention IWACO File Attached | ||
12:00 30mTalk | Latte: Lightweight Aliasing Tracking for Java IWACO Conrad Zimmerman Brown University, Catarina Gamboa Carnegie Mellon University and LASIGE, University of Lisbon, Alcides Fonseca LASIGE, University of Lisbon, Jonathan Aldrich Carnegie Mellon University Pre-print | ||
11:00 - 12:30 | |||
11:00 30mTalk | Large Language Models for Automated Program Repair Doctoral Symposium Francisco Ribeiro University of Minho & HASLab, INESCTEC | ||
11:30 30mTalk | Scaling up Program Synthesis to Efficient Algorithms Doctoral Symposium Ruyi Ji Peking University | ||
12:00 30mTalk | Transforming Ideas into Code: Visual Sketching for ML Development Doctoral Symposium Luis F. Gomes Carnegie Mellon University | ||
11:00 - 12:30 | |||
11:00 30mTalk | Collaborative offline-first applications in Education PLF Annette Bieniusa University of Kaiserslautern-Landau, Christopher Thyssen University of Kaiserslautern-Landau | ||
11:30 30mTalk | Local-first: experiments & lessons learned building TypeCell PLF Yousef El-Dardiry TypeCell | ||
12:00 30mTalk | Proposal: Versioned Collaborative Documents PLF Matthew Weidner Carnegie Mellon University | ||
11:00 - 12:30 | |||
11:00 30mTalk | All Languages are Dynamic DLS James Noble Research & Programming | ||
11:30 30mTalk | Are we Heading Towards a Dynamic Language Winter? DLS Maxime Chevalier-Boisvert Shopify | ||
12:00 30mTalk | Prof. Strangelove or: How I Learned to Stop Worrying and Love Dynamic Languages DLS Jan Vitek Northeastern University | ||
11:00 - 12:30 | |||
11:00 22mTalk | The Configuration Continuum: Using a Unified Model of Configuration to Prevent Outages CONFLANG | ||
11:22 22mTalk | Utilizing the LSP to inform and teach users on config languages CONFLANG Alexander Putman Google | ||
11:45 22mTalk | Evolving a configuration language in place at Google scale CONFLANG Marcos Lara-Reinhold Google | ||
12:07 22mLive Q&A | Experience reports Q&A/Discussion CONFLANG | ||
12:30 - 14:00 | |||
14:00 - 15:30 | |||
14:00 30mResearch paper | Constrained Horn Clauses Satisfiability via Catamorphic Abstractions LOPSTR Emanuele De Angelis CNR-IASI, Fabio Fioravanti University of Chieti-Pescara, Alberto Pettorossi University of Rome Tor Vergata, Italy, Maurizio Proietti CNR-IASI | ||
14:30 25mShort-paper | Transforming Big-Step to Small-Step Semantics Using Interpreter Specialisation LOPSTR John P. Gallagher Roskilde University, Manuel Hermenegildo Technical University of Madrid (UPM) and IMDEA Software Institute, José Morales IMDEA Software Institute, Pedro López-García IMDEA Software Institute | ||
14:55 10mDay closing | Closing and Adjourn LOPSTR | ||
14:00 - 15:30 | |||
14:00 30mTalk | Enabling Blended Modelling of Timing and Variability in EAST-ADLResearch Paper SLE Muhammad Waseem Anwar Department of Innovation, Design and Engineering Malardalen University, Federico Ciccozzi Mälardalen University, Alessio Bucaioni Mälardalen University | ||
14:30 30mTalk | Towards Efficient Model Comparison Using Automated Program RewritingResearch Paper SLE Qurat Ul Ain Ali University of York , Dimitris Kolovos University of York, Konstantinos Barmpis University of York | ||
15:00 30mTalk | Deriving Integrated Multi-Viewpoint Modeling Languages from Heterogeneous Modeling Languages: An Experience ReportResearch Paper SLE Malte Heithoff RWTH Aachen University, Nico Jansen Software Engineering, RWTH Aachen University, Jörg Christian Kirchhof RWTH Aachen University, Judith Michael RWTH Aachen University, Florian Rademacher RWTH Aachen University, Bernhard Rumpe RWTH Aachen University Pre-print | ||
14:00 - 15:30 | |||
14:00 30mTalk | A Mechanized Theory of the Box Calculus IWACO File Attached | ||
14:30 30mTalk | Compositional Reasoning about Advanced Iterator Patterns in Rust IWACO Aurel Bílý ETH Zurich, Jonas Hansen ETH Zurich, Alexander J. Summers University of British Columbia, Peter Müller ETH Zurich File Attached | ||
15:00 30mTalk | Oxidize: A Step-Debugger for Static Semantics IWACO Peter Chon Harvard University, Dimi Racordon Northeastern University, USA, Nada Amin Harvard University File Attached | ||
14:00 - 15:30 | |||
14:00 30mTalk | Remote Just-in-Time Compilation for Dynamic Languages Doctoral Symposium Andrej Pečimúth Oracle Labs | ||
14:30 30mTalk | Reusing Single-Language Analyses for Static Analysis of Multi-Language Programs Doctoral Symposium Tobias Roth Technische Universität Darmstadt | ||
15:00 30mTalk | Semantic Versioning for Python Programs Doctoral Symposium | ||
14:00 - 15:30 | |||
14:00 30mTalk | Can local-first really scale at the edge? PLF Carlos Baquero HASLab/INESC TEC & University of Minho | ||
14:30 30mTalk | Local-first at Actyx PLF | ||
15:00 30mTalk | Extending Automerge: Undo, Redo, and Move PLF | ||
14:00 - 15:30 | |||
14:00 30mTalk | JITs are Nice, but Why Aren’t We Using Them? DLS Kevin Menard Shopify | ||
14:30 30mTalk | Keeping the asm in Wasm – Running high-level languages on a low-level VM DLS Andreas Rossberg Independent | ||
15:00 30mTalk | Language Runtimes for the New Cloud Era DLS Rodrigo Bruno INESC-ID / Técnico, ULisboa | ||
14:00 - 15:30 | |||
14:00 22mTalk | The LIFE of CUE CONFLANG | ||
14:22 22mTalk | Ansible Is Turing Complete CONFLANG | ||
14:45 22mTalk | Cached call-by-name: incremental evaluation of configurations CONFLANG | ||
15:07 22mLive Q&A | Configuration languages Q&A/Discussion CONFLANG | ||
15:30 - 16:00 | |||
16:00 - 17:30 | |||
16:00 20mDemonstration | A Low-Code Platform for Systematic Component-Oriented Language CompositionTool Paper SLE | ||
16:20 20mDemonstration | A Tool for the Definition and Deployment of Platform-Independent Bots on Open Source ProjectsTool Paper SLE Adem Ait-Fonolla IN3 - UOC, Javier Luis Cánovas Izquierdo IN3 - UOC, Jordi Cabot Luxembourg Institute of Science and Technology | ||
16:40 20mDemonstration | Online Name-Based Navigation for Software Meta-languagesTool Paper SLE Peter D. Mosses Swansea University and Delft University of Technology Pre-print | ||
17:00 20mDemonstration | Practical Runtime Instrumentation of Software Languages: the Case of SciHookTool Paper SLE Dorian Leroy CEA/DAM/DIF, France, Benoît Lelandais CEA/DAM/DIF, France, Marie-Pierre Oudot CEA/DAM/DIF, France, Benoit Combemale University of Rennes, Inria, CNRS, IRISA | ||
16:00 - 17:30 | |||
16:00 30mTalk | A Pragmatic Approach to Syntax Repair Doctoral Symposium Breandan Considine McGill University | ||
16:30 60mMeeting | Discussion Doctoral Symposium Michael Coblenz University of California, San Diego | ||
16:00 - 17:30 | |||
16:00 22mTalk | How to Enforce and Verify Invariants in Weakly Consistent Databases PLF Dina Borrego NOVA LINCS, FCT, Universidade NOVA de Lisboa, Carla Ferreira NOVA University Lisbon, Nuno Preguica NOVA LINCS, FCT, Universidade NOVA de Lisboa | ||
16:22 22mTalk | Local-First in Practice: Learnings of building a high-performance, local-first music app PLF Johannes Schickling None | ||
16:45 22mTalk | MVC, MVCC and Causal Trees PLF Victor Grishchenko Unaffiliated | ||
17:07 22mTalk | Mixed & Verified Consistency with Propel & ConOpY PLF George Zakhour University of St.Gallen, Pascal Weisenburger University of St. Gallen, Guido Salvaneschi University of St. Gallen | ||
16:00 - 17:30 | |||
16:00 30mTalk | Programming Languages for AI Programing Agents DLS Mark Marron University of Kentucky | ||
16:30 30mTalk | The Bright Future of Debuggers: Challenges and Opportunities DLS Christophe Scholliers Universiteit Gent, Belgium | ||
16:00 - 17:30 | |||
16:00 22mTalk | Applying Large Scale Diffing to Declarative Configuration Code for Production Safety CONFLANG | ||
16:22 22mTalk | Creed for Speed: Comprehensive Infrastructure as Code Testing CONFLANG Daniel Sokolowski University of St. Gallen, David Spielmann University of St. Gallen, Guido Salvaneschi University of St. Gallen Pre-print | ||
16:45 22mTalk | Configuration testing for Borg at Google CONFLANG Alex Ivanov Google | ||
17:07 22mLive Q&A | Configuration testing Q&A/Discussion CONFLANG | ||
Wed 25 OctDisplayed time zone: Lisbon change
Wed 25 Oct
Displayed time zone: Lisbon change
09:00 - 10:30 | |||
09:00 90mKeynote | Scaling up machine learning without tears (and what do programming languages have to do with it)Keynote OOPSLA Dimitrios Vytiniotis DeepMind | ||
09:00 - 10:30 | |||
09:00 90mKeynote | Creating a learnable and inclusive programming languageKeynote Onward! Papers | ||
09:00 - 10:30 | |||
09:00 45mDay opening | Just-In-Time Introductions SPLASH-E | ||
09:45 45mTalk | Non-Archival Presentations SPLASH-E | ||
10:30 - 11:00 | |||
11:00 - 12:30 | |||
11:00 18mTalk | Grounded Copilot: How Programmers Interact with Code-Generating Models OOPSLA Shraddha Barke University of California at San Diego, Michael B. James University of California at San Diego, Nadia Polikarpova University of California at San Diego DOI | ||
11:18 18mTalk | Two Birds with One Stone: Boosting Code Generation and Code Search via a Generative Adversarial Network OOPSLA Shangwen Wang National University of Defense Technology, Bo Lin National University of Defense Technology, Zhensu Sun Singapore Management University, Ming Wen Huazhong University of Science and Technology, Yepang Liu Southern University of Science and Technology, Yan Lei Chongqing University, Xiaoguang Mao National University of Defense Technology DOI Pre-print | ||
11:36 18mTalk | Turaco: Complexity-Guided Data Sampling for Training Neural Surrogates of Programs OOPSLA Alex Renda Massachusetts Institute of Technology, Yi Ding Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology Pre-print | ||
11:54 18mTalk | Concrete Type Inference for Code Optimization Using Machine Learning with SMT Solving OOPSLA Fangke Ye Georgia Institute of Technology, Jisheng Zhao Georgia Institute of Technology, Jun Shirako Georgia Institute of Technology, Vivek Sarkar Georgia Institute of Technology | ||
12:12 18mTalk | An Explanation Method for Models of Code OOPSLA | ||
11:00 - 12:30 | |||
11:00 18mTalk | Asparagus: Automated Synthesis of Parametric Gas Upper-bounds for Smart Contracts OOPSLA Zhuo Cai Hong Kong University of Science and Technology, Soroush Farokhnia Hong Kong University of Science and Technology, Amir Kafshdar Goharshady IST Austria, Austria, S. Hitarth Hong Kong University of Science and Technology | ||
11:18 18mTalk | Equality Saturation Theory Exploration à la Carte OOPSLA Anjali Pal University of Washington, Brett Saiki University of Washington, Oliver Flatt , Ryan Tjoa University of Washington, Amy Zhu University of Washington, Cynthia Richey University of Washington, Max Willsey University of California, Berkeley, Zachary Tatlock University of Washington, Chandrakana Nandi Certora Pre-print | ||
11:36 18mTalk | Synthesizing Specifications OOPSLA Kanghee Park University of Wisconsin-Madison, Loris D'Antoni University of Wisconsin-Madison, Thomas Reps University of Wisconsin-Madison | ||
11:54 18mTalk | Explainable Program Synthesis by Localizing Specifications OOPSLA Amirmohammad Nazari University of Southern California, Yifei Huang University of Southern California, Roopsha Samanta Purdue University, Arjun Radhakrishna Microsoft, Mukund Raghothaman University of Southern California | ||
12:12 18mTalk | Pushing the Limit of 1-Minimality of Language-Agnostic Program Reduction OOPSLA Zhenyang Xu University of Waterloo, Yongqiang Tian The Hong Kong University of Science and Technology; University of Waterloo, Mengxiao Zhang University of Waterloo, Gaosen Zhao University of Waterloo, Yu Jiang Tsinghua University, Chengnian Sun University of Waterloo DOI | ||
11:00 - 12:30 | |||
11:00 30mTalk | Time-awareness in Object-exploration Tools: Toward In Situ Omniscient Debugging Onward! Papers Christoph Thiede Hasso Plattner Institute, University of Potsdam, Germany, Marcel Taeumel University of Potsdam; Hasso Plattner Institute, Robert Hirschfeld University of Potsdam; Hasso Plattner Institute DOI | ||
11:30 30mTalk | Code Merging Using Transformations and Member Identity Onward! Papers André R. Teles University Institute of Lisbon, André L. Santos University Institute of Lisbon, Portugal | ||
12:00 30mTalk | Scalable Spreadsheet-driven End-User Applications with Incremental Computation Onward! Papers | ||
11:00 - 12:30 | |||
11:00 30mTalk | Teaching Programming with Graphics: Pitfalls and a Solution SPLASH-E | ||
11:30 30mTalk | KOGI: A Seamless Integration of ChatGPT into Jupyter Environments for Programming Education SPLASH-E Kimio Kuramitsu Japan Women's University, Yui Obara Japan Women's University, Miyu Sato Japan Women's University, Momoka Obara Japan Women's University | ||
12:00 30mTalk | A Framework for the Localization of Programming Languages SPLASH-E Alaaeddin Swidan Open University of the Netherlands, The Netherlands, Felienne Hermans Vrije Universiteit Amsterdam | ||
14:00 - 15:30 | |||
14:00 18mTalk | Deep Learning Robustness Verification for Few-Pixel Attacks OOPSLA DOI | ||
14:18 18mTalk | Run-Time Prevention of Software Integration Failures of Machine Learning APIs OOPSLA Chengcheng Wan East China Normal University, Yuhan Liu University of Chicago, Kuntai Du University of Chicago, Henry Hoffmann University of Chicago, Junchen Jiang University of Chicago, Michael Maire University of Chicago, Shan Lu University of Chicago | ||
14:36 18mTalk | Compiling Structured Tensor Algebra OOPSLA Mahdi Ghorbani University of Edinburgh, Mathieu Huot University of Oxford, Shideh Hashemian University of Edinburgh, Amir Shaikhha University of Edinburgh | ||
14:54 18mTalk | Perception Contracts for Safety of ML-Enabled Systems OOPSLA Angello Astorga University of Illinois at Urbana-Champaign, Chiao Hsieh Graduate School of Informatics, Kyoto University, P. Madhusudan University of Illinois at Urbana-Champaign, Sayan Mitra University of Illinois at Urbana-Champaign | ||
15:12 18mTalk | Languages with Decidable Learning: A Meta-theorem OOPSLA Paul Krogmeier University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign DOI | ||
14:00 - 15:30 | |||
14:00 18mTalk | Mobius: Synthesizing Relational Queries with Recursive and Invented Predicates OOPSLA Aalok Thakkar University of Pennsylvania, Nathaniel Sands University of Southern California, Georgios Petrou University of Southern California, Rajeev Alur University of Pennsylvania, Mayur Naik University of Pennsylvania, Mukund Raghothaman University of Southern California | ||
14:18 18mTalk | Data Extraction via Semantic Regular Expression Synthesis OOPSLA Qiaochu Chen University of Texas at Austin, Arko Banerjee University of Texas at Austin, Çağatay Demiralp MIT CSAIL, Greg Durrett University of Texas at Austin, Işil Dillig University of Texas at Austin | ||
14:36 18mTalk | Synthesizing Efficient Memoization Algorithms OOPSLA | ||
14:54 18mTalk | Algebro-geometric Algorithms for Template-Based Synthesis of Polynomial Programs OOPSLA Amir Kafshdar Goharshady Hong Kong University of Science and Technology, S. Hitarth Hong Kong University of Science and Technology, Fatemeh Mohammadi KU Leuven, Harshit Jitendra Motwani Ghent University DOI | ||
15:12 18mTalk | Modular Component-Based Quantum Circuit Synthesis OOPSLA DOI | ||
14:00 - 15:30 | |||
14:00 30mTalk | Could No-Code be Code? -- Toward a No-Code Programming Language for Citizen Developers Onward! Papers | ||
14:30 30mTalk | Toward Programming Languages for Reasoning -- Humans, Symbolic Systems, and AI Agents Onward! Papers Mark Marron University of Kentucky | ||
15:00 30mTalk | Trustworthy Formal Natural Language Specifications Onward! Papers | ||
14:00 - 15:30 | |||
14:00 30mDay opening | Just-In-Time Introductions SPLASH-E | ||
14:30 30mTalk | Composing Turing Machines in FSM SPLASH-E Marco T Morazan Seton Hall University | ||
15:00 30mTalk | Witter: A Library for White-Box Testing of Introductory Programming Algorithms SPLASH-E Afonso Caniço Iscte - Instituto Universitário de Lisboa, André L. Santos University Institute of Lisbon, Portugal | ||
15:30 - 16:00 | |||
16:00 - 17:30 | |||
16:00 18mTalk | A Deductive Verification Infrastructure for Probabilistic Programs OOPSLA Philipp Schröer RWTH Aachen University, Kevin Batz RWTH Aachen University, Benjamin Lucien Kaminski Saarland University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja DTU | ||
16:18 18mTalk | A Gradual Probabilistic Lambda Calculus OOPSLA Wenjia Ye University of Hong Kong, Matías Toro University of Chile, Federico Olmedo University of Chile DOI | ||
16:36 18mTalk | Lower Bounds for Possibly Divergent Probabilistic Programs OOPSLA Shenghua Feng Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Mingshuai Chen Zhejiang University, Han Su Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Benjamin Lucien Kaminski Saarland University; University College London, Joost-Pieter Katoen RWTH Aachen University, Naijun Zhan Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences DOI | ||
16:54 18mTalk | Exact Recursive Probabilistic Programming OOPSLA David Chiang University of Notre Dame, Colin McDonald University of Notre Dame, Chung-chieh Shan Indiana University DOI | ||
17:12 18mTalk | Solving String Constraints with Lengths by Stabilization OOPSLA Yu-Fang Chen Academia Sinica, Taiwan, David Chocholatý Brno University of Technology, Czech Republic, Vojtěch Havlena Brno University of Technology, Lukáš Holík Brno University of Technology, Ondřej Lengál Brno University of Technology, Juraj Síč Brno University of Technology, Czech Republic | ||
16:00 - 17:30 | |||
16:00 45mTalk | Will code remain a relevant user interface for end-user programming with generative AI models? Onward! Essays Advait Sarkar Microsoft Research and University of Cambridge | ||
16:45 45mTalk | programmingLanguage as Language; Onward! Essays | ||
16:00 - 17:30 | |||
16:00 30mTalk | Centering Humans in the Programming Languages Classroom: Building a Text for the Next GenerationRemote SPLASH-E Rose Bohrer Worcester Polytechnic Institute | ||
16:30 30mTalk | Exploring Engagement and Self-Efficacy in an Introductory Computer Science CourseRemote SPLASH-E | ||
17:00 30mDay closing | Past, Present & Future of SPLASH-E Discussion SPLASH-E | ||
Thu 26 OctDisplayed time zone: Lisbon change
Thu 26 Oct
Displayed time zone: Lisbon change
09:00 - 10:30 | |||
09:00 90mKeynote | Hydroflow: A Compiler Target for Fast, Correct Distributed ProgramsKeynote OOPSLA Joseph M. Hellerstein UC Berkeley | ||
10:30 - 11:00 | |||
11:00 - 12:30 | |||
11:00 18mTalk | Reference Capabilities for Flexible Memory Management OOPSLA Ellen Arvidsson Uppsala University, Elias Castegren Uppsala University, Sylvan Clebsch Azure Research, Sophia Drossopoulou Imperial College London , James Noble Research & Programming, Matthew Parkinson Azure Research, Microsoft, UK, Tobias Wrigstad Uppsala University, Sweden | ||
11:18 18mTalk | A Grounded Conceptual Model for Ownership Types in Rust OOPSLA Will Crichton Brown University, Gavin Gray ETH Zürich, Shriram Krishnamurthi Brown University, United States DOI Pre-print | ||
11:36 18mTalk | Inference of Resource Management Specifications OOPSLA Narges Shadab University of California at Riverside, PRITAM MANOHAR GHARAT Microsoft Research India, Shrey Tiwari Microsoft Research, Michael D. Ernst University of Washington, Martin Kellogg New Jersey Institute of Technology, Shuvendu K. Lahiri Microsoft Research, Akash Lal Microsoft Research, Manu Sridharan University of California at Riverside | ||
11:54 18mTalk | Resource-aware soundness for big-step semantics OOPSLA Riccardo Bianchini University of Genoa, Francesco Dagnino University of Genoa, Paola Giannini University of Eastern Piedmont, Elena Zucca University of Genoa | ||
12:12 18mTalk | Verus: Verifying Rust Programs using Linear Ghost Types OOPSLA Andrea Lattuada VMware Research, Travis Hance Carnegie Mellon University, Chanhee Cho Carnegie Mellon University, Matthias Brun ETH Zurich, Isitha Subasinghe UNSW Sydney, Yi Zhou Carnegie Mellon University, Jon Howell VMware Research, Bryan Parno Carnegie Mellon University, Chris Hawblitzel Microsoft Research DOI | ||
11:00 - 12:30 | |||
11:00 18mTalk | The Essence of Verilog: A Tractable and Tested Operational Semantics for Verilog OOPSLA Qinlin Chen Nanjing University, Nairen Zhang Nanjing University, Jinpeng Wang Nanjing University, Tian Tan Nanjing University, Chang Xu Nanjing University, Xiaoxing Ma Nanjing University, Yue Li Nanjing University | ||
11:18 18mTalk | Regular Expression Matching using Bit Vector Automata OOPSLA Alexis Le Glaunec Rice University, Lingkun Kong Rice University, Konstantinos Mamouras Rice University DOI | ||
11:36 18mTalk | Bidirectional Object-Oriented Programming: Towards Programmatic and Direct Manipulation of Objects OOPSLA Xing Zhang Peking University, Guanchen Guo Peking University, Xiao He University of Science and Technology Beijing, Zhenjiang Hu Peking University DOI | ||
11:54 18mTalk | Bring Your Own Data Structures to Datalog OOPSLA Arash Sahebolamri Syracuse University, Langston Barrett Galois, Inc, Scott Moore Galois, Inc., Kristopher Micinski Syracuse University | ||
12:12 18mTalk | Rhombus: A New Spin on Macros Without All the Parentheses OOPSLA Matthew Flatt University of Utah, Taylor Allred University of Utah, Ross Angle independent, Stephen De Gabrielle independent, Robby Findler Northwestern University, Jack Firth independent, Kiran Gopinathan National University of Singapore, Ben Greenman Brown University, Siddhartha Kasivajhula independent, Alex Knauth Northeastern University, Jay McCarthy University of Massachusetts Lowell & Reach, Sam Phillips independent, Sorawee Porncharoenwase University of Washington, Jens Axel Søgaard independent, Sam Tobin-Hochstadt Indiana University Pre-print | ||
11:00 - 12:30 | |||
11:00 30mTalk | Cloning And Beyond: A Quantum Solution to Duplicate Code Onward! Papers | ||
11:30 30mTalk | Towards an Industrial Stateful Software Rejuvenation Toolchain Using Model Learning Onward! Papers | ||
12:00 30mTalk | Concept-Centric Software Development: An Experience Report Onward! Papers Peter Wilczynski Palantir Technologies, Taylor Gregoire-Wright Independent consultant, Daniel Jackson MIT | ||
14:00 - 15:30 | |||
14:00 18mTalk | Greedy Implicit Bounded Quantification OOPSLA Chen Cui University of Hong Kong, Shengyi Jiang University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong | ||
14:18 18mTalk | Structural Subtyping as Parametric Polymorphism OOPSLA Wenhao Tang The University of Edinburgh, Daniel Hillerström Huawei Zurich Research Center, James McKinna Heriot-Watt University, Michel Steuwer Technische Universität Berlin / University of Edinburgh, Ornela Dardha University of Glasgow, Rongxiao Fu The University of Edinburgh, Sam Lindley University of Edinburgh Pre-print | ||
14:36 18mTalk | Simple Reference Immutability for System F-Sub OOPSLA | ||
14:54 18mTalk | Mutually Iso-recursive Subtyping OOPSLA Andreas Rossberg Independent | ||
15:12 18mTalk | Getting Into The Flow: Better Type Error Messages for Constraint-Based Type Inference OOPSLA Ishan Bhanuka HKUST (The Hong Kong University of Science and Technology), Lionel Parreaux HKUST (The Hong Kong University of Science and Technology), David Binder University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen | ||
14:00 - 15:30 | |||
14:00 18mTalk | The Bounded Pathwidth of Control-flow Graphs OOPSLA Giovanna Kobus Conrado Hong Kong University of Science and Technology (HKUST), Amir Kafshdar Goharshady Hong Kong University of Science and Technology, Chun Kit LAM Hong Kong University of Science and Technology (HKUST) | ||
14:18 18mTalk | How Profilers Can Help Navigate Type Migration OOPSLA Ben Greenman Brown University, Matthias Felleisen PLT @ Northeastern University, Christos Dimoulas PLT @ Northwestern University | ||
14:36 18mTalk | Synthesizing Precise Static Analyzers for Automatic Differentiation OOPSLA Jacob Laurel University of Illinois at Urbana-Champaign, Siyuan Brant Qian University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign, Sasa Misailovic University of Illinois at Urbana-Champaign | ||
14:54 18mTalk | A Container-Usage-Pattern-based Context Debloating Approach for Object-Sensitive Pointer Analysis OOPSLA Dongjie He UNSW, Yujiang Gui UNSW Sydney, Wei Li University of New South Wales, Yonggang Tao University of New South Wales, Changwei Zou University of New South Wales, Yulei Sui University of New South Wales, Sydney, Jingling Xue UNSW | ||
15:12 18mTalk | Static Analysis of Memory Models for SMT Encodings OOPSLA Thomas Haas Technical University of Braunschweig, René Maseli TU Braunschweig, Roland Meyer TU Braunschweig, Hernán Ponce de León Huawei Dresden Research Center | ||
14:00 - 15:30 | |||
14:00 45mTalk | Sharing a Perspective on the lambda-Calculus Onward! Essays Beniamino Accattoli Inria & Ecole Polytechnique | ||
14:45 45mTalk | Whither Problem-Solving Environments? Onward! Essays Matthew Dinmore Johns Hopkins Applied Physics Laboratory | ||
15:30 - 16:00 | |||
16:00 - 17:30 | |||
16:00 18mTalk | Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect Systems OOPSLA Magnus Madsen Aarhus University, Jaco van de Pol Aarhus University, Troels Henriksen University of Copenhagen, Denmark | ||
16:18 18mTalk | From Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect Handlers OOPSLA Marius Müller University of Tübingen, Philipp Schuster University of Tübingen, Jonathan Lindegaard Starup Aarhus University, Klaus Ostermann University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen Pre-print | ||
16:36 18mTalk | Gradual Typing for Effect Handlers OOPSLA Max New University of Michigan, Eric Giovannini University of Michigan, Dan Licata Wesleyan University | ||
16:54 18mTalk | When Concurrency Matters: Behaviour-Oriented Concurrency OOPSLA Luke Cheeseman Imperial College London, Matthew Parkinson Azure Research, Microsoft, UK, Sylvan Clebsch Azure Research, Marios Kogias Imperial College London & Microsoft Research, Sophia Drossopoulou Imperial College London , David Chisnall , Tobias Wrigstad Uppsala University, Sweden, Paul Liétar Imperial College London | ||
17:12 18mTalk | Continuing WebAssembly with Effect Handlers OOPSLA Luna Phipps-Costin Northeastern University, Andreas Rossberg Independent, Arjun Guha Northeastern University and Roblox Research, Daan Leijen Microsoft Research, Daniel Hillerström Huawei Zurich Research Center, KC Sivaramakrishnan IIT Madras and Tarides, Matija Pretnar University of Ljubljana, Slovenia, Sam Lindley University of Edinburgh Pre-print | ||
16:00 - 17:30 | |||
16:00 18mTalk | Historia: Refuting Callback Reachability with Message-History Logics OOPSLA Shawn Meier University of Colorado, Boulder, Sergio Mover Ecole Polytechnique, Gowtham Kaki University of Colorado Boulder, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon | ||
16:18 18mTalk | Exploiting the Sparseness of Control-flow and Call Graphs for Efficient and On-demand Algebraic Program Analysis OOPSLA Giovanna Kobus Conrado Hong Kong University of Science and Technology (HKUST), Amir Kafshdar Goharshady Hong Kong University of Science and Technology, Kerim Kochekov Hong Kong University of Science and Technology, Yun Chen Tsai Hong Kong University of Science and Technology, Ahmed Khaled Zaher HKUST | ||
16:36 18mTalk | A Cocktail Approach to Practical Call Graph Construction OOPSLA Yuandao Cai Hong Kong University of Science and Technology, China, Charles Zhang Hong Kong University of Science and Technology | ||
16:54 18mTalk | Building Dynamic System Call Sandbox With Partial Order Analysis OOPSLA Quan Zhang Tsinghua University, Chijin Zhou Tsinghua University, Yiwen Xu Tsinghua University, Zijing Yin Tsinghua University, Mingzhe Wang Tsinghua University, Zhuo Su Tsinghua University, Chengnian Sun University of Waterloo, Yu Jiang Tsinghua University, Jiaguang Sun Tsinghua University | ||
17:12 18mTalk | Improving Oracle-Guided Inductive Synthesis by Efficient Question Selection OOPSLA Ruyi Ji Peking University, Chaozhe Kong Peking University, Yingfei Xiong Peking University, Zhenjiang Hu Peking University DOI | ||
16:00 - 17:30 | |||
16:00 18mTalk | Graph IRs for Impure Higher-Order Languages - Making Aggressive Optimizations Affordable with Precise Effect Dependencies OOPSLA Oliver Bračevac Galois, Inc., Guannan Wei Purdue University, Songlin Jia Purdue University, Supun Abeysinghe Purdue University, Yuxuan Jiang Purdue University, Yuyan Bao Computer and Cyber Sciences, Augusta University, Georgia, USA, Tiark Rompf Purdue University | ||
16:18 18mTalk | AST vs. Bytecode: Interpreters in the Age of Meta-Compilation OOPSLA Octave Larose University of Kent, Sophie Kaleba University of Kent, Humphrey Burchell University of Kent, Stefan Marr University of Kent DOI Pre-print | ||
16:36 18mTalk | Reusing Just-in-Time Compiled Code OOPSLA Meetesh Kalpesh Mehta Indian Institute of Technology Bombay, Sebastián Krynski Czech Technical University, Hugo Musso Gualandi Czech Technical University in Prague, Manas Thakur Indian Institute of Technology Bombay, Jan Vitek Northeastern University | ||
16:54 18mTalk | TASTyTruffle: Just-in-time Specialization of Parametric Polymorphism OOPSLA Matt D'Souza University of Waterloo, James You University of Waterloo, Ondřej Lhoták University of Waterloo, Aleksandar Prokopec Oracle Labs | ||
17:12 18mTalk | Beacons: An End-to-End Compiler Framework for Predicting and Utilizing Dynamic Loop Characteristics OOPSLA Girish Mururu Georgia Institute of Technology, Sharjeel Khan Georgia Institute of Technology, Bodhisatwa Chatterjee Georgia Institute of Technology, Chao Chen Georgia Institute of Technology, Chris Porter Georgia Institute of Technology, USA, Ada Gavrilovska Georgia Institute of Technology, Santosh Pande Georgia Institute of Technology | ||
Fri 27 OctDisplayed time zone: Lisbon change
Fri 27 Oct
Displayed time zone: Lisbon change
09:00 - 10:30 | |||
09:00 90mKeynote | All the Languages TogetherKeynote OOPSLA Amal Ahmed Northeastern University, USA | ||
10:30 - 11:00 | |||
11:00 - 12:30 | |||
11:00 18mTalk | Towards Better Semantics Exploration for Browser Fuzzing OOPSLA Chijin Zhou Tsinghua University, Quan Zhang Tsinghua University, Lihua Guo Tsinghua University, Mingzhe Wang Tsinghua University, Yu Jiang Tsinghua University, Qing Liao Harbin Institute of Technology, Zhiyong Wu National University of Defense Technology, Shanshan Li National University of Defense Technology, Bin Gu Beijing Institute of Control Engineering, China | ||
11:18 18mTalk | Live Pattern Matching with Typed Holes OOPSLA Yongwei Yuan Purdue University, Scott Guest University of Michigan, Eric Griffis University of Michigan, Hannah Potter University of Washington, David Moon University of Michigan, Cyrus Omar University of Michigan DOI | ||
11:36 18mTalk | Interactive Debugging of Datalog Programs OOPSLA | ||
11:54 18mTalk | Accelerating Fuzzing through Prefix-Guided Execution OOPSLA DOI | ||
12:12 18mTalk | MemPerf: Profiling Allocator-Induced Performance Slowdowns OOPSLA Jin Zhou University of Massachusetts Amherst, Sam Silvestro University of Texas at San Antonio, Jiaxun,Tang University of Massachusetts Amherst, Hanmei Yang University of Massachusetts Amherst, Hongyu Liu University of Texas at San Antonio, Guangming Zeng Synopsys, Bo Wu Colorado School of Mines, Cong Liu University of California at Riverside, Tongping Liu University of Massachusetts at Amherst | ||
14:00 - 15:30 | |||
14:00 18mTalk | Stuttering for Free OOPSLA Minki Cho Seoul National University, Youngju Song MPI-SWS, Dongjae Lee Seoul National University, Lennard Gäher MPI-SWS & Saarland University, Derek Dreyer MPI-SWS | ||
14:18 18mTalk | Compositional Verification of Efficient Masking Countermeasures against Side-Channel Attacks OOPSLA Pengfei Gao ShanghaiTech University, Yedi Zhang ShanghaiTech University, Fu Song ShanghaiTech University, Taolue Chen Birkbeck University of London, Francois-Xavier Standaert UCLouvain | ||
14:36 18mTalk | Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier OOPSLA Zhengyao Lin Carnegie Mellon University, Xiaohong Chen University of Illinois at Urbana-Champaign, Minh-Thai Trinh Advanced Digital Sciences Center, John Wang University of Illinois at Urbana-Champaign, Grigore Roşu University of Illinois at Urbana-Champaign DOI | ||
14:54 18mTalk | Complete First-Order Reasoning for Properties of Functional Programs OOPSLA Adithya Murali University of Illinois at Urbana-Champaign, Lucas Pena , Ranjit Jhala University of California at San Diego, P. Madhusudan University of Illinois at Urbana-Champaign | ||
15:12 18mTalk | Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols OOPSLA Orr Tamir Tel Aviv University, Marcelo Taube Tel Aviv University, Israel, Kenneth L. McMillan University of Texas at Austin, Sharon Shoham Tel Aviv University, Jon Howell VMware Research, Guy Gueta VMWare, Mooly Sagiv Tel Aviv University | ||
14:00 - 15:30 | |||
14:00 18mTalk | Formally Verifying Optimizations with Block Simulations OOPSLA Leo Gourdin Université Grenoble-Alpes, Benjamin Bonneau ENS PSL, Sylvain Boulmé Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, David Monniaux CNRS/VERIMAG, Alexandre Bérard Université Grenoble-Alpes DOI Pre-print | ||
14:18 18mTalk | Back to Direct Style: Typed and Tight OOPSLA Marius Müller University of Tübingen, Philipp Schuster University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen, Klaus Ostermann University of Tübingen DOI Pre-print | ||
14:36 18mTalk | Hardware-Aware Static Optimization of Hyperdimensional Computations OOPSLA | ||
14:54 18mTalk | Rapid: Region-based Pointer Disambiguation OOPSLA | ||
15:12 18mTalk | Automated Ambiguity Detection in Layout-Sensitive Grammars OOPSLA Jiangyi Liu Tsinghua University, Fengmin Zhu CISPA Helmholtz Center for Information Security, Fei He Tsinghua University Pre-print | ||
15:30 - 16:00 | |||
16:00 - 17:30 | |||
16:00 18mTalk | Aliasing Limits on Translating C to Safe Rust OOPSLA Mehmet Emre University of San Francisco, Peter Boyland University of California at Santa Barbara, Aesha Parekh University of California at Santa Barbara, Ryan Schroeder University of California at Santa Barbara, Kyle Dewey California State University, Ben Hardekopf University of California at Santa Barbara DOI Pre-print | ||
16:18 18mTalk | Adventure of a Lifetime: Extract Method Refactoring for Rust OOPSLA Sewen Thy Ahrefs Research, Andreea Costea School of Computing, National University Of Singapore, Kiran Gopinathan National University of Singapore, Ilya Sergey National University of Singapore DOI Pre-print | ||
16:36 18mTalk | Inductive Program Synthesis Guided by Observational Program Similarity OOPSLA John Feser Massachusetts Institute of Technology, Işil Dillig University of Texas at Austin, Armando Solar-Lezama Massachusetts Institute of Technology | ||
16:54 18mTalk | Automated Translation of Functional Big Data Queries to SQL OOPSLA Guoqiang Zhang North Carolina State University, Benjamin Mariano University of Texas at Austin, Xipeng Shen North Carolina State University, Işil Dillig University of Texas at Austin DOI | ||
17:12 18mTalk | User-Customizable Transpilation of Scripting Languages OOPSLA Bo Wang National University of Singapore, Aashish Kolluri National University of Singapore, Ivica Nikolić National University of Singapore, Teodora Baluta National University of Singapore, Prateek Saxena National University of Singapore DOI | ||
16:00 - 17:30 | |||
16:00 18mTalk | Verification-Preserving Inlining in Automatic Separation Logic Verifiers OOPSLA DOI | ||
16:18 18mTalk | Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory OOPSLA | ||
16:36 18mTalk | Leaf: Modularity for Temporary Sharing in Separation Logic OOPSLA Travis Hance Carnegie Mellon University, Jon Howell VMware Research, Oded Padon VMware Research, Bryan Parno Carnegie Mellon University | ||
16:54 18mTalk | Proof Automation for Linearizability in Separation Logic OOPSLA DOI Pre-print | ||
17:12 18mTalk | Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic OOPSLA Jaehwang Jung KAIST, South Korea, Janggun Lee KAIST, Jaemin Choi , Jaewoo Kim KAIST, Sunho Park KAIST, Jeehoon Kang KAIST | ||