POPL 2025
Sun 19 - Sat 25 January 2025
Denver, Colorado, United States
Toggle navigation
Attending
Venue: Curtis Hotel Denver
Supporting POPL
Registration
Information for Virtual Attendees
Information for Presenters
Requesting a Visa
POPL Live Streams
Code of Conduct
Program
POPL Program
Your Program
Filter by Day
Sun 19 Jan
Mon 20 Jan
Tue 21 Jan
Wed 22 Jan
Thu 23 Jan
Fri 24 Jan
Sat 25 Jan
Tracks
POPL 2025
Artifact Evaluation
POPL
Student Research Competition
Student Volunteers
Tutorials
Workshops and Co-located Events
Co-hosted Conferences
CPP
VMCAI
Workshops
CoqPL
Dafny
LAFI
PEPM
PLMW @ POPL
PLanQC
PriSC
TPSA
WAW
WITS
Co-hosted Symposia
PADL
Organization
POPL 2025 Committees
Organizing Committee
AV Committee
Student Volunteers
Track Committees
Artifact Evaluation
POPL
Student Research Competition
Contributors
People Index
Co-hosted Conferences
CPP
Organizing Committee
Program Committee
Steering Committee
VMCAI
Organizing Committee
Program Committee
Artifact Evaluation Committee
Workshops
CoqPL
Program Committee
Dafny
Program Committee Chairs
Program Committee
Steering Committee Chairs
LAFI
Program Committee
Steering Committee
PEPM
Chairs
Program Committee Members
PLMW @ POPL
Organizing Committee
Speakers
Panelists
PLanQC
Organizing Committee
Program Committee
PriSC
Program Committee
Steering Committee
TPSA
Organizing Committee
Program Committee
WAW
Organizers
Program Committee
WITS
Program Committee
Co-hosted Symposia
PADL
Programme Chairs
Program Committee
Search
Series
Series
POPL 2025
POPL 2024
POPL 2023
POPL 2022
POPL 2021
POPL 2020
POPL 2019
POPL 2018
POPL 2017
POPL 2016
Sign in
Sign up
POPL 2025
(
series
) /
Curtis Hotel Denver
/
Room information: Hopscotch
Venue
Curtis Hotel Denver
Room name
Hopscotch
Floor
3
Capacity
110
Room Information
No extra information available
Program
Detailed Table
Session Timeline
Detailed Timeline
This program is tentative and subject to change.
Program Display Configuration
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
(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-06: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+03: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 19 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
09:00 - 10:30
Keynote
Dafny
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 Applications
Dafny
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 Teaching
Dafny
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 Synthesis
Dafny
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 Systems
VMCAI
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 # 1
VMCAI
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 Checking
VMCAI
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 Abstraction
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
Applications
VMCAI
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 Service
Recorded
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 Learning
VMCAI
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
Verification
VMCAI
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 # 2
VMCAI
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
Concurrency
VMCAI
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
Lunch
Catering
at
Hopscotch
12:00
80m
Lunch
Lunch
Catering
Thu 23 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
12:00 - 13:20
Lunch
Catering
at
Hopscotch
12:00
80m
Lunch
Lunch
Catering
Fri 24 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
12:00 - 13:20
Lunch
Catering
at
Hopscotch
Hide past events
Sun 19 Jan
Displayed time zone:
Mountain 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
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
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
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
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
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
Room
12:00
30
13:00
30
Hopscotch
Catering
Lunch
Thu 23 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
Room
12:00
30
13:00
30
Hopscotch
Catering
Lunch
Fri 24 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
Room
12:00
30
13:00
30
Hopscotch
Catering
Lunch
Hide past events
Sun 19 Jan
Displayed time zone:
Mountain 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
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
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
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
VMCAI
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
VMCAI
Recorded
Automated Flaw Detection for Industrial Robot RESTful Service
17:00 - 17:30
Tue 21 Jan
Displayed time zone:
Mountain 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
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
Room
12:00
15
30
45
13:00
15
30
45
Hopscotch
POPL Catering
Lunch
12:00 - 13:20
Thu 23 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
Room
12:00
15
30
45
13:00
15
30
45
Hopscotch
POPL Catering
Lunch
12:00 - 13:20
Hide past events
x
Wed 22 Jan 09:28