coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Dafny Workshop at POPL 2025 (deadline extension)

From: Stefan Zetzsche <stefanzetzsche AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Dafny Workshop at POPL 2025 (deadline extension)
Date: Tue, 8 Oct 2024 23:09:21 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=stefanzetzsche AT gmail.com; spf=Pass smtp.mailfrom=stefanzetzsche AT gmail.com; spf=None smtp.helo=postmaster AT mail-pf1-f175.google.com
Ironport-data: A9a23:gViuA69EqXFF7TDw4+F5DrUDLHqTJUtcMsCJ2f8bNWPcYEJGY0x3n WQZXGGDP6mKYWX8Ltkia4m/oEpXusCAmoRqTApv/i1EQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHPymYAL9EngZbRd+Tys8gg5Ulec8g4p56fC0GArlV ena+qUzA3f7nWctWo4ow/jb8k825Kyi4G9wUmEWPJingneOzxH5M7pEfcldH1OgKqFIE+izQ fr0zb3R1gs1KD9wYj8Nuu+TnnwiGtY+DyDW4pZlc/TKbix5m8AH+v1T2Mzwxqtgo27hc9hZk L2hvHErIOsjFvWkdO81C3G0H8ziVEHvFXCuzXWX6KSuI0P6n3TE3K9jB1saGLYj/clJEUIez 81fNh4ER0XW7w626OrTpuhEg80iKIzzMtpatCg/kHfWCvEpRZ2FSKLPjTNa9G1o14YeQLCEP pJfMGUyBPjDS0Un1lM/E44zku6ulHTjYSZTqF+9qq8+4myVxwt0uFToGIuFJ4PQFJsK9qqej kbNoXT7Ai0fCIHF6Ae8/2P9i/fwwzyuDer+E5Xjq6cy3wzNroAJMzUdUkL+qv2kgGalStdHI goV/DAvpO487iSWosLVWhS5pDucsEdZVYMPTqs17waCzqeS6AGcboQZctJfQMN8ucQsaRkR7 VimocPKVQZe96O7QFvIo994sgiOESQSKGYDYwoNQg0E/8TvrekPYvTnHocL/Emd3oydJN3g/ w1muhTSkFn6sCLm/6Cy/FSCmzz145aQEVNz6QLQUWaoqAh+YeZJhrBEC3CKtJ6sz67AETFtW UTofeDAtoji6rnTzUSwrB0lRu3B2hp8GGS0baRTN5cg7S+x3HWoYJpd5jpzTG8wbZxUImC2M RKI4VkIjHO2AJdMRf8mC25WI5R7pZUM6fy8B5g4k/IXPcghKlDdpEmCm2bLhDG9zxNEfV4D1 WezKpv1VSlLV8yLPRK5QOAS1bJjxyY1gwvuqWPTnnyaPU6lTCfNE98taQPQBshgtf/siFuPr 753aZDRoz0BC72WX8Ui2dRMRbz8BSNrW86eRg0+XrLrHzeK70l7UaWMmeNwINQ/90mX/8+Rl kyAtoZj4AKXrRX6xc+iMxiPsZu2Bc0n/0EodzchJ0ip0HUFaIOipvVXPZgucLVtsKQpwfdoR rNXM4+NE9ZeeAThoj49VJjaqJA9VRKJgQnVATGpTgJidLFdRivI2OTeQC3RyAc0ABGai+4Cs py79waCQZM8VwVoV8nXT/S0zmKOh3sWmcMsfk6RItBsZ1nn37l6DxPAntklHtw+c0Td9GGK0 yKTJwkSnsjWgooP6NKSr7u1n4SoNOpfH0RhAGjQ64itBxTa5maOxYxhUv6CWCL0DkfY2fyFS 71O7vfeNPYnog57g7BkGew28ZNktsrdmbBK6y9FQlPJVg2PIZF9KCCk2cJviPV89oVBs1HrZ nPVq8hoApTXCsbLC1VLGREEaN6E3vQqmjX/y/Q5DUH5xS1v9oq8TkRgEEiQuRNZMYdKHtsp8 cU5tO4Szj6PuB4gH9KFryJTrkCnDHgLVYc5vZA7Xq7vrCcWyW95XJ+NMR+uvamzaOhNPHI6f R6Spq7J3IpHymT4LnEcKHnq3Mhmv6oohixk9lE5Cm6yqoL3vcNvhBx12hYrfztR1SRCgr5SO HA0FkhbJpeu3jZPhepFVV+CAwtqWR+ToBTw73Arl2TpaVaieUKQDW86OMeLpFs49UAFdBdl3 bio8kTXehe0Q9PQhwwZRlxAh8H4a+BI5inuuZyCDtuUOZsXeh/nifKeXnUJoB7ZHs8Bvk3Li u109uJWa6egFyovj4AkKoudx5ICYQulITFcfPRf4685J2HQVzWs0zyoKUrqWMdsJeTPwHCoG f5VOcNDeBSv5hmg9glBK/Y3HIZ1u/o16P4pWLDhfzcGuoTCiAtZisvb8yymiVI7R9lrr90GF brQUDC/CU2Vu2pfnj7cjctDO1fgW+I+Wi/H4LmX/tkKRrU5i8M9VWEp07CxgWeZDxs/wTKQo zH4RvH3y85M9N1SurXCQ4t/Aze6E9fRbNiz0RuSto1OZOzfMM2VuAIyrELmDjtsPrAQeopWk LiRgeHzx2fAmqg8aEHCupy7D6ISz96DbOlWFcPWLXdhgiqJXvH30SYD42yVLZ9okstXw8uaG y+UTdSWTsFMfftw31hXZDp6PzdHLp/of4HyoS+ZhNadOCg3iADoAouuyi70UDt9aCQNBazbN ib1nPSLvfVzs4VGAU4/NcFMWpNXDgfqZvo7SofXqzKdM2iPh2GCsJvEkT4Ly2nCKluAIfbAz aP1fDrMXzXsh/iQ1/BciZJ4gTMPBnUkgeUQQFMUy+Qrtx+EVlw5PcYvGrRYLKpLkx7C9oDyP xDMS2oANR/Tfxp5dTfE3dCyeTvHW8IvPI71KAV8qgnQI22zCZibCbRsyjZ47j0kMnH/xeWgM pcF9me2IhG1xYpzSP0O4uCgx91q3e7e2mlC7HWVfxYe2PrCKe5iOL1d8AtxuejvFsjMkADTK zFwSzkbHQe0Tkn+FcsmcHlQcP3cUPUD0B1wBRpjAv6G02lY8AGE4PL6MuD3lLYEaazm4ZYQE GjvSTLlD3++gxQuVGhAhz7tqaBxAPOPWMO9KccPgOHUc76YsgwaAi/JocbDoAzONuKS/5MxW wRAO0QDOXk=
Ironport-hdrordr: A9a23:soLkUqh2dobny6vPHigj+KICL3BQXtcji2hC6mlwRA09TyX4rb HIoB1/73XJYVkqKRIdcLy7WJVoIkm8yXcW2/hyAV7KZmCP01dAR7sSiLcKrQeQfxEWNdQw6U 6jScVD4RHLYmSSRPyV3DWF
Ironport-phdr: A9a23:dKyDIhz+84weFyjXCzJQwFBlVkEcU1XcAAcZ59Idhq5Udez7ptK+Z xSZv643xweUFazgqNt6yMPu8JrcEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzH cBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/9pPPbwlSmjawb61+I BqqoQjRq8IbnZZsJqEtxxTGpXdFZ/5YyWR0K1yNgh3y/N2w/Jlt8yRRv/Iu6ctNWrjkcqo7U LJVEi0oP3g668P3uxbDSxCP5mYHXWUNjhVIGQnF4wrkUZr3ryD3q/By2CiePc3xULA0RTGv5 LplRRP0lCsKMSMy/WfKgcJyka1bugqsqBN/zYDaY4+bKeRwcb/GcNwAWWZMRNxcWzBdDo6+a YYEEuoPPfxfr4n4v1YAsAe+CheiBOz1zD9Dm3z50rMm0+UgCgHJwAwgEMwTu3nTt9X1KLkdU e6vw6nOzDTMce9W2Dbm6IfUchAuv+qBXb11ccXLyEkvExnJgUmXqYzgJj6Y0PkGvGeH4eR6T +2vl3InpB9rojip3sohhJTEi4YVx17E9Ch0w5o4KN23RUN1btOqEJ9dui+aOoZyQM4vQX1kt SI1xLAYp5K3YigExZc6yxDRd/CKc4eG7xT+X+ifJjd4gWhqeLO5hxuq6kigy+L8VtGw0FlQq CpJiN7MtmoC1xDL6siHTed98Vu72TaXzQzc9uZEIUUymKHGKJAh2qY9moQPvUnHBCP7m0X7g LWIekk55uSk8fnrb7fmq5KaKoR5lAX+Mrk1msyjH+s4KBUAX2ma+OuizLDv4Uv0S6hQgPIsi KnWqpXaKNwbpqGnBw9V1Z4u6xOlADen1NQUhGEHLFxYdB6egYjlJlPDLfDiAfewhFSslzhrx /TYMbH7HprNKX3DnK/gfbZ79UFc1BI+wc5D659QEL0MI/L+VlXvuNDFEhM1KRG4zuTnBdll0 4MRQ2OPAquXMKPItl+I4/oiI/KQZIALtjbyMf4l5v/wgn8lmF4dZrWm3ZsJZ32jEfRmJl+WY XvogtsbDWgKuQ8+QPTsiFKZSTFTfWq9X7og5jEnD4KrFZrPSpi3gLOdxCe7AoFWZmdeB1+QF nfobpyIVOsIaCKPOcBsiScEVLikS485zx6irg76y7x9LurV4CIUr5zj1MImr9HUwBo17Hl/C 9mX+2CLVWB92G0SFBEs26UqmlBwxF6FmZp1n+5DHtxer6dSTgo0PJjOwvBoENvyVyrOe96IT BCtRdDwUmJ5dc4439JbOxU1IN6llB2Wh0JCYpcQnr2PX9kv977EmmP2P4B7wmrH068oix8nR NFOPCuonP037BDdUqjOlUjRjKO2beIExieY73uOw2OIrkxEQhV7UajtUnUWZ0+QptP8tQvZV 7H7Mb08KUNazNKabK5Da9nnl1JDEez/NdrXZXC8h3WrDhaF7ryJZYvuPW4a2XaVE1AKxiYU+ 3vOLg0iHmGhrmbZWSRpDk7qaljw/PNWrXq6SgoswVjPYRQ+ivy6/RkagfHaQPQWtl4dkAEmr Tg8XFO03taNTsGFuxIkZ6JEJ9U0/FZA02vd8Q17JJ2paa541BYYdExsskXi2g8SaM0ImNU2r H4s0At5KL6JmFJHeTSC2JnsO7rRYmDs9RGrYqTS1xnQytGTsqsI7f05rR3ksmTLXgI573hp2 t9H3meO/Z7KASIdVJvwVgA88B0777DWby8h5p/FgGV2OPrR0HeK0NYoCe05jxe4Ko0HYeXUS UmoSpVcXpfze4lI0xCzYxkJPf5f7vsxNsKiLL6d3bKzef1nhHSghHhG54Z01gSN8TB9Q6jGx cVgobnQ0w2ZWjP7lFrkvNrwnNUOfi0fEGO52yX4FpVaZqBacoMCCGPoKMqyjIYb5dalSztD+ VivCklTktS1dBSbaU7wwR9L3kQaiXOikCq8iTdzlnt6y8jXlDyLyOPkeh0dP2dNT2Q3llbgL 7+/iNUCVVSpZQwk/Pe8zX7z3LMT5KF2Lm2IBFxNYzCzNGZ6FK25qruFZcdLrpIuqyReFuqmM xiWTbv0oh1S1C2GfSMW3yw2eTisqJjljQdxiG+1I3N6rX6fcsZ1jRvS/93TQ/dN0yFOHnEpz 2mKQALlZ5/woojcnoym0Kj2T2+7U5xPbSTnhZiNsie2/ywiABGymeyyhsyyFAE71SHh0Nw5M EeA5B34Y4Tty+G7Kbc9JhguVAK6sZMiXNghz9hV5tlYw3URi5SL8GBSlG7yNY4ewqfidD8WQ iZNxdfJ4Q/j0UklL3STxou/WG/Op6kpL9S8fG4S3Towqs5QD6LBpqdYkCV8pEi1sRDKavhwt jgYwPoqrnUdhqta3WhlhjXYGb0UEURCaGb3ixmG5tasoblFf22vfJC/0UN/mZaqC7TI8WQ+E D7pP5wlGyF39MB2NlnBhWby5o/Tc97VddsPtxeQnkSIn61PJZk2jPZPmTt/NDe3oyg+0+Bix 08Lv9nyrM2dJm5q5q78HhNIKmi/eZYI4j+0xadGwpTNgsb2T80nQGlUGsOvF67gESpO56q7c VzVS3tl9C/dQf2GTGr9oA9nty6dTc7tbinNYiFflZI4HFGcPBAN3l5SBmlr2M5hUFjtnpSpc V8ltG9LoAek7EIdkKQwcECvNwWX7AawNmVrFN7GdkcQtkcaoB6Lec2GsrAqR3Eep8L+6lzLc ivBPkxJFT1bAxPfQQmyYv/2o4GHqrb9ZKL2LuOSM+/W+KoOCrHRn8Lpisw/oH6NLpndZCA8S aBrnBMSBzYhXJ2I0zQXF35NznyLNZXK4kzmvHUw95HakryjTgvr4cHn56J6F9Jp9lj2hK6CM 7XVnyNlMXND0YtKw3bUyb8Z1VpUiid0djDrH65S/SjKBLndnKNaFXt5I2t6KddI4qQg3wJMJ d+Ti9X70aR9h+I0DFENXELom8Wgb8gHa2+nM1aPCEGOPbWAbTrFpqO/Kbu7UqFVhf5IugeYv D+aFwr7MG3GmWC2ClagNuZDiCzdNxtb+cm8fhtrFWn/XYfmZxm8Y7oVxXU9xbw5gG+PNHZJa 2AtNRMQ6OfJtWUB3agsfg4JpmBoJuSFhSuDuuzRK5JN9OBuHjwxjOVCpnIz17pS6ihAAv1zg irb6NB08DTE2qGCzCRqVB1Wp3NFnoWO6A95JajX/59SVGrW5xkN4E2fDh0Lo51uDdil6MUyg pDf0bn+LjtP6Yee5cwHG83dM96KKlIkOBvtXSbaVU4LFGH2c27YgENZnbeZ8Xjf/f1Y4tD83 ZEJTLFcTlk8EPgXX19kENI1K5ByRjo4kLSfgabgClKxqRDQQINRuZWVD5p65N3gLT+Yif9PY B5amdsQzKwWP4z/nlRsMxx0xduXXUXXWt9Jr2tqaQpm+C1w
Ironport-sdr: 6705adb8_S0Zdu2xUh5az90O5seMZtq6kjO0JYbOJF+25SwFZTh6R3aH k5iY0cLdtzkI/NF/mn8vi1ACFqUP3iJ0x2FIt3g==

-----------------------------------------------------------------------------------------------------------------------------------
**
** Update: Extended submission deadline
**
-----------------------------------------------------------------------------------------------------------------------------------
**
** CALL FOR EXTENDED ABSTRACTS
**
** Dafny at POPL 2025
** 2nd Workshop on the Dafny Programming and Verification Language
** 19th of January 2025, Denver, Colorado, United States
**
** Extended Submission Deadline:
** October 30, 2024
**
** https://popl25.sigplan.org/home/dafny-2025
** https://dafny25.hotcrp.com
**
-----------------------------------------------------------------------------------------------------------------------------------

Dafny is a verification-aware programming language that has native support for specifications
and proofs, and is equipped with an auto-active static program verifier. The workshop aims to
provide a platform for reports about applications of Dafny in industry, research on programming-
language concepts that are relevant to Dafny, and talks about Dafny’s role in teaching. Topics
include but are not limited to the following:

- Alternative verifier backends
- Coinduction and corecursion
- Comparison with other auto-active program verifiers (SPARK, F*, Why3, Viper, Whiley, …)
- Comparison with other proof assistants (Coq, Isabelle/HOL, Lean, …)
- Dafny in teaching
- Dynamic frames vs. separation logic vs. ownership
- Extensions and applications of Dafny
- Interactive theorem proving and SMT automation
- Logical foundations for Dafny (partial functions, nonempty types, extreme predicates, …)
- Program verification at industry-scale
- Relation to Hoare logic, Incorrectness logic, Outcome logic, over- and under-approximation, …
- Specification and proof inference for Dafny
- Test generation for Dafny
- Translation to or from Dafny and other languages

-----------------------------------------------------------------------------------------------------------------------------------
** IMPORTANT DATES
-----------------------------------------------------------------------------------------------------------------------------------

- Submission: Wednesday, October 30, 2024 (AoE)
- Notification: Wednesday, November 20, 2024
- Workshop: Sunday, January 19, 2025

-----------------------------------------------------------------------------------------------------------------------------------
** SUBMISSION GUIDELINES
-----------------------------------------------------------------------------------------------------------------------------------

To give a presentation at the workshop, please submit an anonymous extended abstract
(2-6 pages, excluding references) via hotcrp:

https://dafny25.hotcrp.com

Please use the acmart two-column sigplan sub-format LaTeX style to prepare
your submission:

https://www.sigplan.org/Resources/Author/

The workshop won’t have formal proceedings. However, presentations may be recorded and the

videos may be made publicly available. You are free to submit work for presentation that is or will

be published elsewhere.

-----------------------------------------------------------------------------------------------------------------------------------
** KEYNOTE
-----------------------------------------------------------------------------------------------------------------------------------

Nada Amin (Harvard University)

-----------------------------------------------------------------------------------------------------------------------------------
** ORGANISATION
-----------------------------------------------------------------------------------------------------------------------------------

Program Committee Chairs:
- Stefan Zetzsche (Amazon Web Services)

Program Committee:
- Seth Ahrenbach (Beneficial AI Foundation)
- Tej Chajed (University of Wisconsin–Madison)
- Alastair F. Donaldson (Imperial College London)
- Marie Farrell (The University of Manchester)
- Bryan Parno (Carnegie Mellon University)
- Clément Pit-Claudel (EPFL)

Steering Committee Chairs:
- Rustan Leino (Amazon Web Services)
- Joseph Tassarotti (New York University)
- Jean-Baptiste Tristan (Amazon Web Services)

-----------------------------------------------------------------------------------------------------------------------------------
** CONTACT
-----------------------------------------------------------------------------------------------------------------------------------

All questions about submission should be emailed to the program chair Stefan Zetzsche
(stefanze AT amazon.com).

[Coq-Club] Dafny Workshop at POPL 2025 (deadline extension), Stefan Zetzsche, 10/09/2024