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

Room information: Room 5

VenueCurtis Hotel Denver
Room nameRoom 5
Floor0
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

Mon 20 Jan

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

09:00 - 10:30
Session 1PriSC at Room 5
09:00
4m
Day opening
Opening Remarks
PriSC
Marco Patrignani University of Trento, Marco Vassena Utrecht University
09:05
59m
Keynote
Keynote: Bringing Verified Cryptographic Protocols to Practice
PriSC
Bryan Parno Carnegie Mellon University
10:05
25m
Talk
A Semantic Approach to Robust Property Preservation
PriSC
Niklas Mück MPI-SWS, Michael Sammler Institute of Science and Technology Austria, Aina Linn Georges Max Planck Institute for Software Systems (MPI-SWS), Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS
11:00 - 12:30
Session 2PriSC at Room 5
11:00
25m
Talk
ILA: Correctness via Type Checking for Fully Homomorphic Encryption
PriSC
Tarakaram Gollamudi None, Anitha Gollamudi University of Massachusetts Lowell, Joshua Gancher Northeastern University
11:25
24m
Talk
Leveraging Duality for Programming with zkSNARKs
PriSC
Rahul Krishnan University of Wisconsin-Madison, Ethan Cecchetti University of Wisconsin-Madison
11:50
24m
Talk
Preservation of Speculative Constant-time by Compilation
PriSC
Santiago Arranz Olmos Max Planck Institute for Security and Privacy, Gilles Barthe MPI-SP; IMDEA Software Institute, Lionel Blatter Max Planck Institute for Security and Privacy, Benjamin Gregoire INRIA, Vincent Laporte Inria
12:15
15m
Talk
Lightning talks
PriSC

14:00 - 15:30
Session 3PriSC at Room 5
14:00
24m
Talk
Auditing Rust Crates Effectively
PriSC
Lydia Zoghbi University of California, San Diego, David Thien University of California, San Diego, Ranjit Jhala UCSD, Deian Stefan University of California at San Diego, Caleb Stanford University of California, Davis
14:25
24m
Talk
Automatic Inference of Enclave Placement in LLVM Compiler
PriSC
Wesley B Nuzzo University of Massachusetts, Lowell (UML), Mohamed Elwakil U.S. Coast Guard Academy, Anitha Gollamudi University of Massachusetts Lowell
14:50
24m
Talk
Counterexamples in Safe Rust
PriSC
Muhammad Hassnain University of California, Davis, Caleb Stanford University of California, Davis
15:15
15m
Talk
Lightning talks
PriSC

16:00 - 17:30
Session 4PriSC at Room 5
16:00
24m
Talk
BeePL: Correct-by-compilation kernel extensions
PriSC
Swarn Priya Virginia Tech, Tim Steenvoorden Open Universiteit, Connor Sughrue Virginia Tech, Frédéric Besson Inria, Rennes, Freek Verbeek Open Universiteit & Virginia Tech
16:25
24m
Talk
Non-Interference Preserving and Optimising Compilation with Hyperproperty Simulations
PriSC
Julian Rosemann Saarland University, Saarland Informatics Campus, Sebastian Hack Saarland University, Saarland Informatics Campus, Deepak Garg MPI-SWS
16:50
24m
Talk
SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
PriSC
Sören van der Wall PhD Student, Roland Meyer TU Braunschweig
17:15
15m
Day closing
Closing Remarks
PriSC
Marco Patrignani University of Trento, Marco Vassena Utrecht University

Mon 20 Jan

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Room 5

PriSC

Session 1

PriSC

Session 2

PriSC

Session 3

PriSC

Session 4

Tue 21 Jan

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Room 5

PLMW @ POPL

PLMW @ POPL

PLMW @ POPL

PLMW @ POPL

Mon 20 Jan

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Room 5
PriSC
Opening Remarks
09:00 - 09:04
PriSC
Keynote: Bringing Verified Cryptographic Protocols to Practice
09:05 - 10:04
PriSC
A Semantic Approach to Robust Property Preservation
10:05 - 10:30
PriSC
ILA: Correctness via Type Checking for Fully Homomorphic Encryption
11:00 - 11:25
PriSC
Leveraging Duality for Programming with zkSNARKs
11:25 - 11:49
PriSC
Preservation of Speculative Constant-time by Compilation
11:50 - 12:14
PriSC
Lightning talks
12:15 - 12:30
PriSC
Auditing Rust Crates Effectively
14:00 - 14:24
PriSC
Automatic Inference of Enclave Placement in LLVM Compiler
14:25 - 14:49
PriSC
Counterexamples in Safe Rust
14:50 - 15:14
PriSC
Lightning talks
15:15 - 15:30
PriSC
BeePL: Correct-by-compilation kernel extensions
16:00 - 16:24
PriSC
Non-Interference Preserving and Optimising Compilation with Hyperproper ...
16:25 - 16:49
PriSC
SNIP: Speculative Execution and Non-Interference Preservation for Compi ...
16:50 - 17:14
PriSC
Closing Remarks
17:15 - 17:30