PLMW @ POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States
co-located with POPL 2025
POPL 2025 (series) / PLMW @ POPL 2025 (series) / Curtis Hotel Denver /

Room information: Patty Cake

VenueCurtis Hotel Denver
Room namePatty Cake
Floor2
Capacity110
Room InformationNo extra information available
Program

This program is tentative and subject to change.

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

Tue 21 Jan

Displayed time zone: Mountain Time (US & Canada) change

09:00 - 10:30
Introduction and KeynoteTPSA at Patty Cake
09:00
10m
Day opening
Introduction
TPSA
Noam Zilberstein Cornell University, Azalea Raad Imperial College London, Jules Villard Meta
09:10
60m
Keynote
Improving Static Analysis using Information Collected at RuntimeKeynote
TPSA
Radu Grigore Meta
11:00 - 12:30
Program LogicsTPSA at Patty Cake
11:00
18m
Talk
Data Structure Abstraction and Incorrectness Separation Logic
TPSA
Andreas Lööw Imperial College London
11:18
18m
Talk
Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification
TPSA
Conrad Zimmerman Northeastern University, Jenna DiVincenzo (Wise) Purdue University
Pre-print
11:36
18m
Talk
Partial Incorrectness Logic
TPSA
Lena Verscht RWTH Aachen University; Saarland University, Ānrán Wáng Saarland University, Benjamin Lucien Kaminski Saarland University; University College London
11:54
18m
Talk
Concurrent Quantum Separation Logic for Fine-Grained Parallelism
TPSA
Yusuke Matsushita Kyoto University, Kengo Hirata University of Edinburgh, Ryo Wakizaka Kyoto University
12:12
18m
Talk
Total Outcome Logic: Termination and Nontermination Proving for Effectful Branching
TPSA
James Li Cornell University, Noam Zilberstein Cornell University, Alexandra Silva Cornell University
14:00 - 15:30
Static Analysis and Abstract InterpretationTPSA at Patty Cake
14:00
18m
Talk
Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Extended Abstract)
TPSA
Florian Sextl TU Wien, Austria, Adam Rogalewicz Brno University of Technology, Czechia, Tomáš Vojnar Brno University of Technology, Florian Zuleger TU Vienna
14:18
18m
Talk
Calculational design of Incorrectness Separation Logic
TPSA
Lorenzo Gazzella Università di Pisa
14:36
18m
Talk
Scalable Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Refutation
TPSA
Pedro Carrott Imperial College London, Sacha-Élie Ayoun Imperial College London, Azalea Raad Imperial College London
14:54
18m
Talk
Enhancing Infer Compositional Analysis with Summary Specialization
TPSA
David Pichardie Meta
15:12
18m
Talk
Cyclic Message Histories for Automated Safety Verification of Distributed Algorithms
TPSA
Christian Fontenot University of Colorado Boulder, Gowtham Kaki University of Colorado at Boulder, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon
16:00 - 17:30
Analysis TechniquesTPSA at Patty Cake
16:00
18m
Talk
Distributed transactions over mergeable types: A meta-theory for 5G control-plane protocol verification
TPSA
Prasanth Prahladan University of Colorado Boulder
16:18
18m
Talk
Domain Reasoning In TopKAT: Reduction and Completeness
TPSA
Cheng Zhang University College London (UCL), Arthur Azevedo de Amorim Rochester Institute of Technology, USA, Marco Gaboardi Boston University
16:36
18m
Talk
From Traces to Program Incorrectness: A Type-Theoretic Approach
TPSA
Yongwei Yuan Purdue University, Zhe Zhou Purdue University, Julia Belyakova Purdue University, Benjamin Delaware Purdue University, Suresh Jagannathan Purdue University
16:54
18m
Talk
Towards Semantics Lifting for Scientific Computing: A Case Study on FFT
TPSA
Naifeng Zhang Carnegie Mellon University, Sanil Rao Carnegie Mellon University, Mike Franusich SpiralGen, Inc., Franz Franchetti Carnegie Mellon University, USA
17:12
18m
Talk
U-turn: Forward-driven backward analysis for incorrectness
TPSA
Flavio Ascari University of Pisa, Roberto Bruni University of Pisa, Roberta Gori Diaprtimento di Informatica, Universita' di Pisa, Italy, Azalea Raad Imperial College London
18:00 - 22:00
Jane Street Social EventPOPL at Patty Cake
Chair(s): Chris Casinghino Jane Street, Richard A. Eisenberg Jane Street
18:00
4h
Social Event
Jane Street Game Night
POPL
Richard A. Eisenberg Jane Street, Chris Casinghino Jane Street

Tue 21 Jan

Displayed time zone: Mountain Time (US & Canada) change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:003018:003019:003020:003021:0030
Patty Cake

TPSA

Introduction and Keynote

TPSA

Program Logics

TPSA

Static Analysis and Abstract Interpretation

TPSA

Analysis Techniques

POPL

Jane Street Social Event

Tue 21 Jan

Displayed time zone: Mountain Time (US & Canada) change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:0015304519:0015304520:0015304521:00153045
Patty Cake
TPSA
Introduction
09:00 - 09:10
TPSAKeynote
Improving Static Analysis using Information Collected at Runtime
09:10 - 10:10
TPSA
Data Structure Abstraction and Incorrectness Separation Logic
11:00 - 11:18
TPSA
Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via G ...
11:18 - 11:36
TPSA
Partial Incorrectness Logic
11:36 - 11:54
TPSA
Concurrent Quantum Separation Logic for Fine-Grained Parallelism
11:54 - 12:12
TPSA
Total Outcome Logic: Termination and Nontermination Proving for Effectf ...
12:12 - 12:30
TPSA
Compositional Shape Analysis with Shared Abduction and Biabductive Loop ...
14:00 - 14:18
TPSA
Calculational design of Incorrectness Separation Logic
14:18 - 14:36
TPSA
Scalable Bug Detection for Internally Unsafe Libraries: A Logical Appro ...
14:36 - 14:54
TPSA
Enhancing Infer Compositional Analysis with Summary Specialization
14:54 - 15:12
TPSA
Cyclic Message Histories for Automated Safety Verification of Distribut ...
15:12 - 15:30
TPSA
Distributed transactions over mergeable types: A meta-theory for 5G con ...
16:00 - 16:18
TPSA
Domain Reasoning In TopKAT: Reduction and Completeness
16:18 - 16:36
TPSA
From Traces to Program Incorrectness: A Type-Theoretic Approach
16:36 - 16:54
TPSA
Towards Semantics Lifting for Scientific Computing: A Case Study on FFT
16:54 - 17:12
TPSA
U-turn: Forward-driven backward analysis for incorrectness
17:12 - 17:30
POPL
Jane Street Game Night
18:00 - 22:00