POPL 2022
Sun 16 - Fri 28 January 2022
Philadelphia, Pennsylvania, United States
Toggle navigation
Attending
Hotel: Westin Philadelphia
Supporting POPL
Accessibility
Visa Information
Registration
Program
Complete Program
Your Program
Filter by Day
Sun 16 Jan
Mon 17 Jan
Tue 18 Jan
Wed 19 Jan
Thu 20 Jan
Fri 21 Jan
Sat 22 Jan
Sun 23 Jan
Mon 24 Jan
Tue 25 Jan
Wed 26 Jan
Thu 27 Jan
Fri 28 Jan
Tracks
POPL 2022
POPL
Student Research Competition
Student Volunteers
TutorialFest
Artifact Evaluation
Workshops and Co-located Events
Virtual Workshop
Diversity, Equity and Inclusion
Co-hosted Conferences
CPP
VMCAI
VMCAI
- Back to the Future: A Fresh Look at Linear Temporal Logic
- Sequential Information Flow
- Simplifying Concurrent Programming via Synchronization Synthesis
Workshops
CoqPL
LAFI
PEPM
PLMW
PriSC
ProLaLa
Programming Languages and the Law
WITS
Co-hosted Symposia
PADL
Organization
POPL 2022 Committees
Organizing Committee
Track Committees
POPL
Student Research Competition
TutorialFest
Artifact Evaluation
Virtual Workshop
Contributors
People Index
Co-hosted Conferences
CPP
Organization Committee
Program Committee
Steering Committee
VMCAI
Organizing Committee
Program Committee
Artifact Evaluation Committee
Workshops
CoqPL
Invited speaker
Organizing Committee
Program Committee
LAFI
Organizing Committee
Program Committee
Steering Committee
PEPM
Organizing Committee
Program Committee
Steering Committee
PLMW
Organizing Committee
Invited speakers
Panelists
PriSC
Program Committee
Steering Committee
ProLaLa
Program Committee
WITS
Program Committee
Co-hosted Symposia
PADL
Programme Chairs
Programme Committee
Search
Series
Series
POPL 2025
POPL 2024
POPL 2023
POPL 2022
POPL 2021
POPL 2020
POPL 2019
POPL 2018
POPL 2017
POPL 2016
Sign in
Sign up
POPL 2022
(
series
) /
Westin Philadelphia
/
Room information: Salon I
Venue
Westin Philadelphia
Room name
Salon I
Room Information
No extra information available
Program
Detailed Table
Session Timeline
Detailed Timeline
Program Display Configuration
Time Zone
The program is currently displayed in
(GMT-05:00) Eastern Time (US & Canada)
.
Use conference time zone: (GMT-05:00) Eastern Time (US & Canada)
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-10:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-09:00) Alaska
(GMT-08:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-08:00) Pacific Time (US & Canada)
(GMT-07:00) Mountain Time (US & Canada)
(GMT-07:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-05:00) Guadalajara, Mexico City, Monterrey
(GMT-05:00) Easter Island
(GMT-06:00) Central Time (US & Canada)
(GMT-05:00) Eastern Time (US & Canada)
(GMT-05:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-03:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-04:00) Manaus, Amazonas, Brazil
(GMT-04:00) Atlantic Time (Goose Bay)
(GMT-04:00) Atlantic Time (Canada)
(GMT-03:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-03:00) Miquelon, St. Pierre
(GMT-03:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-03:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT-01:00) Azores
(UTC) Coordinated Universal Time
(GMT) Belfast
(GMT) Dublin
(GMT) Lisbon
(GMT) London
(GMT) Monrovia, Reykjavik
(GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+01:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+01:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+02:00) Athens
(GMT+02:00) Beirut
(GMT+02:00) Cairo
(GMT+02:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+02:00) Jerusalem
(GMT+03:00) Minsk
(GMT+02:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+03:30) Tehran
(GMT+04:00) Abu Dhabi, Muscat
(GMT+04:00) Yerevan
(GMT+04:30) Kabul
(GMT+05:00) Ekaterinburg
(GMT+05:00) Tashkent
(GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi
(GMT+05:45) Kathmandu
(GMT+06:00) Astana, Dhaka
(GMT+07:00) Novosibirsk
(GMT+06:30) Yangon (Rangoon)
(GMT+07:00) Bangkok, Hanoi, Jakarta
(GMT+07:00) Krasnoyarsk
(GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi
(GMT+08:00) Irkutsk, Ulaan Bataar
(GMT+08:00) Perth
(GMT+08:45) Eucla
(GMT+09:00) Osaka, Sapporo, Tokyo
(GMT+09:00) Seoul
(GMT+09:00) Yakutsk
(GMT+10:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+11:00) Hobart
(GMT+10:00) Vladivostok
(GMT+11:00) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+12:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+13:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+13:45) Chatham Islands
(GMT+13:00) Nuku'alofa
(GMT+14:00) Kiritimati
The GMT offsets shown reflect the offsets
at the moment of the conference
.
Time Band
By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.
Display full program
Specify a time band
-
Save
×
You're viewing the program in a time zone which is different from your device's time zone
change time zone
Sun 16 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
09:00 - 10:00
Invited Talk
VMCAI
at
Salon I
Chair(s):
Thomas Wies
New York University
09:00
60m
Keynote
Sequential Information Flow
Remote
VMCAI
Thomas A. Henzinger
IST Austria, Austria
10:20 - 11:50
Static Analysis and Abstract Interpretation
VMCAI
at
Salon I
Chair(s):
Thomas Wies
New York University
10:20
30m
Paper
Relational String Abstract Domains
Remote
VMCAI
Vincenzo Arceri
University of Parma - Department of Mathematical, Physical, and Computer Sciences
,
Martina Olliaro
Ca' Foscari University of Venice - Department of Environmental Sciences, Informatics and Statistics
,
Agostino Cortesi
Università Ca' Foscari Venezia
,
Pietro Ferrara
Università Ca' Foscari, Venezia, Italy
10:50
30m
Paper
Lightweight Shape Analysis based on Physical Types
InPerson
VMCAI
Olivier Nicole
CEA LIST, France
,
Matthieu Lemerre
CEA LIST, France
,
Xavier Rival
INRIA/CNRS/ENS Paris
11:20
30m
Paper
A Flow-Insensitive-Complete Program Representation
Remote
VMCAI
Solène Mirliaz
ENS Rennes / IRISA / Inria
,
David Pichardie
Facebook Paris
13:30 - 14:30
Privacy and Security
VMCAI
at
Salon I
Chair(s):
Vincenzo Arceri
University of Parma - Department of Mathematical, Physical, and Computer Sciences
13:30
30m
Paper
Verifying Pufferfish Privacy in Hidden Markov Models
Remote
VMCAI
Depeng Liu
Institute of Software, Chinese Academy of Sciences
,
Bow-Yaw Wang
Academia Sinica
,
Lijun Zhang
Institute of Software, Chinese Academy of Sciences
14:00
30m
Paper
Verifying Solidity Smart Contracts Via Communication Abstraction in SmartACE
Remote
VMCAI
Scott Wesley
University of Waterloo, Canada
,
Maria Christakis
MPI-SWS
,
Jorge A. Navas
Certora, inc.
,
Richard Trefler
University of Waterloo, Canada
,
Valentin Wüstholz
ConsenSys
,
Arie Gurfinkel
University of Waterloo
15:05 - 16:35
Satisfiability Modulo Theories
VMCAI
at
Salon I
Chair(s):
Natarajan Shankar
SRI International, USA
15:05
30m
Paper
Generalized Arrays for Stainless Frames
Remote
VMCAI
Georg Stefan Schmid
EPFL, Switzerland
,
Viktor Kunčak
EPFL, Switzerland
15:35
30m
Paper
NP Satisfiability for Arrays as Powers
InPerson
VMCAI
Rodrigo Raya
EPFL
,
Viktor Kunčak
EPFL, Switzerland
16:05
30m
Paper
Bit-Precise Reasoning via Int-Blasting
Remote
VMCAI
Yoni Zohar
Bar Ilan University
,
Ahmed Irfan
Stanford University
,
Makai Mann
Stanford University
,
Aina Niemetz
Stanford University
,
Andres Nötzli
Stanford University, USA
,
Mathias Preiner
Stanford University
,
Andrew Reynolds
University of Iowa
,
Clark Barrett
Stanford University
,
Cesare Tinelli
University of Iowa
Mon 17 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
09:00 - 10:00
Invited Talk
VMCAI
at
Salon I
Chair(s):
Bernd Finkbeiner
CISPA Helmholtz Center for Information Security
09:00
60m
Keynote
Back to the Future: A Fresh Look at Linear Temporal Logic
Remote
VMCAI
Javier Esparza
10:20 - 11:50
Model Checking
VMCAI
at
Salon I
Chair(s):
Arie Gurfinkel
University of Waterloo
10:20
30m
Paper
Automata-Driven Partial Order Reduction and Guided Search for LTL Model Checking
Remote
VMCAI
Peter Gjøl Jensen
Aalborg University, Denmark
,
Jiri Srba
Aalborg University
,
Nikolaj Jensen Ulrik
Aalborg University
,
Simon Mejlby Virenfeldt
Aalborg University
10:50
30m
Paper
Stateful Dynamic Partial Order Reduction for Model Checking Event-Driven Applications that Do Not Terminate
Remote
VMCAI
Rahmadi Trimananda
University of California at Irvine, USA
,
Weiyu Luo
University of California, Irvine
,
Brian Demsky
University of California at Irvine
,
Harry Xu
University of California, Los Angeles (UCLA)
Link to publication
DOI
Pre-print
Media Attached
File Attached
11:20
30m
Paper
Scaling Up Livelock Verification for Network-on-Chip Routing Algorithms
InPerson
VMCAI
Landon Taylor
Utah State University
,
Zhen Zhang
Utah State University
13:30 - 14:30
Formal Methods in Machine Learning
VMCAI
at
Salon I
Chair(s):
Rupak Majumdar
MPI-SWS
13:30
30m
Paper
Fanoos: Multi-Resolution, Multi-Strength, Interactive Explanations for Learned Systems
Remote
VMCAI
David Bayani
Carnegie Mellon University's School of Computer Science
,
Stefan Mitsch
Carnegie Mellon University, USA
14:00
30m
Paper
Bisimulations for Neural Network Reduction
InPerson
VMCAI
Pavithra Prabhakar
Kansas State University
15:05 - 16:35
Program Verification
VMCAI
at
Salon I
Chair(s):
Elizabeth Polgreen
University of Edinburgh
15:05
30m
Paper
High Assurance Software for Financial Regulation and Business Platforms
Remote
VMCAI
Stephen Goldbaum
Morgan Stanley
,
Attila Mihaly
Morgan Stanley
,
Tosha Ellison
Fintech Open Source Foundation
,
Earl Barr
UCL
,
Mark Marron
Microsoft Research
15:35
30m
Paper
Loop Verification with Invariants and Contracts
Remote
VMCAI
Gidon Ernst
Ludwig Maximilian University of Munich
Pre-print
16:05
30m
Paper
Making PROGRESS in Property Directed Reachability
Remote
VMCAI
Tobias Seufert
University of Freiburg
,
Christoph Scholl
University of Freiburg
,
Arun Chandrasekharan
OneSpin Solutions, Munich
,
Sven Reimer
OneSpin Solutions, Munich
,
Tobias Welp
OneSpin Solutions, Munich
Tue 18 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
09:00 - 10:00
Synthesis
VMCAI
at
Salon I
Chair(s):
Viktor Kunčak
EPFL, Switzerland
09:00
30m
Paper
Gradient-Descent for Randomized Controllers under Partial Observability
InPerson
VMCAI
Jip Spel
RWTH Aachen University
,
Linus Heck
RWTH Aachen University
,
Sebastian Junges
University of California, Berkeley
,
Joshua Moerman
Open University of the Netherlands
,
Joost-Pieter Katoen
RWTH Aachen University
09:30
30m
Paper
Satisfiability and Synthesis Modulo Oracles
Remote
VMCAI
Elizabeth Polgreen
University of Edinburgh
,
Andrew Reynolds
University of Iowa
,
Sanjit Seshia
UC Berkeley
10:20 - 11:50
Probabilistic Systems
VMCAI
at
Salon I
Chair(s):
Pavithra Prabhakar
Kansas State University
10:20
30m
Paper
Out of Control: Reducing Probabilistic Models by Control-State Elimination
InPerson
VMCAI
Tobias Winkler
RWTH Aachen University
,
Johannes Lehmann
RWTH Aachen University
,
Joost-Pieter Katoen
RWTH Aachen University
10:50
30m
Paper
STAMINA 2.0: Improving Scalability of Infinite-StateStochastic Model Checking
Remote
VMCAI
Riley Roberts
Utah State University
,
Thakur Neupane
The MathWorks, Inc.
,
Lukas Buecherl
University of Colorado, Boulder
,
Chris Myers
University of Colorado, Boulder
,
Zhen Zhang
Utah State University
11:20
30m
Paper
EPMC Gets Knowledge in Multi-Agent Systems
Remote
VMCAI
Chen Fu
Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences
,
Ernst Moritz Hahn
University of Twente
,
Yong Li
Institute of Software, Chinese Academy of Sciences
,
Sven Schewe
University of Liverpool
,
Meng Sun
Peking University
,
Andrea Turrini
State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
,
Lijun Zhang
Institute of Software, Chinese Academy of Sciences
13:30 - 14:30
Invited Talk
VMCAI
at
Salon I
Chair(s):
Bernd Finkbeiner
CISPA Helmholtz Center for Information Security
13:30
60m
Keynote
Simplifying Concurrent Programming via Synchronization Synthesis
Remote
VMCAI
Işıl Dillig
University of Texas at Austin
15:05 - 16:05
Static Analysis and Hybrid Systems
VMCAI
at
Salon I
Chair(s):
Yoni Zohar
Bar Ilan University
15:05
30m
Paper
Fast Three-Valued Abstract Bit-Vector Arithmetic
InPerson
VMCAI
Jan Onderka
Czech Technical University in Prague
,
Stefan Ratschan
The Czech Academy of Sciences
15:35
30m
Paper
Mixed Semantics Guided Layered Bounded Reachability Analysis of Compositional Linear Hybrid Automata
Remote
VMCAI
Yuming Wu
Nanjing University
,
Lei Bu
Nanjing University
,
Jiawan Wang
Nanjing University
,
Xinyue Ren
Nanjing University
,
Wen Xiong
Nanjing University
,
Xuandong Li
Nanjing University
Wed 19 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
08:50 - 09:00
Welcome
POPL
at
Salon I
Chair(s):
Rajeev Alur
University of Pennsylvania
,
Hongseok Yang
KAIST
09:00 - 10:00
Invited Talk
POPL
at
Salon I
Chair(s):
Rajeev Alur
University of Pennsylvania
09:00
60m
Keynote
Principles of Programming Language Translators
Remote
Invited Talk
POPL
Alfred V. Aho
Columbia University
10:20 - 12:00
Automated Verification
POPL
at
Salon I
Chair(s):
Roberto Giacobazzi
University of Verona
10:20
25m
Research paper
Software Model-Checking as Cyclic-Proof Search
Remote
POPL
Takeshi Tsukada
Chiba University
,
Hiroshi Unno
University of Tsukuba; RIKEN AIP
DOI
Media Attached
10:45
25m
Research paper
Induction Duality: Primal-Dual Search for Invariants
Remote
POPL
Oded Padon
VMware Research; Stanford University
,
James R. Wilcox
Certora
,
Jason R. Koenig
Stanford University
,
Kenneth L. McMillan
University of Texas at Austin
,
Alex Aiken
Stanford University
DOI
Media Attached
11:10
25m
Research paper
Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive Functions
Remote
POPL
Hari Govind V K
University of Waterloo
,
Sharon Shoham
Tel Aviv University
,
Arie Gurfinkel
University of Waterloo
DOI
Media Attached
11:35
25m
Research paper
Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables
Remote
POPL
Taolue Chen
Birkbeck University of London
,
Alejandro Flores Lamas
Royal Holloway University of London
,
Matthew Hague
Royal Holloway University of London
,
Zhilei Han
Tsinghua University
,
Denghang Hu
Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences
,
Shuanglong Kan
TU Kaiserslautern
,
Anthony Widjaja Lin
TU Kaiserslautern; MPI-SWS
,
Philipp Ruemmer
Uppsala University
,
Zhilin Wu
Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences
DOI
Media Attached
13:30 - 14:45
Program Analysis
POPL
at
Salon I
Chair(s):
Gagandeep Singh
University of Illinois at Urbana-Champaign; VMware
13:30
25m
Research paper
Property-Directed Reachability as Abstract Interpretation in the Monotone Theory
Remote
POPL
Yotam M. Y. Feldman
Tel Aviv University
,
Mooly Sagiv
Tel Aviv University
,
Sharon Shoham
Tel Aviv University
,
James R. Wilcox
Certora
DOI
Media Attached
13:55
25m
Research paper
Partial (In)Completeness in Abstract Interpretation: Limiting the Imprecision in Program Analysis
InPerson
POPL
Marco Campion
University of Verona
,
Mila Dalla Preda
University of Verona
,
Roberto Giacobazzi
University of Verona
DOI
Media Attached
14:20
25m
Research paper
Return of CFA: Call-Site Sensitivity Can Be Superior to Object Sensitivity Even for Object-Oriented Programs
InPerson
POPL
Minseok Jeon
Korea University
,
Hakjoo Oh
Korea University
DOI
Media Attached
15:05 - 16:20
Algorithmic Verification 1
POPL
at
Salon I
Chair(s):
Qirun Zhang
Georgia Institute of Technology
15:05
25m
Research paper
Efficient Algorithms for Dynamic Bidirected Dyck-Reachability
Remote
POPL
Yuanbo Li
Georgia Institute of Technology
,
Kris Satya
Georgia Institute of Technology
,
Qirun Zhang
Georgia Institute of Technology
DOI
Media Attached
15:30
25m
Research paper
The Decidability and Complexity of Interleaved Bidirected Dyck Reachability
Remote
POPL
Adam Husted Kjelstrøm
Aarhus University
,
Andreas Pavlogiannis
Aarhus University
DOI
Media Attached
15:55
25m
Research paper
Subcubic Certificates for CFL Reachability
Remote
POPL
Dmitry Chistikov
University of Warwick
,
Rupak Majumdar
MPI-SWS
,
Philipp Schepper
CISPA
DOI
Media Attached
16:40 - 17:30
Algorithmic Verification 2
POPL
at
Salon I
Chair(s):
Qirun Zhang
Georgia Institute of Technology
16:40
25m
Research paper
Context-Bounded Verification of Thread Pools
Remote
POPL
Pascal Baumann
MPI-SWS
,
Rupak Majumdar
MPI-SWS
,
Ramanathan S. Thinniyam
MPI-SWS
,
Georg Zetzsche
MPI-SWS
DOI
Media Attached
17:05
25m
Research paper
What’s Decidable about Linear Loops?
InPerson
POPL
Toghrul Karimov
MPI-SWS
,
Engel Lefaucheux
MPI-SWS
,
Joël Ouaknine
MPI-SWS
,
David Purser
MPI-SWS
,
Anton Varonka
MPI-SWS
,
Markus A. Whiteland
MPI-SWS
,
James Worrell
University of Oxford
DOI
Pre-print
Media Attached
Thu 20 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
09:00 - 10:00
Invited Talk
POPL
at
Salon I
Chair(s):
Michael Hicks
University of Maryland at College Park
09:00
60m
Keynote
Better Learning through Programming Languages
Invited Talk
InPerson
POPL
Armando Solar-Lezama
Massachusetts Institute of Technology
10:20 - 12:00
Foundation and Verification of Machine-Learning Systems
POPL
at
Salon I
Chair(s):
Gilbert Bernstein
University of California at Berkeley
10:20
25m
Research paper
A Dual Number Abstraction for Static Analysis of Clarke Jacobians
InPerson
POPL
Jacob Laurel
University of Illinois at Urbana-Champaign
,
Rem Yang
University of Illinois at Urbana-Champaign
,
Gagandeep Singh
University of Illinois at Urbana-Champaign; VMware
,
Sasa Misailovic
University of Illinois at Urbana-Champaign
DOI
Media Attached
10:45
25m
Research paper
Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation
Remote
POPL
Faustyna Krawiec
University of Cambridge
,
Simon Peyton Jones
Microsoft Research
,
Neel Krishnaswami
University of Cambridge
,
Tom Ellis
Microsoft Research
,
Richard A. Eisenberg
Tweag
,
Andrew Fitzgibbon
Graphcore
DOI
Media Attached
11:10
25m
Research paper
Interval Universal Approximation for Neural Networks
InPerson
POPL
Zi Wang
University of Wisconsin-Madison
,
Aws Albarghouthi
University of Wisconsin-Madison
,
Gautam Prakriya
Chinese University of Hong Kong
,
Somesh Jha
University of Wisconsin
DOI
Media Attached
11:35
25m
Research paper
PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations
InPerson
POPL
Mark Niklas Müller
ETH Zurich
,
Gleb Makarchuk
ETH Zurich
,
Gagandeep Singh
University of Illinois at Urbana-Champaign; VMware
,
Markus Püschel
ETH Zurich
,
Martin Vechev
ETH Zurich
DOI
Media Attached
13:30 - 14:45
Types
POPL
at
Salon I
Chair(s):
Stephanie Weirich
University of Pennsylvania
13:30
25m
Research paper
On Type-Cases, Union Elimination, and Occurrence Typing
InPerson
POPL
Giuseppe Castagna
CNRS; Université de Paris
,
Mickaël Laurent
Université de Paris
,
Kim Nguyễn
Université Paris-Saclay
,
Matthew Lutze
Université de Paris
DOI
Media Attached
13:55
25m
Research paper
Oblivious Algebraic Data Types
InPerson
POPL
Qianchuan Ye
Purdue University
,
Benjamin Delaware
Purdue University
DOI
Media Attached
14:20
25m
Research paper
SolType: Refinement Types for Arithmetic Overflow in Solidity
Remote
POPL
Bryan Tan
University of California at Santa Barbara
,
Benjamin Mariano
University of Texas at Austin
,
Shuvendu K. Lahiri
Microsoft Research
,
Işıl Dillig
University of Texas at Austin
,
Yu Feng
University of California at Santa Barbara
DOI
Media Attached
15:05 - 16:20
Systems
POPL
at
Salon I
Chair(s):
Arthur Azevedo de Amorim
Boston University
15:05
25m
Research paper
Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI
InPerson
POPL
Matthew Kolosick
University of California at San Diego
,
Shravan Ravi Narayan
University of California at San Diego
,
Evan Johnson
University of California at San Diego
,
Conrad Watt
University of Cambridge
,
Michael LeMay
Intel Labs
,
Deepak Garg
MPI-SWS
,
Ranjit Jhala
University of California at San Diego
,
Deian Stefan
University of California at San Diego
DOI
Media Attached
15:30
25m
Research paper
Relational E-matching
Remote
POPL
Yihong Zhang
University of Washington
,
Yisu Remy Wang
University of Washington
,
Max Willsey
University of Washington
,
Zachary Tatlock
University of Washington
DOI
Media Attached
15:55
25m
Research paper
Linked Visualisations via Galois Dependencies
Remote
POPL
Roly Perera
Alan Turing Institute
,
Minh Nguyen
University of Bristol
,
Tomas Petricek
University of Kent
,
Meng Wang
University of Bristol
DOI
Media Attached
16:40 - 18:00
POPL Business Meeting and SIGPLAN Awards
POPL
at
Salon I
Chair(s):
Rajeev Alur
University of Pennsylvania
16:40
10m
Meeting
General Chair Report
InPerson
POPL
Rajeev Alur
University of Pennsylvania
16:50
10m
Meeting
Program Chair Report
Remote
POPL
Hongseok Yang
KAIST
17:00
10m
Meeting
Virtualization Chair Report
Remote
POPL
Adam Chlipala
Massachusetts Institute of Technology
17:10
5m
Meeting
POPL 2023 Report
InPerson
POPL
Andrew Myers
Cornell University
17:15
3m
Awards
Student Research Competition Winners
Remote
POPL
Azalea Raad
Imperial College London
17:18
3m
Awards
POPL'22 Distinguished Papers
Remote
POPL
Hongseok Yang
KAIST
17:21
3m
Awards
SIGPLAN Reynolds Dissertation Award
Remote
POPL
Işıl Dillig
University of Texas at Austin
17:24
3m
Awards
POPL Most Influential Paper Award
Remote
POPL
Tony Hosking
Australian National University
17:27
3m
Awards
SIGPLAN Programming Languages Achievements Award
Remote
POPL
Işıl Dillig
University of Texas at Austin
17:30
10m
Awards
Remarks by SIGPLAN PL Achievements Award Winner
Remote
POPL
17:40
20m
Meeting
Open Forum for Q&A
InPerson
POPL
Rajeev Alur
University of Pennsylvania
Fri 21 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
09:00 - 10:00
Invited Talk
POPL
at
Salon I
Chair(s):
Adam Chlipala
Massachusetts Institute of Technology
09:00
60m
Keynote
Coalgebra for the working programming languages researcher
Remote
Invited Talk
POPL
Alexandra Silva
Cornell University
10:20 - 12:00
Distributed or Network Programs
POPL
at
Salon I
Chair(s):
J. Garrett Morris
The University of Iowa
10:20
25m
Research paper
Pirouette: Higher-Order Typed Functional Choreographies
Distinguished Paper
InPerson
POPL
Andrew K. Hirsch
MPI-SWS
,
Deepak Garg
MPI-SWS
DOI
Media Attached
10:45
25m
Research paper
Fair Termination of Binary Sessions
Remote
POPL
Luca Ciccone
University of Turin
,
Luca Padovani
University of Turin
DOI
Media Attached
11:10
25m
Research paper
Safe, Modular Packet Pipeline Programming
Remote
POPL
Devon Loehr
Princeton University
,
David Walker
Princeton University
DOI
Media Attached
11:35
25m
Research paper
Dependently-Typed Data Plane Programming
Remote
POPL
Matthias Eichholz
TU Darmstadt
,
Eric Campbell
Cornell University
,
Matthias Krebs
TU Darmstadt
,
Nate Foster
Cornell University
,
Mira Mezini
TU Darmstadt
DOI
Media Attached
12:30 - 13:30
ShutdownPL
Diversity, Equity and Inclusion
at
Salon I
Chair(s):
David Justo
Microsoft Azure
12:30
60m
Talk
Designing and Developing for the Black Experience
Remote
Diversity, Equity and Inclusion
Brittany Johnson
George Mason University
13:30 - 14:45
TOPLAS Session
POPL
at
Salon I
Chair(s):
Andrew Myers
Cornell University
13:30
25m
Talk
Armed cats: formal concurrency modelling at Arm
Remote
POPL
Jade Alglave
University College London
,
Will Deacon
ARM Ltd.
,
Richard Grisenthwaite
,
Antoine Hacquard
EPITA, LRDE
,
Luc Maranget
Inria
13:55
25m
Talk
TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs
Remote
POPL
Emanuele D’Osualdo
MPI-SWS
,
Julian Sutherland
Imperial College London
,
Azadeh Farzan
University of Toronto
,
Philippa Gardner
Imperial College London
DOI
14:20
25m
Talk
Gradualizing the Calculus of Inductive Constructions
Remote
POPL
Meven Lennon-Bertrand
Inria – LS2N, Université de Nantes
,
Kenji Maillard
Inria Nantes & University of Chile
,
Nicolas Tabareau
Inria
,
Éric Tanter
University of Chile
15:05 - 16:20
Verification 1
POPL
at
Salon I
Chair(s):
Lennart Beringer
Princeton University
15:05
25m
Research paper
Certifying Derivation of State Machines from Coroutines
InPerson
POPL
Mirai Ikebuchi
National Institute of Informatics
,
Andres Erbsen
Massachusetts Institute of Technology
,
Adam Chlipala
Massachusetts Institute of Technology
DOI
Media Attached
15:30
25m
Research paper
VIP: Verifying Real-World C Idioms with Integer-Pointer Casts
Remote
POPL
Rodolphe Lepigre
MPI-SWS
,
Michael Sammler
MPI-SWS
,
Kayvan Memarian
University of Cambridge
,
Robbert Krebbers
Radboud University Nijmegen
,
Derek Dreyer
MPI-SWS
,
Peter Sewell
University of Cambridge
DOI
Media Attached
15:55
25m
Research paper
Verified Compilation of C Programs with a Nominal Memory Model
Remote
POPL
Yuting Wang
Shanghai Jiao Tong University
,
Ling Zhang
Shanghai Jiao Tong University
,
Zhong Shao
Yale University
,
Jérémie Koenig
Yale University
DOI
Media Attached
16:40 - 17:30
Verification 2
POPL
at
Salon I
Chair(s):
Jonathan Protzenko
Microsoft Research, Redmond
16:40
25m
Research paper
Verified Tensor-Program Optimization Via High-Level Scheduling Rewrites
Remote
POPL
Amanda Liu
Massachusetts Institute of Technology
,
Gilbert Bernstein
University of California at Berkeley
,
Adam Chlipala
Massachusetts Institute of Technology
,
Jonathan Ragan-Kelley
Massachusetts Institute of Technology
DOI
Media Attached
17:05
25m
Research paper
One Polynomial Approximation to Produce Correctly Rounded Results of an Elementary Function for Multiple Representations and Rounding Modes
Distinguished Paper
Remote
POPL
Jay P. Lim
Rutgers University
,
Santosh Nagarakatte
Rutgers University
DOI
Media Attached
Sat 22 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
09:00 - 10:00
Invited Talk I
CoqPL
at
Salon I
Chair(s):
Benjamin C. Pierce
University of Pennsylvania
09:00
60m
Keynote
Coq meets literate programming: tools for documenting, preserving, and sharing mechanized proofs
Remote
CoqPL
I:
Clément Pit-Claudel
MIT / AWS
10:20 - 12:00
Contributed Talks (Morning)
CoqPL
at
Salon I
Chair(s):
Benjamin C. Pierce
University of Pennsylvania
10:20
20m
Talk
A Visual Ltac Debugger in CoqIDE
Remote
CoqPL
S:
Jim Fehrle
None
File Attached
10:40
20m
Talk
Scrap your boilerplate definitions in 10 lines of Ltac!
InPerson
CoqPL
S:
Qianchuan Ye
Purdue University
,
Benjamin Delaware
Purdue University
File Attached
11:00
20m
Talk
Tealeaves: Categorical structures for syntax
InPerson
CoqPL
S:
Lawrence Dunn
University of Pennsylvania
,
Steve Zdancewic
University of Pennsylvania
,
Val Tannen
University of Pennsylvania, USA
File Attached
11:20
20m
Talk
Towards a Formalization of Nominal Sets in Coq
Remote
CoqPL
S:
Fabrício S. Paranhos
Universidade Federal de Goiás
,
Daniel Ventura
Universidade Federal de Goiás
File Attached
11:40
20m
Talk
A Case for Lightweight Interfaces in Coq
InPerson
CoqPL
David Swasey
BedRock Systems
,
Paolo G. Giarrusso
BedRock Systems
,
S:
Gregory Malecha
BedRock Systems
File Attached
13:30 - 14:30
Invited Talk II
CoqPL
at
Salon I
Chair(s):
Amin Timany
Aarhus University
13:30
60m
Keynote
Verifying Concurrent, Crash-Safe Systems with Perennial
Remote
CoqPL
I:
Joseph Tassarotti
Boston College
14:30 - 14:50
Contributed Talk (Afternoon)
CoqPL
at
Salon I
Chair(s):
Amin Timany
Aarhus University
14:30
20m
Talk
A Verified Pipeline from a Specification Language to Optimized, Safe Rust
Remote
CoqPL
S:
Rasmus Holdsbjerg-Larsen
Aarhus University
,
Bas Spitters
Aarhus University
,
Mikkel Milo
Concordium Blockchain Research Center, Aarhus University
Pre-print
File Attached
15:05 - 15:50
Session with the Coq Development Team
CoqPL
at
Salon I
Chair(s):
Amin Timany
Aarhus University
15:05
45m
Panel
Session with the Coq Development Team
Remote
CoqPL
S:
Matthieu Sozeau
Inria
,
S:
Yves Bertot
INRIA
,
S:
Hugo Herbelin
,
S:
Emilio Jesús Gallego Arias
INRIA
,
S:
Jason Gross
MIT CSAIL
Sun 16 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
Salon I
VMCAI
Invited Talk
VMCAI
Static Analysis and Abstract Interpretation
VMCAI
Privacy and Security
VMCAI
Satisfiability Modulo Theories
Mon 17 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
Salon I
VMCAI
Invited Talk
VMCAI
Model Checking
VMCAI
Formal Methods in Machine Learning
VMCAI
Program Verification
Tue 18 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
Salon I
VMCAI
Synthesis
VMCAI
Probabilistic Systems
VMCAI
Invited Talk
VMCAI
Static Analysis and Hybrid Systems
Wed 19 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
8:00
30
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Salon I
POPL
Welcome
POPL
Invited Talk
POPL
Automated Verification
POPL
Program Analysis
POPL
Algorithmic Verification 1
POPL
Algorithmic Verification 2
Thu 20 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Salon I
POPL
Invited Talk
POPL
Foundation and Verification of Machine-Learning Systems
POPL
Types
POPL
Systems
POPL
POPL Business Meeting and SIGPLAN Awards
Fri 21 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Salon I
POPL
Invited Talk
POPL
Distributed or Network Programs
Diversity, Equity and Inclusion
ShutdownPL
POPL
TOPLAS Session
POPL
Verification 1
POPL
Verification 2
Sat 22 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
Salon I
CoqPL
Invited Talk I
CoqPL
Contributed Talks (Morning)
CoqPL
Invited Talk II
CoqPL
Contributed Talk (Afternoon)
CoqPL
Session with the Coq Development Team
Sun 16 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
Salon I
VMCAI
Remote
Sequential Information Flow
09:00 - 10:00
VMCAI
Remote
Relational String Abstract Domains
10:20 - 10:50
VMCAI
InPerson
Lightweight Shape Analysis based on Physical Types
10:50 - 11:20
VMCAI
Remote
A Flow-Insensitive-Complete Program Representation
11:20 - 11:50
VMCAI
Remote
Verifying Pufferfish Privacy in Hidden Markov Models
13:30 - 14:00
VMCAI
Remote
Verifying Solidity Smart Contracts Via Communication Abstraction in Sma ...
14:00 - 14:30
VMCAI
Remote
Generalized Arrays for Stainless Frames
15:05 - 15:35
VMCAI
InPerson
NP Satisfiability for Arrays as Powers
15:35 - 16:05
VMCAI
Remote
Bit-Precise Reasoning via Int-Blasting
16:05 - 16:35
Mon 17 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
Salon I
VMCAI
Remote
Back to the Future: A Fresh Look at Linear Temporal Logic
09:00 - 10:00
VMCAI
Remote
Automata-Driven Partial Order Reduction and Guided Search for LTL Model ...
10:20 - 10:50
VMCAI
Remote
Stateful Dynamic Partial Order Reduction for Model Checking Event-Drive ...
10:50 - 11:20
VMCAI
InPerson
Scaling Up Livelock Verification for Network-on-Chip Routing Algorithms
11:20 - 11:50
VMCAI
Remote
Fanoos: Multi-Resolution, Multi-Strength, Interactive Explanations for ...
13:30 - 14:00
VMCAI
InPerson
Bisimulations for Neural Network Reduction
14:00 - 14:30
VMCAI
Remote
High Assurance Software for Financial Regulation and Business Platforms
15:05 - 15:35
VMCAI
Remote
Loop Verification with Invariants and Contracts
15:35 - 16:05
VMCAI
Remote
Making PROGRESS in Property Directed Reachability
16:05 - 16:35
Tue 18 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
Salon I
VMCAI
InPerson
Gradient-Descent for Randomized Controllers under Partial Observability
09:00 - 09:30
VMCAI
Remote
Satisfiability and Synthesis Modulo Oracles
09:30 - 10:00
VMCAI
InPerson
Out of Control: Reducing Probabilistic Models by Control-State Elimination
10:20 - 10:50
VMCAI
Remote
STAMINA 2.0: Improving Scalability of Infinite-StateStochastic Model Ch ...
10:50 - 11:20
VMCAI
Remote
EPMC Gets Knowledge in Multi-Agent Systems
11:20 - 11:50
VMCAI
Remote
Simplifying Concurrent Programming via Synchronization Synthesis
13:30 - 14:30
VMCAI
InPerson
Fast Three-Valued Abstract Bit-Vector Arithmetic
15:05 - 15:35
VMCAI
Remote
Mixed Semantics Guided Layered Bounded Reachability Analysis of Composi ...
15:35 - 16:05
Wed 19 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Salon I
POPL
Remote
Invited Talk
Principles of Programming Language Translators
09:00 - 10:00
POPL
Remote
Software Model-Checking as Cyclic-Proof Search
10:20 - 10:45
POPL
Remote
Induction Duality: Primal-Dual Search for Invariants
10:45 - 11:10
POPL
Remote
Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recurs ...
11:10 - 11:35
POPL
Remote
Solving String Constraints with Regex-Dependent Functions through Trans ...
11:35 - 12:00
POPL
Remote
Property-Directed Reachability as Abstract Interpretation in the Monoto ...
13:30 - 13:55
POPL
InPerson
Partial (In)Completeness in Abstract Interpretation: Limiting the Impre ...
13:55 - 14:20
POPL
InPerson
Return of CFA: Call-Site Sensitivity Can Be Superior to Object Sensitiv ...
14:20 - 14:45
POPL
Remote
Efficient Algorithms for Dynamic Bidirected Dyck-Reachability
15:05 - 15:30
POPL
Remote
The Decidability and Complexity of Interleaved Bidirected Dyck Reachability
15:30 - 15:55
POPL
Remote
Subcubic Certificates for CFL Reachability
15:55 - 16:20
POPL
Remote
Context-Bounded Verification of Thread Pools
16:40 - 17:05
POPL
InPerson
What’s Decidable about Linear Loops?
17:05 - 17:30
Thu 20 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Salon I
POPL
Invited Talk
InPerson
Better Learning through Programming Languages
09:00 - 10:00
POPL
InPerson
A Dual Number Abstraction for Static Analysis of Clarke Jacobians
10:20 - 10:45
POPL
Remote
Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode A ...
10:45 - 11:10
POPL
InPerson
Interval Universal Approximation for Neural Networks
11:10 - 11:35
POPL
InPerson
PRIMA: General and Precise Neural Network Certification via Scalable Co ...
11:35 - 12:00
POPL
InPerson
On Type-Cases, Union Elimination, and Occurrence Typing
13:30 - 13:55
POPL
InPerson
Oblivious Algebraic Data Types
13:55 - 14:20
POPL
Remote
SolType: Refinement Types for Arithmetic Overflow in Solidity
14:20 - 14:45
POPL
InPerson
Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly ...
15:05 - 15:30
POPL
Remote
Relational E-matching
15:30 - 15:55
POPL
Remote
Linked Visualisations via Galois Dependencies
15:55 - 16:20
POPL
InPerson
General Chair Report
16:40 - 16:50
POPL
Remote
Program Chair Report
16:50 - 17:00
POPL
Remote
Virtualization Chair Report
17:00 - 17:10
POPL
InPerson
POPL 2023 Report
17:10 - 17:15
POPL
Remote
Student Research Competition Winners
17:15 - 17:18
POPL
Remote
POPL'22 Distinguished Papers
17:18 - 17:21
POPL
Remote
SIGPLAN Reynolds Dissertation Award
17:21 - 17:24
POPL
Remote
POPL Most Influential Paper Award
17:24 - 17:27
POPL
Remote
SIGPLAN Programming Languages Achievements Award
17:27 - 17:30
POPL
Remote
Remarks by SIGPLAN PL Achievements Award Winner
17:30 - 17:40
POPL
InPerson
Open Forum for Q&A
17:40 - 18:00
Fri 21 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Salon I
POPL
Remote
Invited Talk
Coalgebra for the working programming languages researcher
09:00 - 10:00
POPL
Distinguished Paper
InPerson
Pirouette: Higher-Order Typed Functional Choreographies
10:20 - 10:45
POPL
Remote
Fair Termination of Binary Sessions
10:45 - 11:10
POPL
Remote
Safe, Modular Packet Pipeline Programming
11:10 - 11:35
POPL
Remote
Dependently-Typed Data Plane Programming
11:35 - 12:00
POPL Diversity, Equity and Inclusion
Remote
Designing and Developing for the Black Experience
12:30 - 13:30
POPL
Remote
Armed cats: formal concurrency modelling at Arm
13:30 - 13:55
POPL
Remote
TaDA Live: Compositional Reasoning for Termination of Fine-grained Conc ...
13:55 - 14:20
POPL
Remote
Gradualizing the Calculus of Inductive Constructions
14:20 - 14:45
POPL
InPerson
Certifying Derivation of State Machines from Coroutines
15:05 - 15:30
POPL
Remote
VIP: Verifying Real-World C Idioms with Integer-Pointer Casts
15:30 - 15:55
POPL
Remote
Verified Compilation of C Programs with a Nominal Memory Model
15:55 - 16:20
POPL
Remote
Verified Tensor-Program Optimization Via High-Level Scheduling Rewrites
16:40 - 17:05
POPL
Distinguished Paper
Remote
One Polynomial Approximation to Produce Correctly Rounded Results of an ...
17:05 - 17:30
Sat 22 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
Salon I
CoqPL
Remote
Coq meets literate programming: tools for documenting, preserving, and ...
09:00 - 10:00
CoqPL
Remote
A Visual Ltac Debugger in CoqIDE
10:20 - 10:40
CoqPL
InPerson
Scrap your boilerplate definitions in 10 lines of Ltac!
10:40 - 11:00
CoqPL
InPerson
Tealeaves: Categorical structures for syntax
11:00 - 11:20
CoqPL
Remote
Towards a Formalization of Nominal Sets in Coq
11:20 - 11:40
CoqPL
InPerson
A Case for Lightweight Interfaces in Coq
11:40 - 12:00
CoqPL
Remote
Verifying Concurrent, Crash-Safe Systems with Perennial
13:30 - 14:30
CoqPL
Remote
A Verified Pipeline from a Specification Language to Optimized, Safe Rust
14:30 - 14:50
CoqPL
Remote
Session with the Coq Development Team
15:05 - 15:50
x
Sun 3 Nov 23:43