The Coq mailing list

[Alex Sanchez-Stern <alex.sanchezstern AT gmail.com>]

Hey coq club folks!

The First International Workshop on Deep Learning-aided Verification (DAV 2024) will be colocated with CAV 2024 this year, so please consider submitting!

The call for papers is here on the website: https://dav-workshop-2024.github.io/cfp.html, and can be found below. Paper submission will be due May 2nd.

Scope and Topics of Interest

Deep learning has become state-of-the-art for many human-like tasks, such as computer vision or translation. The persistent perception remains that deep neural networks cannot be applied in computer-aided verification tasks due to the complex symbolic reasoning involved. Recently, this perception has started to shift: massive leaps in architecural design enabled the successful application of deep neural networks to various formal reasoning and automatic verification tasks (Examples include SAT and QBF solving, higher-order theorem proving, LTL satisfiability and synthesis, symbolic differentiation, autoformalization, and termination analysis). The workshop on Deep Learning-aided Verification (DAV) aims to cover this unexplored research area in all its facets.

We cover the recent highlights and upcoming ideas in the intersection between computer-aided verification and deep learning research. The workshop provides a platform to bring together industry and academic researchers from both communities, attract and motivate young talent, and raise awareness of new technologies

Computer-aided verification research will benefit from developing hybrid algorithms that combine the best of both worlds (efficiency and correctness), and machine learning researchers will gain novel application domains to study architectures and a model's generalization and reasoning capabilities.

Topics of interest include, but are not limited to:

• - use of large language models for automated verification and synthesis
• - deep learning heuristics for performance gains in automated verification domains, such as model checking, synthesis, theorem proving, or SAT/SMT solving
• - deep learning guidance for software and hardware synthesis
• - accessibility and explainability of verification and synthesis tools
• - autoformalization of mathematics, logics, and formal specifications from informal natural language
• - deep learning for end-to-end solving of verification tasks
• - application of deep learning to runtime verification.

The workshop focuses on how to use deep learning in verification, not to verify neural networks.

Submission

People interested in contributing to this workshop are invited to contribute short talks.

DAV'24 welcomes the following submissions:

• Extended Abstracts (up to 3 pages, excluding references and clearly marked appendices).

All submissions should be in the two-column sub-format of the ACM proceedings format. The review process is single-blind. Submissions will be judged on how interesting they are to the intersection of the deep learning and formal methods communities. Overlap with previously published work should be indicated, but does not disqualify a submission if the presentation can be expected to be of enough interest. Printouts of the extended abstracts will be handed out at the workshop.

Submissions will be accepted via openreview.

The submission link is open: Submission Link.

Cheers,

Dr. Alex Sanchez-Stern