Verification languages such as, among others, Coq, Lean, Agda, Athena, Liquid Haskell, Maude ,… have become central tools for building reliable software and for advancing formal methods research. While each language has its own community and conference, there is a growing need for a shared forum where researchers can exchange insights across language boundaries.
The First Workshop on Verification Languages aims to bring together researchers, practitioners, and tool developers to discuss common design principles, compare approaches, underlying mathematical theories, capacities, capabilities, and in general share experiences in the development and application of verification languages into modern reliable software systems.
This workshop will be a forum to discuss advances in verification languages and their application, with the objective of breaking the boundaries of a single verification language, that can foster collaboration between researchers of different language backgrounds.
The workshop will feature:
- An invited keynote talk. (TBC)
- Presentations of peer-reviewed papers.
- A Verification Challenge, where participants tackle a proposed challenge using their weapon of choice (e.g., Maude, Adga, Liquid Haskell, Athena…). Then during the workshop we will have space to share/show solutions between the different language, to show case the similarities and differences between verification languages, as possible collaboration points.
Call for Papers
VeriLang seeks submissions of papers discussing the implementation and application of verification languages and their associated tools.
Topics of Interest
We welcome submissions on all aspects of verification languages, including but not limited to:
- Language design and semantics.
- Type systems and logical foundations.
- Integration with automated provers and SMT solvers.
- Tooling, IDEs, Debuggers and usability.
- Verification of software, hardware, and systems.
- Educational use of verification languages.
- Comparative studies of verification languages.
- Case studies and applications.
We invite two categories of submissions:
- Full papers (up to 12 pages, excluding references): Original research contributions, experience reports, or detailed case studies.
- Short papers (up to 6 pages, excluding references): Work-in-progress, new ideas, position papers, or reports on ongoing projects.
Papers accepted for presentation to VeriLang will have a publication at the ACM Digital Library as part of the collaboration between ECOOP and ACM. Therefore, papers should be formatted using the latest version of the ACM proceedings (https://www.sigplan.org/Resources/Author/) using the sigplan subformat.
Paper submission will be though EasyChair
