The Coq mailing list

[Stephen Siegel <siegel AT udel.edu>]

[Apologies if you receive multiple copies of this CfP]

                               VSS 2025
First International Workshop on Verification of Scientific Software

                           Call for Papers

Web: https://vsl.cis.udel.edu/vss2025/
Submission deadline: February 1, 2025
Workshop date: May 4, 2025
Venue: Hamilton, Ontario, Canada, part of ETAPS 2025

Software plays an increasingly important role in scientific and
engineering disciplines. Climate modeling, weather prediction, drug
discovery, the design of buildings, vehicles, and aircraft,
simulations of astrophysical phenomena, and prediction of seismic
activity are some of the many applications. Verification of such
software presents numerous challenges, e.g.: the programs are large,
complex, and utilize multiple CPU and GPU concurrency interfaces;
precise reasoning about real or floating-point operations is often
required; there is often no oracle; and correctness may require
reasoning about deep mathematical concepts such as convergence and
stability. This workshop will focus on verification techniques that
address these challenges, including approaches based on deductive
reasoning, model checking, symbolic execution, abstract
interpretation, and static analysis.

The workshop will take place as part of ETAPS 2025, on Sunday, May 4,
2025, at McMaster University in Hamilton, Canada. We aim to bring
together researchers from both the scientific computing and the
software verification communities. Through invited talks and
presentations of peer-reviewed papers, participants will learn about
the correctness challenges developers face, as well as a variety of
verification approaches for tackling those challenges. We are
interested in all aspects of the verification problem for scientific
software, including, but not limited to:

- ways to specify scientific software

- reasoning about mathematical concepts realized in software,
including linear algebra, differential equations, convergence,
stability, and order of accuracy

- effective verification techniques for programs that use MPI,
OpenMP, CUDA, or other CPU or GPU concurrency interfaces used in
scientific computing

- precise reasoning about floating-point computations

- techniques to reason about discretization in time and space, such
as discrete grids and adaptive mesh refinement

- case studies applying verification tools to scientific software

- methods to decompose verification problems for scientific
programs, such as function contracts.

Please see the workshop web site https://vsl.cis.udel.edu/vss2025/ for
submission details.

Invited Speaker: Andrew Appel, Princeton Univ.

Workshop Organizers:

Ganesh Gopalakrishnan, University of Utah, ganesh AT cs.utah.edu
Stephen Siegel, University of Delaware, siegel AT udel.edu

Program Committee:

Alastair Donaldson, Imperial College London, UK
Cindy Rubio-González, University of California Davis, US
Dorra Ben Khalifa, ENAC, FR
Erika Ábrahám, RWTH Aachen University, DE
Ignacio Laguna, Lawrence Livermore National Laboratory, US
Jean-Baptiste Jeannin, University of Michigan, US
Kristin Rozier, Iowa State University, US
Marieke Huisman, University of Twente, NL
Paul Hovland, Argonne National Laboratory, US
Samuel Pollard, Sandia National Laboratories, US
Sylvie Boldo, INRIA, FR