coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Stefan Zetzsche <stefanzetzsche AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] (CfP) Dafny Workshop at POPL 2025
Date: Thu, 22 Aug 2024 15:18:50 +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-pj1-f53.google.com
Ironport-data: A9a23:jTvJ/Kguy1nYmKsDmE2POHzSX161+hQKZh0ujC45NGQN5FlHY01je htvDT3QPfyLNGehett2a4vnoE8HvceGytI1TVc6/H09F3hjpJueD7x1DG+gZnLIdpWroGFPt phFNIGYdKjYaleG+39B55C49SEUOZmgH+a6UqieUsxIbVcMYD87jh5+kPIOjIdtgNyoayuAo tqaT/f3YTdJ4BYqdDtMg06/gEk35qiq6GlC5gBWic1j5TcyqVFFVPrzGonqdxMUcqEMdsamS uDKyq2O/2+x13/B3fv4+lpTWhRiro/6ZWBiuFIOM0SRqkQqShgJ70oOHKF0hXG7JNm+t4sZJ N1l7fRcQOqyV0HGsLx1vxJwS0mSMUDakVNuzLfWXcG7liX7n3XQL/pGMwITO7Ug/fRLE1oSz KBACAE/YCvEiLfjqF67YrEEasULKcDqOMYHuCglw2yCS/khRp/HTuPB4towMDUY3JgfW6aDI ZBAN3wyN3wsYDUXUrsTIIkikemhgGvyby9Do1KYjaUy6mnXigd21dABNfKEJoHQHpkNwC50o ErtwnnWJAE0DeCVzGCjyXOHg8yXwi/kDdd6+LqQraMz2ALCmAT/EiY+Xlyi5PK9l0SWQMNaM 0VS+yw0rKF0+lbDczXmdxixoXrBphxFHtQNSKs17waCzqeS6AGcboQZctJfQONlkckOfTs46 k2yw+q1XRxegrOuDn3Io994sgiOESQSKGYDYwoNQg0E/8TvrekPYvTnHocL/Emd3o2dJN3g/ w1muhTSkFn6sCLm/6Cy/FSCmzD145aUFUg64QLYWm/j5QR8DGJEW2BKwQmAhRqjBN/GJrVkg JTis5bFhAzpJc/X/BFhuM1XQNmUCw+taVUwe2JHEZg77CiK8HW+Z41W6zwWDB42aJpeJ2KwP RKK5V05CHpv0J2CPf4fj2WZW5RC8EQcPY68PhwpRoMRMsgvK1XflM2QTRXJhDC9zyDAbp3Ty b/ALJ/0UidEYUiW5DWxQOgZ3PcqwCt4rV4/triqpylLJYG2PSbPIZ9caAXmRrlgsMus/l+Jm /4BbJDi40sEAIXDjtz/q9F7waYidihlW/gbaqV/Koa+H+aRMDx6Ua6JmelwIOSIXc19z4/1w 510YWcAoHKXuJENAVzihqlLMeu1A8RMvjggMDYyPF2l/XEmbMz9pO0cbpY7N/1vvuBq0fc+H bFPdtSiE8Z/bG3N2w0cSp3h861kVhCg3jyVMwSfPTMQQp9HRi7ywOHCQDfBzic1IxCMhZMMm IH4jgL/argfdjtmF/fTOa6OzUvunH0zm9BSfkrvI/tVcnrC6IJBdi771Kc2B+ouKhzz4CSQ+ CjLIBUfpMjL+5QU9vuQj4+6jo6ZKclMNWsEIHv6tJGdKjv/0le457N5QMKkXGz4RXzl3qePf sBXxKzMC+IGl1N0rIZMKbZn4qYg7d/JpbUB7ABbMFjUTlasGJVyC2Kn2JRRi6hz2bNpgwu6d UaR8N18O7/SGsfEEkYUFTU1fNa4yvAYtTnD38sbeHygyndMw4OGdkFOMz2nqi9XduJ1Obx45 9YRgpcd7gjnhyc6NtqDsDtvyF2NCX49SIQiiIARBd76qwgsy2waW6fmNA3N3MitZelPY24QG R3FoIrZhr9Z+FjOTGprK1jJwthmpMovvDJk8QY8Amqny/v/u+8P/RxO8D4IYBxf4TdZ3slSZ GV6FU1HCp+f3jVvhcJ8cXimMFheDR+05n7z9kktkWHHRROkTV72cW83Y76M2Gs78GtsWCdR0 5/F6WTiUBfsJNrQ2AlrU2FbivXTd/5D3Sycp9KCAOKEAIgcXTrppoSMdFg4gULrLu1pjXKWu NQw2vh7bJPKEBI5ooo5OtG87qsRQhXVH15ya6ht041RFF6NZQzo/yaFLn2wXcZ/J/bq10ucI O42L+JtUyWO7gq/ngo5N4UtfYAtxOUI4eAccIzFPWQF6ruTjgR4uaLqqxTRujUZfMVMo+0cd KXqaDOwIk6BjyB1mkjMjvV+FEiWXN0mXDD4jceJqLgnNpRbq+x9U1AA4p3ttVWvDQZX1Ra1v gTCWqzo89Jf2blcx7XLLKESKDi3ePXSVfuJ+j+dq95hT83CGuaQuhI3qmvIBRV3P7wQaY4ul b2yr8PGhhLZnbcpUlL2n4uKOLlJ6P6TAstWEJPTB1tLkRSSXPTD50M4xFm5DphSgfVh6dKCV SLhTOeNLfsuRMZ66FhOTipvAzIxKv/QUP/7hCWfq/+sNEAs4TbfJon6yU6zPHBpSCAYHrbfV CrmsOmKzfJFpt1uABQkOalXM6VgKgW+ZZp8JszDjhjGPGyGmVjYh6DDkyAn4jT1CnWpNsb2z JbGZxrmfiSJp6D644BFgrN2oyEoIi5xscsocmIZ3uxGuTSwIWoFDOYaaLEtKJVflA7s35DZO hDJSkYfChvGYDcVSiWkvezfXTqeCNJXa529bnYs8liPYii7OJKYDfEzvm186nNxYX34wPvhN dga/WbqMwOsxo1yA9we/eG/nfwt08ayKqjkIqwhu5ea79ci7bQ2OLhJGQNMUWnfEZiImhiQY 2cyQm9ATQewTkuZ/QOMvZJKMElxgd8t52xAgeSzLBL3tICSzekGw/r6Uw02+qNWd9wEfdbiW luuL1ZgIAmqNrg7tq4gutZviqhxYR5O8g5WM4e7LTAvc2qMBqjL8i/McefjjC3vxeKHL27gq w==
Ironport-hdrordr: A9a23:HVN1+KkMBw8ZrdnDuyKGGsiBexrpDfIh3DAbv31ZSRFFG/Fw9v re+8jzsCWftN9/YgBCpTntAsm9qBDnlKKdg7NhX4tKNTOO0ACVxepZnO7fKlPbaknDHy1muZ uIsZISNDQ9NzdHZA/BjjWFLw==
Ironport-phdr: A9a23:JYxFiB2LFyLvbK0dsmDOFw4yDhhOgF0UFjAc5pdvsb9SaKPrp82kY BeHo6w31BSWBM3y0LFttan/i+PaZSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQF cVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pDdfwlEniexba1uI Bm5rwjdq9QdjJd/JKo21hbGrXxEdvhMy29vOVydgQv36N2q/J5k/SRQuvYh+NBFXK7nYak2T qFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4 qx2RhLklDsLOjgk+2zRl8d+jr9UoAi5qhNww4DaboKbOudgcKzBZt4VX3ZNU9xLWiBdHo+xb Y0CBPcBM+ZCqIn9okMDowaiBQayCuPg0DlIjWL10qIkz+QgEBrG0xAgH90QrX/Zq871NLsMX uC71qbIyzTCYO1K2Tb884jHbhAhru+XULJ/dMre00gvFwffglqMrozlOiqY2+IQuGeU8+RuT /igi3I7qw5vuDivwN8hh4fUi48Ryl3K9SR0zYUpKNC4R0N2b9GpHptUuiyUN4Z7RsEvTmN0t Cs+xbMLp4C3cDYKxpkk2hLRZeCLfoiH7B/lSe2fLzB4hHd/d7K+gRa/6VOgyuzzVsms1FZFt CxFnsPLtnAX2Bzf8siHSvxh/ki9wzaPzxrf5f1DIUAxk6fQNp0vwqYom5YNrUjOGjX6lUb2g aOMaEko5+ml5/7nb7jooJKXKpF5igXjMqQ1hsywH/44PBUPX2ma5+uxzKHv8EvkS7tQlPI2i LPWsJXCKMQbuKG5BwhV354m6xmlDjem1M0UnWEFLF5YYR6HgYjkNl/ULPD3Cve/hFuskDN1y PzcIrLhBZDNImDCkLfnY7l991ZRxBQvwd1b/Z5ZCbEMLOjtVkPstdHUFB80PgKsz+biEtp91 4ceWWyVAq+eNaPfqUSI5v4xLOmCfoAVvjf8JOY55//vln82hV8dcrey0JsYbXC3BPVmI0GDb XXwhdcBFH8GvgwlQ+Pykl2NTSZTZ2quX6I7/jw3FZqqDZ3fSYC1nLyBwCC7E4VKaWBBE1CAC Gvnd4GZW/gXcy+SOc9gkjkcVbe7UYMh1BeutBX7y7V9NObU9DcY5trf041+4PSWnhUv/xR1C d6c2ieDVTJahGQNEgQq0a52pwRPx0uRyqN4jrQMDsBe6fpPQAomJ4XXz+FSBNX7WwaHddCMH gX1Cu66CC08G4pii+QFZFxwTo3KZnHr2iOrB+RQjLmXHNkv9bqa2XHtJsF7wnKA1a87jlBgT NEcfXa+iPtZ8A7eT5XMj13fj7yjIL8A0SDE8nWO0XiVt0FVeAF1WKTBG3sYYxietsz3s3vLV KTmErE7Kk1EwM+GJLFNb4jykVhITfHxNcjMeGmxlk+/AB+JwvWHa4+5M34F0nD7D04J2xsW4 W7ANQU6AXK5pHnCCTV1CV/1S0bl8O07sHHiC0FplEeFaEpu07fz8RkQ7RCFY9UU2L9M+CIoq jEvWU24w8qTEN2Y4QxoYKRbZ9o5plZBz2PQ8QJnbNSmKOh5i1gSfh4S3Qum3ghrCohGjckhr W87hAt0J6WC1VpddjSelZnuM7zTI2P28VihcanTkl3Z1d+X/O8I5pFa4x34oAynH0ww/ml1y NJV3lOT45zLCEwZVpewGkc7+h5mpq3LNzEn7tCxtzUkOq21vznentMxUbF9m1DwIpEFaf3CS VShdq9ST9KjI+ErhVWzOxcNPeQJsbUxI9vjbPyenqiiIOdnmjuiy2VB+oF0lEyWpE8eAqbF2 YgIx/aA006JTTD52R26rs35kIZWaC0ABWG/xADrAYdQYut5eoNBWgLMa4Wng85zgZLgQSsS7 0KuCVoAysK1awGZb1HV0ghZ1EBRqnui03jdrXQ8g3QiqayR2zbLyuLpeU8cO2JFc2JliE/lP Ym+i91ysFGAVwEyj1Pl4E/7w/Mev6FjNyzIRl8OeSHqLmZkW6/2t7yYYscJ5ol6+SlQVe29Z xidRNuf61MBzy7tFm1MySwpbDqqt732mhV7jCSWK3M7oHfCeM52zAvS/5SGHa8XjmdAHnAmz 2SMTlGnWrvhtc2ZjZLCrvyzWyq6W5tffDOqhYKMuS2n5HF7VBi2nvS9gNriQkAx1S720cUvV D2d9k6tJNm2kf7jb6Q6JRoNZhe08cdxF4Bgn5FlgZgR3SNfnZCJ5T8cln+1N9xH2KX4ZX5LR DgRwteT7hK2vS8rZn+P2Y/9UW2Qh8V7YNzvKHgK1yw06dJHFLWP57xJtSRwq1u86wnWZLIu+ 1VVgetr83Mcj+wT7UA20iiTC7YAEFVKJifsmjyH6tm/qONcY2PlIt3SnAJu2NumCr+FuARVX n30L4wjESFH5cJ6KFvQ0Xf359KsaJzKYNkUrBHRjwbYgr0fNscqjvRTz3kCWyq1rTg/xuU8l xArwZyqoN3NNTB25KzgSh9Aam+uOoVKq2mr1/oB2J7RhdznH409SGtXGsGzFrTxTmpU7bO+Z mPsWHU9sivJR+SZRFfFrh8g9zWVS9iqLy3Feidfl4kzAknFYhQY2lhcXS1mzMFjUFn2gpWwK gEhoWlBgzyw4hpUlrA3a1+mCDqZ/EHwLW5qAJmHcEgPtlEEvhiKd5zYtqUpRmlZ5sHz9VPWb DXKO0IQSzlOAxLhZRirP6Hyt4OYoq7IW6zndauIOfLX9qRfT6van8vxlNY2uW/dbIPXeSAzR /wjhhgZBC4/QZ+I3W5VDXRQznOoDYbTsh64/mcfQtmX1vPtVUqv4IKOD+AXKtBz41Wthr/FM eeMhSF/IDIe15UWxHaOxqJNlFgVwzpjcTWgC9Fi/WbEUb7Ql6lLDhUadzI7Nc1G6Lg51xVMP siTg83817pxhPo4Q1lfUlmplsasbM0Ma2azUTGPTF6ML6iDLCbXztvfZKq9TfhIjrwRuUDr/ zmcFEDnM3KIkDyoHxGjPOdQjT2KaRxTvIbuF3QlQWPnTd/gdli6KIot1WxwkeBy3CqUczNHY l0eOwtXo7ad7D1VmKB6Em1FtT9+KPWc3j2e96/eI4oXtv1iBmJ1kfhb6TI00egwjmkMSfprl S/VttMrrUuhl7zF0SZqXhNIuDtXlpmAvUhKNqDQ950GUnHBtkFojy3YG1ERqt1pB8e68bhX0 cTKnbnvJS1q9tvV+Y4EBZGRJp/cdnUmNhXtFXjfCw5PHlvJfSnPwkdalv+V7HicqJM3/4Ptl JQ5QbheTFUpF/keByyN+fQNJZ52WnUvlrvJ1KbgBFK7pRjVAd1Y59XJC6nUDvLoJzKUy7JDY klQqVsXBYsWP4z/nUdlbwsj9Lk=
Ironport-sdr: 66c748f1_S/698GjzeST4IN7AxhdJPkravR7OjGIZpLIo5GHyEgi1OHl xxb4dyC1JqNIjzp9BmtghBKfADayKvFHCUrY/3w==

-----------------------------------------------------------------------------------------------------------------------------------
**
** 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
**
** Submission Deadline:
** October 16, 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 16, 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/

We don’t intend to publish the workshop’s submissions. However, presentations may be

recorded and the videos may be made publicly available.

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

Program Chairs:
- Stefan Zetzsche (Amazon Web Services)

Steering Committee:
- 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] (CfP) Dafny Workshop at POPL 2025, Stefan Zetzsche, 08/22/2024