Salon I - POPL 2022

VenueWestin Philadelphia

Room nameSalon I

Room InformationNo extra information available

Program

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

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 programSpecify 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 TalkVMCAI at Salon I Chair(s): Thomas Wies New York University

09:00 60m Keynote		Sequential Information FlowRemote VMCAI Thomas A. Henzinger IST Austria, Austria

10:20 - 11:50	Static Analysis and Abstract InterpretationVMCAI at Salon I Chair(s): Thomas Wies New York University

10:20 30m Paper		Relational String Abstract DomainsRemote 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 TypesInPerson 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 RepresentationRemote VMCAI Solène Mirliaz ENS Rennes / IRISA / Inria, David Pichardie Facebook Paris

13:30 - 14:30	Privacy and SecurityVMCAI 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 ModelsRemote 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 SmartACERemote 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 TheoriesVMCAI at Salon I Chair(s): Natarajan Shankar SRI International, USA

15:05 30m Paper		Generalized Arrays for Stainless FramesRemote VMCAI Georg Stefan Schmid EPFL, Switzerland, Viktor Kunčak EPFL, Switzerland
15:35 30m Paper		NP Satisfiability for Arrays as PowersInPerson VMCAI Rodrigo Raya EPFL, Viktor Kunčak EPFL, Switzerland
16:05 30m Paper		Bit-Precise Reasoning via Int-BlastingRemote 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 TalkVMCAI 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 LogicRemote VMCAI Javier Esparza

10:20 - 11:50	Model CheckingVMCAI 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 CheckingRemote 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 TerminateRemote 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 AlgorithmsInPerson VMCAI Landon Taylor Utah State University, Zhen Zhang Utah State University

13:30 - 14:30	Formal Methods in Machine LearningVMCAI at Salon I Chair(s): Rupak Majumdar MPI-SWS

13:30 30m Paper		Fanoos: Multi-Resolution, Multi-Strength, Interactive Explanations for Learned SystemsRemote 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 ReductionInPerson VMCAI Pavithra Prabhakar Kansas State University

15:05 - 16:35	Program VerificationVMCAI at Salon I Chair(s): Elizabeth Polgreen University of Edinburgh

15:05 30m Paper		High Assurance Software for Financial Regulation and Business PlatformsRemote 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 ContractsRemote VMCAI Gidon Ernst Ludwig Maximilian University of Munich Pre-print
16:05 30m Paper		Making PROGRESS in Property Directed ReachabilityRemote 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	SynthesisVMCAI at Salon I Chair(s): Viktor Kunčak EPFL, Switzerland

09:00 30m Paper		Gradient-Descent for Randomized Controllers under Partial ObservabilityInPerson 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 OraclesRemote VMCAI Elizabeth Polgreen University of Edinburgh, Andrew Reynolds University of Iowa, Sanjit Seshia UC Berkeley

10:20 - 11:50	Probabilistic SystemsVMCAI at Salon I Chair(s): Pavithra Prabhakar Kansas State University

10:20 30m Paper		Out of Control: Reducing Probabilistic Models by Control-State EliminationInPerson 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 CheckingRemote 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 SystemsRemote 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 TalkVMCAI at Salon I Chair(s): Bernd Finkbeiner CISPA Helmholtz Center for Information Security

13:30 60m Keynote		Simplifying Concurrent Programming via Synchronization SynthesisRemote VMCAI Işıl Dillig University of Texas at Austin

15:05 - 16:05	Static Analysis and Hybrid SystemsVMCAI at Salon I Chair(s): Yoni Zohar Bar Ilan University

15:05 30m Paper		Fast Three-Valued Abstract Bit-Vector ArithmeticInPerson 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 AutomataRemote 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	WelcomePOPL at Salon I Chair(s): Rajeev Alur University of Pennsylvania, Hongseok Yang KAIST

09:00 - 10:00	Invited TalkPOPL at Salon I Chair(s): Rajeev Alur University of Pennsylvania

09:00 60m Keynote		Principles of Programming Language TranslatorsRemoteInvited Talk POPL Alfred V. Aho Columbia University

10:20 - 12:00	Automated VerificationPOPL at Salon I Chair(s): Roberto Giacobazzi University of Verona

10:20 25m Research paper		Software Model-Checking as Cyclic-Proof SearchRemote 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 InvariantsRemote 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 FunctionsRemote 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 VariablesRemote 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 AnalysisPOPL 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 TheoryRemote 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 AnalysisInPerson 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 ProgramsInPerson POPL Minseok Jeon Korea University, Hakjoo Oh Korea University DOI Media Attached

15:05 - 16:20	Algorithmic Verification 1POPL at Salon I Chair(s): Qirun Zhang Georgia Institute of Technology

15:05 25m Research paper		Efficient Algorithms for Dynamic Bidirected Dyck-ReachabilityRemote 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 ReachabilityRemote POPL Adam Husted Kjelstrøm Aarhus University, Andreas Pavlogiannis Aarhus University DOI Media Attached
15:55 25m Research paper		Subcubic Certificates for CFL ReachabilityRemote POPL Dmitry Chistikov University of Warwick, Rupak Majumdar MPI-SWS, Philipp Schepper CISPA DOI Media Attached

16:40 - 17:30	Algorithmic Verification 2POPL at Salon I Chair(s): Qirun Zhang Georgia Institute of Technology

16:40 25m Research paper		Context-Bounded Verification of Thread PoolsRemote 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 TalkPOPL at Salon I Chair(s): Michael Hicks University of Maryland at College Park

09:00 60m Keynote		Better Learning through Programming LanguagesInvited TalkInPerson POPL Armando Solar-Lezama Massachusetts Institute of Technology

10:20 - 12:00	Foundation and Verification of Machine-Learning SystemsPOPL 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 JacobiansInPerson 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 DifferentiationRemote 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 NetworksInPerson 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 ApproximationsInPerson 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	TypesPOPL at Salon I Chair(s): Stephanie Weirich University of Pennsylvania

13:30 25m Research paper		On Type-Cases, Union Elimination, and Occurrence TypingInPerson 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 TypesInPerson POPL Qianchuan Ye Purdue University, Benjamin Delaware Purdue University DOI Media Attached
14:20 25m Research paper		SolType: Refinement Types for Arithmetic Overflow in SolidityRemote 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	SystemsPOPL 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 SFIInPerson 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-matchingRemote 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 DependenciesRemote 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 AwardsPOPL at Salon I Chair(s): Rajeev Alur University of Pennsylvania

16:40 10m Meeting		General Chair ReportInPerson POPL Rajeev Alur University of Pennsylvania
16:50 10m Meeting		Program Chair ReportRemote POPL Hongseok Yang KAIST
17:00 10m Meeting		Virtualization Chair ReportRemote POPL Adam Chlipala Massachusetts Institute of Technology
17:10 5m Meeting		POPL 2023 ReportInPerson POPL Andrew Myers Cornell University
17:15 3m Awards		Student Research Competition WinnersRemote POPL Azalea Raad Imperial College London
17:18 3m Awards		POPL'22 Distinguished PapersRemote POPL Hongseok Yang KAIST
17:21 3m Awards		SIGPLAN Reynolds Dissertation AwardRemote POPL Işıl Dillig University of Texas at Austin
17:24 3m Awards		POPL Most Influential Paper AwardRemote POPL Tony Hosking Australian National University
17:27 3m Awards		SIGPLAN Programming Languages Achievements AwardRemote POPL Işıl Dillig University of Texas at Austin
17:30 10m Awards		Remarks by SIGPLAN PL Achievements Award WinnerRemote POPL
17:40 20m Meeting		Open Forum for Q&AInPerson POPL Rajeev Alur University of Pennsylvania

Fri 21 Jan
Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:00	Invited TalkPOPL at Salon I Chair(s): Adam Chlipala Massachusetts Institute of Technology

09:00 60m Keynote		Coalgebra for the working programming languages researcherRemoteInvited Talk POPL Alexandra Silva Cornell University

10:20 - 12:00	Distributed or Network ProgramsPOPL at Salon I Chair(s): J. Garrett Morris The University of Iowa

10:20 25m Research paper		Pirouette: Higher-Order Typed Functional ChoreographiesDistinguished PaperInPerson POPL Andrew K. Hirsch MPI-SWS, Deepak Garg MPI-SWS DOI Media Attached
10:45 25m Research paper		Fair Termination of Binary SessionsRemote POPL Luca Ciccone University of Turin, Luca Padovani University of Turin DOI Media Attached
11:10 25m Research paper		Safe, Modular Packet Pipeline ProgrammingRemote POPL Devon Loehr Princeton University, David Walker Princeton University DOI Media Attached
11:35 25m Research paper		Dependently-Typed Data Plane ProgrammingRemote 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	ShutdownPLDiversity, Equity and Inclusion at Salon I Chair(s): David Justo Microsoft Azure

12:30 60m Talk		Designing and Developing for the Black ExperienceRemote Diversity, Equity and Inclusion Brittany Johnson George Mason University

13:30 - 14:45	TOPLAS SessionPOPL at Salon I Chair(s): Andrew Myers Cornell University

13:30 25m Talk		Armed cats: formal concurrency modelling at ArmRemote 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 ConstructionsRemote 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 1POPL at Salon I Chair(s): Lennart Beringer Princeton University

15:05 25m Research paper		Certifying Derivation of State Machines from CoroutinesInPerson 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 CastsRemote 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 ModelRemote 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 2POPL at Salon I Chair(s): Jonathan Protzenko Microsoft Research, Redmond

16:40 25m Research paper		Verified Tensor-Program Optimization Via High-Level Scheduling RewritesRemote 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 ModesDistinguished PaperRemote 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 ICoqPL 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 proofsRemote 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 CoqIDERemote 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 syntaxInPerson 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 CoqRemote 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 CoqInPerson CoqPL David Swasey BedRock Systems, Paolo G. Giarrusso BedRock Systems, S: Gregory Malecha BedRock Systems File Attached

13:30 - 14:30	Invited Talk IICoqPL at Salon I Chair(s): Amin Timany Aarhus University

13:30 60m Keynote		Verifying Concurrent, Crash-Safe Systems with PerennialRemote 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 RustRemote 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 TeamCoqPL at Salon I Chair(s): Amin Timany Aarhus University

15:05 45m Panel		Session with the Coq Development TeamRemote 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	VMCAIRemote Sequential Information Flow 09:00 - 10:00																VMCAIRemote Relational String Abstract Domains 10:20 - 10:50						VMCAIInPerson Lightweight Shape Analysis based on Physical Types 10:50 - 11:20						VMCAIRemote A Flow-Insensitive-Complete Program Representation 11:20 - 11:50																										VMCAIRemote Verifying Pufferfish Privacy in Hidden Markov Models 13:30 - 14:00						VMCAIRemote Verifying Solidity Smart Contracts Via Communication Abstraction in Sma ... 14:00 - 14:30													VMCAIRemote Generalized Arrays for Stainless Frames 15:05 - 15:35						VMCAIInPerson NP Satisfiability for Arrays as Powers 15:35 - 16:05						VMCAIRemote 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	VMCAIRemote Back to the Future: A Fresh Look at Linear Temporal Logic 09:00 - 10:00																VMCAIRemote Automata-Driven Partial Order Reduction and Guided Search for LTL Model ... 10:20 - 10:50						VMCAIRemote Stateful Dynamic Partial Order Reduction for Model Checking Event-Drive ... 10:50 - 11:20						VMCAIInPerson Scaling Up Livelock Verification for Network-on-Chip Routing Algorithms 11:20 - 11:50																										VMCAIRemote Fanoos: Multi-Resolution, Multi-Strength, Interactive Explanations for ... 13:30 - 14:00						VMCAIInPerson Bisimulations for Neural Network Reduction 14:00 - 14:30													VMCAIRemote High Assurance Software for Financial Regulation and Business Platforms 15:05 - 15:35						VMCAIRemote Loop Verification with Invariants and Contracts 15:35 - 16:05						VMCAIRemote 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	VMCAIInPerson Gradient-Descent for Randomized Controllers under Partial Observability 09:00 - 09:30						VMCAIRemote Satisfiability and Synthesis Modulo Oracles 09:30 - 10:00										VMCAIInPerson Out of Control: Reducing Probabilistic Models by Control-State Elimination 10:20 - 10:50						VMCAIRemote STAMINA 2.0: Improving Scalability of Infinite-StateStochastic Model Ch ... 10:50 - 11:20						VMCAIRemote EPMC Gets Knowledge in Multi-Agent Systems 11:20 - 11:50																										VMCAIRemote Simplifying Concurrent Programming via Synchronization Synthesis 13:30 - 14:30																			VMCAIInPerson Fast Three-Valued Abstract Bit-Vector Arithmetic 15:05 - 15:35						VMCAIRemote 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 RemoteInvited 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 TalkInPerson 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 RemoteInvited Talk Coalgebra for the working programming languages researcher 09:00 - 10:00																POPL Distinguished PaperInPerson 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 InclusionRemote 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 PaperRemote 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	CoqPLRemote Coq meets literate programming: tools for documenting, preserving, and ... 09:00 - 10:00																CoqPLRemote A Visual Ltac Debugger in CoqIDE 10:20 - 10:40				CoqPLInPerson Scrap your boilerplate definitions in 10 lines of Ltac! 10:40 - 11:00				CoqPLInPerson Tealeaves: Categorical structures for syntax 11:00 - 11:20				CoqPLRemote Towards a Formalization of Nominal Sets in Coq 11:20 - 11:40				CoqPLInPerson A Case for Lightweight Interfaces in Coq 11:40 - 12:00																						CoqPLRemote Verifying Concurrent, Crash-Safe Systems with Perennial 13:30 - 14:30												CoqPLRemote A Verified Pipeline from a Specification Language to Optimized, Safe Rust 14:30 - 14:50							CoqPLRemote Session with the Coq Development Team 15:05 - 15:50

Room information: Salon I

Program Display Configuration

Sun 16 JanDisplayed time zone: Eastern Time (US & Canada) change

Mon 17 JanDisplayed time zone: Eastern Time (US & Canada) change

Tue 18 JanDisplayed time zone: Eastern Time (US & Canada) change

Wed 19 JanDisplayed time zone: Eastern Time (US & Canada) change

Thu 20 JanDisplayed time zone: Eastern Time (US & Canada) change

Fri 21 JanDisplayed time zone: Eastern Time (US & Canada) change

Sat 22 JanDisplayed time zone: Eastern Time (US & Canada) change

Sun 16 JanDisplayed time zone: Eastern Time (US & Canada) change

VMCAI

VMCAI

VMCAI

VMCAI

Mon 17 JanDisplayed time zone: Eastern Time (US & Canada) change

VMCAI

VMCAI

VMCAI

VMCAI

Tue 18 JanDisplayed time zone: Eastern Time (US & Canada) change

VMCAI

VMCAI

VMCAI

VMCAI

Wed 19 JanDisplayed time zone: Eastern Time (US & Canada) change

POPL

POPL

POPL

POPL

POPL

POPL

Thu 20 JanDisplayed time zone: Eastern Time (US & Canada) change

POPL

POPL

POPL

POPL

POPL

Fri 21 JanDisplayed time zone: Eastern Time (US & Canada) change

POPL

POPL

Diversity, Equity and Inclusion

POPL

POPL

POPL

Sat 22 JanDisplayed time zone: Eastern Time (US & Canada) change

CoqPL

CoqPL

CoqPL

CoqPL

CoqPL

Sun 16 JanDisplayed time zone: Eastern Time (US & Canada) change

Mon 17 JanDisplayed time zone: Eastern Time (US & Canada) change

Tue 18 JanDisplayed time zone: Eastern Time (US & Canada) change

Wed 19 JanDisplayed time zone: Eastern Time (US & Canada) change

Thu 20 JanDisplayed time zone: Eastern Time (US & Canada) change

Fri 21 JanDisplayed time zone: Eastern Time (US & Canada) change

Sat 22 JanDisplayed time zone: Eastern Time (US & Canada) change

Sun 16 Jan
Displayed time zone: Eastern Time (US & Canada) change

Mon 17 Jan
Displayed time zone: Eastern Time (US & Canada) change

Tue 18 Jan
Displayed time zone: Eastern Time (US & Canada) change

Wed 19 Jan
Displayed time zone: Eastern Time (US & Canada) change

Thu 20 Jan
Displayed time zone: Eastern Time (US & Canada) change

Fri 21 Jan
Displayed time zone: Eastern Time (US & Canada) change

Sat 22 Jan
Displayed time zone: Eastern Time (US & Canada) change

Sun 16 Jan
Displayed time zone: Eastern Time (US & Canada) change

Mon 17 Jan
Displayed time zone: Eastern Time (US & Canada) change

Tue 18 Jan
Displayed time zone: Eastern Time (US & Canada) change

Wed 19 Jan
Displayed time zone: Eastern Time (US & Canada) change

Thu 20 Jan
Displayed time zone: Eastern Time (US & Canada) change

Fri 21 Jan
Displayed time zone: Eastern Time (US & Canada) change

Sat 22 Jan
Displayed time zone: Eastern Time (US & Canada) change

Sun 16 Jan
Displayed time zone: Eastern Time (US & Canada) change

Mon 17 Jan
Displayed time zone: Eastern Time (US & Canada) change

Tue 18 Jan
Displayed time zone: Eastern Time (US & Canada) change

Wed 19 Jan
Displayed time zone: Eastern Time (US & Canada) change

Thu 20 Jan
Displayed time zone: Eastern Time (US & Canada) change

Fri 21 Jan
Displayed time zone: Eastern Time (US & Canada) change

Sat 22 Jan
Displayed time zone: Eastern Time (US & Canada) change