WAVE

There is an established group of verification-aware programming languages that have native support for specifications and proofs, and are equipped with an auto-active static program verifier. Examples of such languages are Dafny, SPARK, F*, Why3, Viper, Whiley. Auto-active tools also exist for other languages like C, Java or Rust. The workshop aims to be a forum for all auto-active program verifiers and their related techniques.

It is the 4th edition of this workshop, which was previously called the Dafny Workshop.

Topics include but are not limited to the following:

• AI for verification and vice versa
• Alternative verifier backends
• Coinduction and corecursion
• Comparison with interactive proof assistants (Rocq, Isabelle/HOL, Lean, …)
• Dynamic frames vs. separation logic vs. ownership
• Extensions and applications of the auto-active language
• GUI and IDE for auto-active verification
• User interaction features
• Logical foundations (partial functions, nonempty types, extreme predicates, …)
• Program verification at industry-scale
• Relation to Hoare logic, Incorrectness logic, Outcome logic, over- and under-approximation, …
• SMT automation
• Specification and proof inference for the auto-active language
• Test generation
• Translation to or from the auto-active language
• Verification in teaching

Call for Papers

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.

Important Dates

Submission: 7 Oct 2026 (AoE)

Notification: 11 Nov 2026 (AoE)

Workshop: 10 Jan, 2027

Submission Guidelines

To give a presentation at the workshop, please submit an anonymous extended abstract (2-6 pages, excluding references) via hotcrp: TBD. Please use the acmart two-column sigplan sub-format LaTeX style to prepare your submission: https://www.sigplan.org/Resources/Author/

Contact

All questions about submission should be emailed to the program chairs Nada Amin (namin@seas.harvard.edu) or Yannick Moy (yannick.moy@gmail.com).