SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
VenueHotel Cascais Miragem
Room nameRoom II
Floor0
Capacity196
Room InformationNo extra information available
Program

This program is tentative and subject to change.

You're viewing the program in a time zone which is different from your device's time zone - change time zone

Sun 22 Oct

Displayed time zone: Lisbon change

09:00 - 10:30
Session 1SAS at Room II
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
60m
Keynote
Goal-Directed Abstract Interpretation and Event-Driven FrameworksKeynote
SAS
I: Bor-Yuh Evan Chang University of Colorado Boulder & Amazon
10:05
30m
Talk
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
11:00 - 12:30
Domain precisionSAS at Room II
11:00
30m
Talk
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
30m
Talk
Domain Precision in Galois Connection-less Abstract Interpretation
SAS
Isabella Mastroeni University of Verona, Italy, Michele Pasqua University of Verona
12:00
30m
Talk
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
14:00 - 15:30
Synthesis and applicationsSAS at Room II
14:00
30m
Talk
Generalized Program Sketching by Abstract Interpretation and Logical Abduction
SAS
Aleksandar S. Dimovski Mother Teresa University, Skopje
14:30
30m
Talk
Reverse Template Processing using Abstract Interpretation
SAS
Matthieu Lemerre Université Paris-Saclay - CEA LIST
15:00
30m
Talk
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
16:00 - 17:30
Quantum, neuralSAS at Room II
16:00
30m
Talk
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
30m
Talk
Boosting Multi-Neuron Convex Relaxation for Neural Network Verification
SAS
XueZhou Tang ShenZhen University, Ye Zheng Shenzhen University, Jiaxiang Liu Shenzhen University

Mon 23 Oct

Displayed time zone: Lisbon change

11:00 - 12:30
Modular arithmetic and numeric analysisSAS at Room II
11:00
30m
Talk
Symbolic transformation of expressions in modular arithmetic
SAS
Jérôme Boillot École Normale Supérieure, PSL University & INRIA, Jerome Feret INRIA Paris
11:30
30m
Talk
Polynomial Analysis of Modular Arithmetic
SAS
Thomas Seed University of Kent, Andy King Kent, Neil Evans AWE, Chris Coppins University of Kent
12:00
30m
Talk
Octagons Revisited - Elegant Proofs and Simplified Algorithms
SAS
Michael Schwarz Technische Universität München, Helmut Seidl Technische Universität München
14:00 - 15:30
Error location and scalingSAS at Room II
14:00
30m
Talk
Error Invariants for Fault Localization via Abstract Interpretation
SAS
Aleksandar S. Dimovski Mother Teresa University, Skopje
14:30
30m
Talk
Error Localization for Sequential Effect Systems
SAS
Colin Gordon Drexel University, Chaewon Yun Drexel University
15:00
30m
Talk
Scaling up Roundoff Analysis of Functional Data Structure Programs
SAS
Anastasia Isychev Technical University of Munich, Eva Darulova Uppsala University
16:00 - 17:30
Session 8SAS at Room II
16:00
60m
Keynote
Building Trust and Safety in Artificial Intelligence with Abstract InterpretationKeynote
SAS
I: Gagandeep Singh University of Illinois at Urbana-Champaign
17:00
30m
Awards
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

Tue 24 Oct

Displayed time zone: Lisbon change

09:00 - 10:30
Session 9SAS at Room II
09:00
60m
Keynote
Verifying Infinitely Many Programs at OnceKeynote
SAS
I: Loris D'Antoni University of Wisconsin-Madison
10:00
30m
Talk
Mutual Refinements of Context-Free Language Reachability
SAS
Shuo Ding Georgia Institute of Technology, Qirun Zhang Georgia Institute of Technology
11:00 - 12:30
Cost/precision trade-offs and accelerationSAS at Room II
11:00
30m
Talk
ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses
SAS
Florian Frohn RWTH Aachen University, Jürgen Giesl RWTH Aachen University
11:30
30m
Talk
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
30m
Talk
Modular Optimization-Based Roundoff Error Analysis of Floating-Point Programs
SAS
Rosa Abbasi Boroujeni Max Planck Institute for Software Systems, Eva Darulova Uppsala University

Wed 25 Oct

Displayed time zone: Lisbon change

11:00 - 12:30
program synthesis 1OOPSLA at Room II
11:00
18m
Talk
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
18m
Talk
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
18m
Talk
Synthesizing Specifications
OOPSLA
Kanghee Park University of Wisconsin-Madison, Loris D'Antoni University of Wisconsin-Madison, Thomas Reps University of Wisconsin-Madison
11:54
18m
Talk
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
18m
Talk
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
14:00 - 15:30
program synthesis 2OOPSLA at Room II
14:00
18m
Talk
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
18m
Talk
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
18m
Talk
Synthesizing Efficient Memoization Algorithms
OOPSLA
Yican Sun Peking University, Xuanyu Peng Peking University, Yingfei Xiong Peking University
14:54
18m
Talk
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
18m
Talk
Modular Component-Based Quantum Circuit Synthesis
OOPSLA
Chan Gu Kang Korea University, Hakjoo Oh Korea University
DOI
16:00 - 17:30
16:00
15m
Talk
Fluent APIs in Functional Languages
OOPSLA
Ori Roth Technion, Yossi Gil Technion
DOI Pre-print
16:15
15m
Talk
Mat2Stencil: A Modular Matrix-Based DSL for Explicit and Implicit Matrix-Free PDE Solvers on Structured Grid
OOPSLA
Huanqi Cao Tsinghua University, Shizhi Tang Tsinghua University, Qianchao Zhu Peking University, Bowen Yu Nanjing University, Wenguang Chen Tsinghua University
16:30
15m
Talk
How Domain Experts Use an Embedded DSL
OOPSLA
Lisa Rennels UC Berkeley, Sarah E. Chasins University of California at Berkeley
16:45
15m
Talk
Saggitarius: A DSL for Specifying Grammatical Domains
OOPSLA
Anders Miltner Simon Fraser University, Devon Loehr Princeton University, Arnold Mong Princeton University, Kathleen Fisher Tufts University, David Walker Princeton University
17:00
15m
Talk
A Pretty Expressive Printer
OOPSLA
Sorawee Porncharoenwase University of Washington, Justin Pombrio Brown University, USA, Emina Torlak Amazon Web Services, USA
Pre-print
17:15
15m
Talk
Translating canonical SQL to imperative code in Coq
OOPSLA
Véronique Benzaken Université Paris-Saclay - Laboratoire de Méthodes Formelles , Évelyne Contejean CNRS, ENS Paris-Saclay & Université Paris-Saclay, Houssem Hachmaoui , Chantal Keller Université Paris Saclay, Louis Mandel IBM Research, USA, Avraham Shinnar IBM Research, Jerome Simeon DocuSign, Inc.
Link to publication DOI

Thu 26 Oct

Displayed time zone: Lisbon change

11:00 - 12:30
language semanticsOOPSLA at Room II
11:00
18m
Talk
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
18m
Talk
Regular Expression Matching using Bit Vector Automata
OOPSLA
Alexis Le Glaunec Rice University, Lingkun Kong Rice University, Konstantinos Mamouras Rice University
DOI
11:36
18m
Talk
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
18m
Talk
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
18m
Talk
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
14:00 - 15:30
program analysis 1OOPSLA at Room II
14:00
18m
Talk
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
18m
Talk
How Profilers Can Help Navigate Type Migration
OOPSLA
Ben Greenman Brown University, Matthias Felleisen PLT @ Northeastern University, Christos Dimoulas PLT @ Northwestern University
14:36
18m
Talk
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
18m
Talk
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
18m
Talk
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
16:00 - 17:30
program analysis 2OOPSLA at Room II
16:00
18m
Talk
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
18m
Talk
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
18m
Talk
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
18m
Talk
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
18m
Talk
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

Fri 27 Oct

Displayed time zone: Lisbon change

11:00 - 12:30
distribution & networking 1OOPSLA at Room II
11:00
18m
Talk
Initializing Global Objects: Time and Order
OOPSLA
Fengyun Liu Oracle Labs, Ondřej Lhoták University of Waterloo, David Hua University of Waterloo, Enze Xing University of Waterloo
11:18
18m
Talk
Type-Safe Dynamic Placement with First-Class Placed Values
OOPSLA
George Zakhour University of St.Gallen, Pascal Weisenburger University of St. Gallen, Guido Salvaneschi University of St. Gallen
DOI Pre-print
11:36
18m
Talk
Secure RDTs: Enforcing Access Control Policies for Offline Available JSON Data
OOPSLA
Thierry Renaux Vrije Universiteit Brussel, Sam Van den Vonder Vrije Universiteit Brussel, Wolfgang De Meuter Vrije Universiteit Brussel
DOI Pre-print
11:54
18m
Talk
AtomiS: Data-centric synchronization made practical
OOPSLA
Hervé Paulino NOVA University of Lisbon, Ana Matos University of Lisbon, Jan Cederquist University of Lisbon, Marco Giunti NOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa, João Batista Pereira Matos Júnior Sidia Instituto de Ciência e Tecnologia, Antonio Ravara NOVA LINCS & FCT, NOVA University of Lisbon
12:12
18m
Talk
Enabling Bounded Verification of Doubly-Unbounded Distributed Agreement-Based Systems via Bounded Regions
OOPSLA
Christopher Wagner Purdue University, Nouraldin Jaber Purdue University, Roopsha Samanta Purdue University
DOI
14:00 - 15:30
compilation and optimization 1OOPSLA at Room II
14:00
18m
Talk
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
18m
Talk
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
18m
Talk
Hardware-Aware Static Optimization of Hyperdimensional Computations
OOPSLA
Pu (Luke) Yi Stanford University, Sara Achour MIT
14:54
18m
Talk
Rapid: Region-based Pointer Disambiguation
OOPSLA
Khushboo Chitre IIIT Delhi, Piyus Kedia IIIT Delhi, Rahul Purandare University of Nebraska-Lincoln
15:12
18m
Talk
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
16:00 - 17:30
refactoringOOPSLA at Room II
16:00
18m
Talk
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
18m
Talk
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
18m
Talk
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
18m
Talk
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
18m
Talk
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

Sun 22 Oct

Displayed time zone: Lisbon change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Room II

Mon 23 Oct

Displayed time zone: Lisbon change

Tue 24 Oct

Displayed time zone: Lisbon change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Room II

Wed 25 Oct

Displayed time zone: Lisbon change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Room II

Thu 26 Oct

Displayed time zone: Lisbon change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Room II

Fri 27 Oct

Displayed time zone: Lisbon change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Room II