VSS 2025: International Workshop on Verification of Scientific Software

News

• Dinner! Maccheroni Cucina Alfresco, 6:15 PM. It is a 20 minute walk from workshop venue. For those who want to walk together, we will meet in the main lobby and depart at 5:55 PM.
• Challenge drafts added.

About

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.

Keynote Speakers

Andrew Appel, Princeton University, US

• Title: Foundational end-to-end verification of numerical programs
• Abstract: Program verification is foundational when it assumes only the axioms of logic, the specification of the machine to be run on, and the specification of desired input/output behavior. It is end-to-end when the machine model is low-level, the desired specification is high-level, and all the component verifications compose together into a single machine-checked theorem. Foundational E2E verification has been demonstrated in a few application domains (cryptography, operating systems, compilers). Now it's time to apply it to scientific computing. This requires several different kinds of proofs: correctness of a low-level program w.r.t. a floating-point functional model, data structure proofs, floating-point round-off error analysis, method-error bounds, convergence proofs. Each kind of proof needs its own tools and libraries, and its own experts. Fortunately, the proof assistants for a logical framework provides a structure in which all these tools and libraries can connect, and these experts can collaborate.

• Bio: Andrew W. Appel is the Eugene Higgins Professor of Computer Science at Princeton University. His first work in scientific computing (undergraduate thesis 1981, journal publication 1985) was the invention of the "tree code," an efficient divide-and-conquer algorithm for N-body problems widely used in astrophysical simulations. Since 1983 he has worked in programming-language semantics, functional programming, compilers, machine-checked program verification, and technology policy. He has verified programs in the application domains of compilers, operating systems, cryptography, networks, and (since 2020) formally verified numerical methods.

Jacob Laurel, Georgia Tech, US

• Title: Automated Program Analysis for Scientific Software
• Abstract: Program Analysis has successfully solved a variety of problems across multiple areas including software engineering, compilers, security, and most recently machine learning. Despite these successes, the application of program analysis to scientific computing remains understudied. Further, the few existing techniques that analyze scientific software focus mainly on lower-level concerns such as floating-point stability. While those issues remain important, scientific programs must also obey higher-level mathematical properties for which there do not exist any automated program analyses. Despite this need, a gap exists between the scientific computing community and the programming languages and formal methods community.
  As a step towards bridging this gap, this talk describes why automated program analysis, in particular abstract interpretation, offers a natural way to reason about the programs encountered in scientific computing. I will also discuss how one can cleanly formalize new domain-specific properties from scientific computing in the language of abstract interpretation and focus on applications found in Automatic Differentiation and Bayesian inference. Beyond abstract interpretation, this talk will highlight why the entire program analysis, testing, and formal methods toolkit offers new opportunities to ensure safe and correct scientific software.

• Bio: Jacob Laurel is an Assistant Professor in the School of Computer Science at Georgia Tech. Jacob completed his PhD in Computer Science at the University of Illinois Urbana-Champaign in Fall 2024. Jacob’s research interests center upon applying insights from continuous mathematics to build program analyses for differentiable and probabilistic programming languages. His current research focuses on building precise, general and scalable static analyses for Automatic Differentiation and other scientific computing applications. He earned bachelors degrees in both Electrical Engineering and Applied Mathematics (Scientific Computation Track) at the University of Alabama at Birmingham.

Organization

• Ganesh Gopalakrishnan, University of Utah
• Stephen Siegel, University of Delaware

To send a message to the organizers, email vss2025@googlegroups.com.

• 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

Call for papers

We are interested in submissions dealing with all aspects of the verification problem as it applies to scientific software.

We plan to publish the accepted papers on this web site shortly before the workshop. After the workshop, authors will be given a month to revise their manuscripts and the final versions will be published in a volume of the Electronic Proceedings in Theoretical Computer Science.

All submissions must be unpublished and not be under review elsewhere. Experience reports, novel expositions of previous work, position papers, and reports on preliminary work are all welcome.

Manuscripts should be prepared using the EPTCS LaTeX style. There are two kinds of papers: short (4–6 pages, excluding references) and regular (7–11 pages, excluding references). Each submission will be reviewed by at least 3 members of the Program Committee. At least one author of each paper is expected to register for and attend the workshop in person to present the paper.

Submission instructions: Email your paper as a single PDF file to: vss2025@googlegroups.com, on or before February 1, 2025 (any time on earth). Use the subject line “VSS 2025 Submission”. Papers must be prepared using the EPTCS latex style (see above) and must include an abstract and the names and email addresses of all authors. The organizers will reply to the email to confirm receipt of the paper.

Important Dates:

Travel Scholarships for U.S. Students

Thanks to a grant from the U.S. National Science Foundation, scholarships are available for select students at U.S. universities to travel to and participate in VSS 2025. If you are interested in this opportunity, send an email to vss2025@googlegroups.com with subject line “VSS 2025 Student Scholarship” by February 2, 2025 (any time on earth), with the following information:

Your name:
Your university:
Your student status (degree sought, major, year):
Are you a (co-)author on a paper submitted to VSS 2025?
If you answered "yes" above, enter the title of your paper:
If your paper is accepted and you attend VSS 2025, will you be presenting the paper?
Describe your background and interest in this area in one paragraph:

Program

Challenge Problems

• siegel-fc-vss2025.pdf
• zhang-spmd-vss2025.pdf
• hovland-mpich-vss2025.pdf