Program - POPL 2025

Detailed Table Session Timeline Detailed Timeline

Time Zone

The program is currently displayed in (GMT-07:00) Mountain Time (US & Canada).

Use conference time zone: (GMT-07:00) Mountain 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

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		Total Outcome Logic: Termination and Nontermination Proving for Effectful Branching TPSA James Li Cornell University, Noam Zilberstein Cornell University, Alexandra Silva Cornell University
12: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

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)Remote TPSA Florian Sextl TU Wien, Austria, Adam Rogalewicz Brno University of Technology, Czechia, Tomáš Vojnar Brno University of Technology, Florian Zuleger TU Vienna Pre-print
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		Concurrent Quantum Separation Logic for Fine-Grained Parallelism TPSA Yusuke Matsushita Kyoto University, Kengo Hirata University of Edinburgh, Ryo Wakizaka Kyoto University

TPSA 2025 Program

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

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia

TPSA 2025 Program

Switch Program View

Program Display Configuration

Tue 21 JanDisplayed time zone: Mountain Time (US & Canada) change

Get Calendar (iCal)

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