[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
----------------------------------------------------------------------------------------------------------
**
** CALL FOR EXTENDED ABSTRACTS
**
** Dafny at POPL 2024
** 1st Workshop on the Dafny Programming and Verification Language
** 14th of January 2024, London, United Kingdom
**
** Submission Deadline:
** October 11, 2023
**
**
https://urldefense.com/v3/__https://popl24.sigplan.org/home/dafny-2024__;!!IBzWLUs!XnBuhDPfO8iySlXlAxucYqWgcjFRiJ_AvcL3Stts4ZwdbxSsiseiJcwVuw7kob8ZhtTPk0zkjmpQK9iWBpSLp5EUNntydBtHcogq9Dk$
**
https://urldefense.com/v3/__https://dafny24.hotcrp.com/__;!!IBzWLUs!XnBuhDPfO8iySlXlAxucYqWgcjFRiJ_AvcL3Stts4ZwdbxSsiseiJcwVuw7kob8ZhtTPk0zkjmpQK9iWBpSLp5EUNntydBtHdAhaGBI$
**
-----------------------------------------------------------------------------------------------------------
* OVERVIEW
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:
- Relation to Hoare logic, Incorrectness logic, Outcome logic, over- and
under-approximation, ...
- Interactive theorem proving and SMT automation
- Coinduction and corecursion
- Dynamic frames vs. separation logic vs. ownership
- Test generation for Dafny
- Specification and proof inference for Dafny
- Extensions and applications of Dafny
- Alternative verifier backends
- Program verification at industry-scale
- Translation to or from Dafny and other languages
- Logical foundations for Dafny (partial functions, nonempty types, extreme
predicates, ...)
- Dafny in teaching
- Comparison with other auto-active program verifiers (SPARK, F*, Why3,
Viper, Whiley, ...)
- Comparison with other proof assistants (Coq, Isabelle/HOL, Lean, ...)
-----------------------------------------------------------------------------------------------------------
** IMPORTANT DATES
-----------------------------------------------------------------------------------------------------------
- Submission: Wednesday, October 11, 2023 (AoE)
- Notification: Wednesday, November 15, 2023
- Workshop: Sunday, January 14, 2024
-----------------------------------------------------------------------------------------------------------
** SUBMISSION GUIDELINES
-----------------------------------------------------------------------------------------------------------
To give a presentation at the workshop, please submit an anonymous extended
abstract (2-6 pages, excluding references) via hotcrp:
https://urldefense.com/v3/__https://dafny24.hotcrp.com__;!!IBzWLUs!XnBuhDPfO8iySlXlAxucYqWgcjFRiJ_AvcL3Stts4ZwdbxSsiseiJcwVuw7kob8ZhtTPk0zkjmpQK9iWBpSLp5EUNntydBtHVwlHpIk$
<https://urldefense.com/v3/__https://dafny24.hotcrp.com/__;!!IBzWLUs!XnBuhDPfO8iySlXlAxucYqWgcjFRiJ_AvcL3Stts4ZwdbxSsiseiJcwVuw7kob8ZhtTPk0zkjmpQK9iWBpSLp5EUNntydBtHdAhaGBI$
>
Please use the acmart two-column sigplan sub-format LaTeX style to prepare
your submission:
https://urldefense.com/v3/__https://www.sigplan.org/Resources/Author/__;!!IBzWLUs!XnBuhDPfO8iySlXlAxucYqWgcjFRiJ_AvcL3Stts4ZwdbxSsiseiJcwVuw7kob8ZhtTPk0zkjmpQK9iWBpSLp5EUNntydBtHzcFBSfY$
We don’t intend to publish the workshop’s submissions. However, presentations
may be recorded and the videos may be made publicly available.
-----------------------------------------------------------------------------------------------------------
** CONTACT
-----------------------------------------------------------------------------------------------------------
All questions about submission should be emailed to the program chairs Stefan
Zetzsche (stefa...@amazon.com <mailto:stefa...@amazon.com>) and Joseph
Tassarotti (jt4...@nyu.edu <mailto:jt4...@nyu.edu>).
