POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States
POPL 2025 (series) / Curtis Hotel Denver /

Room information: Hopscotch

VenueCurtis Hotel Denver
Room nameHopscotch
Floor3
Capacity110
Room InformationNo extra information available
Program

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

Sun 19 Jan

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

09:00 - 10:30
KeynoteDafny at Hopscotch
Chair(s): Stefan Zetzsche Amazon Web Services
09:00
10m
Day opening
Day opening
Dafny
Stefan Zetzsche Amazon Web Services
09:10
60m
Keynote
Keynote
Dafny
K. Rustan M. Leino Amazon
11:00 - 12:30
Proof Stability and ApplicationsDafny at Hopscotch
Chair(s): Stefan Zetzsche Amazon Web Services
11:00
18m
Talk
Helping users to reduce Brittleness in their Dafny programs - a success story
Dafny
Remy Willems Amazon, Matthias Schlaipfer Amazon, Olivier Bouissou Amazon
11:18
18m
Talk
Towards Proof Stability in SMT-based Program Verification
Dafny
Yi Zhou Carnegie Mellon University, Bryan Parno Carnegie Mellon University
11:36
18m
Talk
Verifying the Fisher-Yates Shuffle Algorithm in Dafny
Dafny
Stefan Zetzsche Amazon Web Services, Tancrède Lepoint Amazon Web Services, Jean-Baptiste Tristan Amazon Web Services, Mikael Mayer Automated Reasoning Group, Amazon Web Services
Pre-print
11:54
18m
Talk
Shipwright: A Modular Framework for Verifying Liveness of Byzantine Fault Tolerant Systems
Dafny
Derek Leung Massachusetts Institute of Technology, USA, Nickolai Zeldovich Massachusetts Institute of Technology, USA, M. Frans Kaashoek Massachusetts Institute of Technology, USA
12:12
18m
Talk
Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny
Dafny
Stefan Zetzsche Amazon Web Services, Wojciech Różowski University College London
14:00 - 15:30
Backends and TeachingDafny at Hopscotch
Chair(s): Stefan Zetzsche Amazon Web Services
14:00
18m
Talk
Baking for Dafny: A CakeML Backend for Dafny
Dafny
Daniel Nezamabadi Chalmers University of Technology and University of Gothenburg, Magnus O. Myreen Chalmers University of Technology
Pre-print
14:18
18m
Talk
Lean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean
Dafny
Wojciech Różowski University College London, Georges-Axel Jaloyan Amazon Web Services, Sean McLaughlin Amazon Web Services
14:36
18m
Talk
Performant, Readable and Interoperable Rust from Dafny
Dafny
Mikael Mayer Automated Reasoning Group, Amazon Web Services, Shadaj Laddad University of California at Berkeley, Fabio Madge Automated Reasoning Group, Amazon Web Services, Siva Somayyajula Amazon Web Services, Jean-Baptiste Tristan Amazon Web Services
14:54
18m
Talk
Randomised Testing of the Dafny Compiler: Into the CI
Dafny
Karnbongkot Boonriong Imperial College London, Alastair F. Donaldson Imperial College London, Stefan Zetzsche Amazon Web Services
15:12
18m
Talk
Teaching Types and Non-Interference in Dafny
Dafny
Bryan Parno Carnegie Mellon University
16:00 - 18:00
Verified Code SynthesisDafny at Hopscotch
Chair(s): Stefan Zetzsche Amazon Web Services
16:00
18m
Talk
Laurel: Unblocking Automated Verification with Large Language Models
Dafny
Eric Mugnier University of California San Diego, Emmanuel Anaya Gonzalez UCSD, Nadia Polikarpova University of California at San Diego, Ranjit Jhala University of California at San Diego, Zhou Yuanyuan UCSD
16:18
18m
Talk
VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search
Dafny
David Brandfonbrener Harvard, Simon Henniger Technical University of Munich, Sibi Raja Harvard, Tarun Prasad Harvard, Chloe Loughridge Harvard University, Federico Cassano Northeastern University, Sabrina Ruixin Hu Harvard, Jianang Yang Million.js, William E. Byrd University of Alabama at Birmingham, USA, Robert Zinkov University of Oxford, Nada Amin Harvard University
16:36
18m
Talk
dafny-annotator: AI-Assisted Verification of Dafny Programs
Dafny
Gabriel Poesia Stanford University, Chloe Loughridge Harvard University, Nada Amin Harvard University
16:54
18m
Talk
Dafny as Verification-Aware Intermediate Language for Code Generation
Dafny
Yue Chen Li Massachusetts Institute of Technology, Stefan Zetzsche Amazon Web Services, Siva Somayyajula Amazon Web Services
Pre-print
17:12
18m
Talk
DafnyBench: A Benchmark for Formal Software Verification
Dafny
Chloe Loughridge Harvard University, Qinyi Sun Massachusetts Institute of Technology, Seth Ahrenbach Beneficial AI Foundation, Federico Cassano Northeastern University, Chuyue Sun Stanford University, Ying Sheng Stanford University, Anish Mudide Massachusetts Institute of Technology, Md Rakib Hossain Misu University of California Irvine, Nada Amin Harvard University, Max Tegmark Massachusetts Institute of Technology
17:30
18m
Talk
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
Dafny
Saikat Chakraborty Microsoft Research, Gabriel Ebner Microsoft Research, Siddharth Bhat University of Cambridge, Sarah Fakhoury Microsoft Research, Sakina Fatima University of Ottawa, Shuvendu K. Lahiri Microsoft Research, Nikhil Swamy Microsoft Research
17:48
12m
Day closing
Day closing
Dafny
Stefan Zetzsche Amazon Web Services

Mon 20 Jan

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

09:00 - 10:30
Keynote Talk and Cyber-Physical SystemsVMCAI at Hopscotch
Chair(s): Sriram Sankaranarayanan University of Colorado, Boulder
09:00
60m
Talk
Keynote Talk: Formal methods in a model-free, data-driven world
VMCAI
Jyotirmoy Deshmukh University of Southern California
10:00
30m
Talk
Synthesis of Controllers for Continuous Blackbox Systems
VMCAI
Benedikt Maderbacher Graz University of Technology, Felix Windisch Graz University of Technology, Alberto Larrauri University of Oxford, Roderick Bloem Institute of Software Technology, Graz University of Technology
11:00 - 12:30
Abstract Interpretation # 1VMCAI at Hopscotch
Chair(s): Kedar Namjoshi Nokia Bell Labs
11:00
30m
Talk
Affine Disjunctive Invariant Generation with Farkas’ Lemma
VMCAI
Jingyu Ke Shanghai Jiao Tong University, Hongfei Fu Shanghai Jiao Tong University, Hongming Liu Shanghai Jiao Tong University, Zhouyue Sun Shanghai Jiao Tong University, Liqian Chen National University of Defense Technology, Guoqiang Li Shanghai Jiao Tong University
11:30
30m
Talk
Automatic Inference of Relational Object Invariants
VMCAI
Yusen Su University of Waterloo, Jorge A. Navas Certora, Arie Gurfinkel University of Waterloo, Isabel Garcia-Contreras University of Waterloo
12:00
30m
Talk
A Static Analysis of Entanglement
VMCAI
Nicola Assolini University of Verona, Alessandra Di Pierro University of Verona, Isabella Mastroeni University of Verona
14:00 - 15:30
Model CheckingVMCAI at Hopscotch
Chair(s): Arie Gurfinkel University of Waterloo
14:00
30m
Talk
Space-Efficient Model-Checking of Higher-Order Recursion Schemes
VMCAI
Florian Bruse University of Kassel
14:30
30m
Talk
Parameterized Verification of Systems with Precise (0,1)-Counter AbstractionRemote
VMCAI
Paul Eichler CISPA - Helmholtz Center for Information Security, Swen Jacobs CISPA, Chana Weil-Kennedy IMDEA Software Institute
15:00
30m
Talk
Property-agnostic base case extension for scalable verification of distributed systems
VMCAI
Kyle Storey Brigham Young University, Eric Mercer Brigham Young University
16:00 - 17:30
ApplicationsVMCAI at Hopscotch
Chair(s): Jyotirmoy Deshmukh University of Southern California
16:00
30m
Talk
ExpectAll: A BDD Based Approach for Link Failure Resilience in Elastic Optical Networks
VMCAI
Gustav S. Bruhns Aalborg University, Martin P. Hansen Aalborg University, Rasmus Hebsgaard Aalborg University, Frederik M. W. Hyldgaard Aalborg University, Jiri Srba Aalborg University
16:30
30m
Talk
Constructing Trustworthy Smart Contracts
VMCAI
Devora Chait-Roth New York University, Kedar Namjoshi Nokia Bell Labs
17:00
30m
Talk
Automated Flaw Detection for Industrial Robot RESTful ServiceRecorded
VMCAI
Yuncheng Wang Institute of Information Engineering, Chinese Academy of Sciences; School of Cyber Security, UCAS Beijing, China, Puzhuo Liu Tsinghua University, Yaowen Zheng Institute of Information Engineering at Chinese Academy of Sciences, Dongliang Fang Beijing Key Laboratory of IOT Information Security Technology, Institute of Information Engineering, CAS, China; School of Cyber Security, University of Chinese Academy of Sciences, China, Zhiwen Pan Institute of Information Engineering, Chinese Academy of Sciences; School of Cyber Security, UCAS Beijing, China, Shuaizong Si Institute of Information Engineering, Chinese Academy of Sciences; School of Cyber Security, UCAS Beijing, China, Weidong Zhang Institute of Information Engineering, Chinese Academy of Sciences; School of Cyber Security, UCAS Beijing, China, Limin Sun Institute of Information Engineering at Chinese Academy of Sciences; University of Chinese Academy of Sciences
Media Attached

Tue 21 Jan

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

09:00 - 10:30
Keynote Talk (Tuesday) and LearningVMCAI at Hopscotch
Chair(s): Ashutosh Trivedi University of Colorado Boulder
09:00
60m
Talk
Keynote Talk: Outcome Logic: a foundational framework for concurrent and probabilistic program analysis
VMCAI
Alexandra Silva Cornell University
10:00
30m
Talk
1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization
VMCAI
Muqsit Azeem Technical University of Munich, Debraj Chakraborty Masaryk University, Sudeep Kanav LMU Munich, Jan Kretinsky Masaryk University, Czech Republic, Mohammadsadegh Mohagheghi Masaryk University, Stefanie Mohr Technical University of Munich, Maximilian Weininger Institute of Science and Technology Austria
11:00 - 12:30
VerificationVMCAI at Hopscotch
Chair(s): Isabella Mastroeni University of Verona
11:00
30m
Talk
A Real-Blasting Extension of Cvc5 for Reasoning about Floating-Point Arithmetic
VMCAI
Daisuke Ishii JAIST
11:30
30m
Talk
Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study
VMCAI
Mario Bucev EPFL, Samuel Chassot EPFL, LARA, Simon Felix Ateleris GmbH, Filip Schramka Ateleris GmbH, Viktor Kunčak EPFL, Switzerland
Pre-print
12:00
30m
Talk
Formal Verification of Probabilistic Deep Reinforcement Learning Policies with Abstract Training
VMCAI
Junfeng Yang Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Junfeng Yang Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Xin Chen University of New Mexico, USA, Qin Li Shanghai Key Laboratory of Trustworthy Computing, East China Normal University
14:00 - 15:30
Abstract Interpretation # 2VMCAI at Hopscotch
Chair(s): Alexandra Silva Cornell University
14:00
30m
Talk
Abstract Local Completeness: A Local form of Abstract Non-Interference
VMCAI
Isabella Mastroeni University of Verona
14:30
30m
Talk
An Abstract Domain for Heap Commutativity
VMCAI
Jared Pincus Boston University, Eric Koskinen Stevens Institute of Technology
15:00
30m
Talk
Two-way collaboration between flow and proof in SPARK
VMCAI
Claire Dross AdaCore, Joffrey Huguet AdaCore, Johannes Kanig AdaCore
16:00 - 17:30
ConcurrencyVMCAI at Hopscotch
Chair(s): Sriram Sankaranarayanan University of Colorado, Boulder
16:00
30m
Talk
LLOR: Automated Repair of OpenMP Programs
VMCAI
Gautam Muduganti Indian Institute of Technology Hyderabad, India, Utpal Bora University of Cambridge, Saurabh Joshi Supra Research, Ramakrishna Upadrasta
16:30
30m
Talk
Synthesis of Parametric Locally Symmetric Protocols from Abstract Temporal Specifications
VMCAI
Ruoxi Zhang University of Waterloo, Richard Trefler University of Waterloo, Canada, Kedar Namjoshi Nokia Bell Labs
17:00
30m
Talk
Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts
VMCAI
Julian Erhard LMU Munich; TU Munich, Manuel Bentele University of Freiburg, Matthias Heizmann University of Freiburg, Germany, Dominik Klumpp University of Freiburg, Simmo Saan University of Tartu, Estonia, Frank Schüssele University of Freiburg, Michael Schwarz TU Munich, Helmut Seidl TU Munich, Sarah Tilscher Technical University of Munich, Garching, Germany, Vesal Vojdani University of Tartu
Pre-print

Wed 22 Jan

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

12:00 - 13:20
Mentoring LunchCatering at Hopscotch
12:00
80m
Lunch
Mentoring Lunch
Catering

Thu 23 Jan

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

12:00 - 13:20
LunchCatering at Hopscotch
12:00
80m
Lunch
Lunch
Catering

Fri 24 Jan

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

12:00 - 13:20
LunchCatering at Hopscotch

Sun 19 Jan

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Hopscotch

Dafny

Keynote

Dafny

Proof Stability and Applications

Dafny

Backends and Teaching

Dafny

Verified Code Synthesis

Mon 20 Jan

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Hopscotch

VMCAI

Keynote Talk and Cyber-Physical Systems

VMCAI

Abstract Interpretation # 1

VMCAI

Model Checking

VMCAI

Applications

Tue 21 Jan

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Hopscotch

VMCAI

Keynote Talk (Tuesday) and Learning

VMCAI

Verification

VMCAI

Abstract Interpretation # 2

VMCAI

Concurrency

Wed 22 Jan

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

Room12:003013:0030
Hopscotch

Catering

Mentoring Lunch

Thu 23 Jan

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

Room12:003013:0030
Hopscotch

Catering

Lunch

Fri 24 Jan

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

Room12:003013:0030
Hopscotch

Catering

Lunch

Sun 19 Jan

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Hopscotch
Dafny
Day opening
09:00 - 09:10
Dafny
Keynote
09:10 - 10:10
Dafny
Helping users to reduce Brittleness in their Dafny programs - a success ...
11:00 - 11:18
Dafny
Towards Proof Stability in SMT-based Program Verification
11:18 - 11:36
Dafny
Verifying the Fisher-Yates Shuffle Algorithm in Dafny
11:36 - 11:54
Dafny
Shipwright: A Modular Framework for Verifying Liveness of Byzantine Fau ...
11:54 - 12:12
Dafny
Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny
12:12 - 12:30
Dafny
Baking for Dafny: A CakeML Backend for Dafny
14:00 - 14:18
Dafny
Lean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean
14:18 - 14:36
Dafny
Performant, Readable and Interoperable Rust from Dafny
14:36 - 14:54
Dafny
Randomised Testing of the Dafny Compiler: Into the CI
14:54 - 15:12
Dafny
Teaching Types and Non-Interference in Dafny
15:12 - 15:30
Dafny
Laurel: Unblocking Automated Verification with Large Language Models
16:00 - 16:18
Dafny
VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Lan ...
16:18 - 16:36
Dafny
dafny-annotator: AI-Assisted Verification of Dafny Programs
16:36 - 16:54
Dafny
Dafny as Verification-Aware Intermediate Language for Code Generation
16:54 - 17:12
Dafny
DafnyBench: A Benchmark for Formal Software Verification
17:12 - 17:30
Dafny
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
17:30 - 17:48
Dafny
Day closing
17:48 - 18:00

Mon 20 Jan

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Hopscotch
VMCAI
Keynote Talk: Formal methods in a model-free, data-driven world
09:00 - 10:00
VMCAI
Synthesis of Controllers for Continuous Blackbox Systems
10:00 - 10:30
VMCAI
Affine Disjunctive Invariant Generation with Farkas’ Lemma
11:00 - 11:30
VMCAI
Automatic Inference of Relational Object Invariants
11:30 - 12:00
VMCAI
A Static Analysis of Entanglement
12:00 - 12:30
VMCAI
Space-Efficient Model-Checking of Higher-Order Recursion Schemes
14:00 - 14:30
VMCAIRemote
Parameterized Verification of Systems with Precise (0,1)-Counter Abstra ...
14:30 - 15:00
VMCAI
Property-agnostic base case extension for scalable verification of dist ...
15:00 - 15:30
VMCAI
ExpectAll: A BDD Based Approach for Link Failure Resilience in Elastic ...
16:00 - 16:30
VMCAI
Constructing Trustworthy Smart Contracts
16:30 - 17:00
VMCAIRecorded
Automated Flaw Detection for Industrial Robot RESTful Service
17:00 - 17:30

Tue 21 Jan

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Hopscotch
VMCAI
Keynote Talk: Outcome Logic: a foundational framework for concurrent an ...
09:00 - 10:00
VMCAI
1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes ...
10:00 - 10:30
VMCAI
A Real-Blasting Extension of Cvc5 for Reasoning about Floating-Point Ar ...
11:00 - 11:30
VMCAI
Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study
11:30 - 12:00
VMCAI
Formal Verification of Probabilistic Deep Reinforcement Learning Polici ...
12:00 - 12:30
VMCAI
Abstract Local Completeness: A Local form of Abstract Non-Interference
14:00 - 14:30
VMCAI
An Abstract Domain for Heap Commutativity
14:30 - 15:00
VMCAI
Two-way collaboration between flow and proof in SPARK
15:00 - 15:30
VMCAI
LLOR: Automated Repair of OpenMP Programs
16:00 - 16:30
VMCAI
Synthesis of Parametric Locally Symmetric Protocols from Abstract Tempo ...
16:30 - 17:00
VMCAI
Correctness Witnesses for Concurrent Programs: Bridging the Semantic Di ...
17:00 - 17:30

Wed 22 Jan

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

Room12:0015304513:00153045
Hopscotch
POPL Catering
Mentoring Lunch
12:00 - 13:20

Thu 23 Jan

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

Room12:0015304513:00153045
Hopscotch
POPL Catering
Lunch
12:00 - 13:20