WITS 2022
Sat 22 Jan 2022
Philadelphia, Pennsylvania, United States
co-located with
POPL 2022
Toggle navigation
Attending
Hotel: Westin Philadelphia
Program
Complete Program
Your Program
Sat 22 Jan
Track/Call
Organization
WITS 2022 Committees
Track Committees
Program Committee
Contributors
People Index
Search
Series
Series
WITS 2024
WITS 2022
Sign in
Sign up
POPL 2022
(
series
) /
WITS 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 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
POPL 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
POPL 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
POPL 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
Tue 7 May 00:39