LAFI 2025
Sun 19 Jan 2025
Denver, Colorado, United States
co-located with
POPL 2025
Toggle navigation
Attending
Venue: Curtis Hotel Denver
Program
LAFI Program
Your Program
Sun 19 Jan
Track/Call
Organization
LAFI 2025 Committees
Track Committees
Program Committee
Steering Committee
Contributors
People Index
Search
Series
Series
LAFI 2025
LAFI 2024
LAFI 2023
LAFI 2022
LAFI 2021
LAFI 2020
LAFI 2019
PPS 2018
PPS 2017
PPS 2016
Sign in
Sign up
POPL 2025
(
series
) /
LAFI 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
09:00
10m
Day opening
Day opening
Dafny
Stefan Zetzsche
Amazon Web Services
09:10
60m
Keynote
Keynote
Dafny
Nada Amin
Harvard University
11:00 - 12:30
Proof Stability and Applications
Dafny
at
Hopscotch
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
11:54
18m
Talk
Shipwright: A Modular Framework for Verifying Liveness of Byzantine Fault Tolerant Systems
Dafny
Derek Leung
MIT
,
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
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
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
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
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
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
VMCAI
VMCAI
VMCAI
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
VMCAI
VMCAI
VMCAI
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
x
Sun 22 Dec 02:31