arXiv subjects

Stephen F. Siegel

Publications and source records attributed to Stephen F. Siegel.

8 recordsLinked to original sources

arXiv2026

Parameterized Verification of Deterministic MPI Programs

We consider the problem of verifying a message passing program in which the number of processes is a parameter NP and each process knows its unique ID. Processes communicate using send and receive commands which specify a single destination or source. To verify the program, the user provides functions specifying the number of messages sent from process i to process j, the level of each communication event in the happens-before hierarchy, and a fact that holds for the k-th message sent from i to j. These are used to transform the program to a parameterized sequential program which can be verified using any techniques appropriate for such programs. We realize this approach in an extension to Frama-C/Wp to verify C/MPI programs.

cs.PL↗

arXiv2026

LAP: Simple Command-line Tools for Teaching Logic, Algorithms, and Proof in Computer Science

The LAP toolset is a set of command line tools for teaching logic in computer science. It provides implementations of standard algorithms for propositional and first order logic, including conversions to various normal forms, propositional satisfiability algorithms such as DPLL, Tseytin's transformation, and equivalence checking. Significantly, LAP also supports a language for expressing a natural deduction derivation for propositional or first order logic. The tools can check the derivation, provide meaningful feedback if it is wrong, or display the derivation in a variety of formats. The toolset is written in Java and has no dependencies other than a Java Virtual Machine. The code has been designed to be easy to read and to illuminate the data definitions and algorithms.

cs.LO↗

arXiv2025

Specification and Verification for Climate Modeling: Formalization Leading to Impactful Tooling

Earth System Models (ESMs) are critical for understanding past climates and projecting future scenarios. However, the complexity of these models, which include large code bases, a wide community of developers, and diverse computational platforms, poses significant challenges for software quality assurance. The increasing adoption of GPUs and heterogeneous architectures further complicates verification efforts. Traditional verification methods often rely on bitwise reproducibility, which is not always feasible, particularly under new compilers or hardware. Manual expert evaluation, on the other hand, is subjective and time-consuming. Formal methods offer a mathematically rigorous alternative, yet their application in ESM development has been limited due to the lack of climate model-specific representations and tools. Here, we advocate for the broader adoption of formal methods in climate modeling. In particular, we identify key aspects of ESMs that are well suited to formal specification and introduce abstraction approaches for a tailored framework. To demonstrate this approach, we present a case study using CIVL model checker to formally verify a bug fix in an ocean mixing parameterization scheme. Our goal is to develop accessible, domain-specific formal tools that enhance model confidence and support more efficient and reliable ESM development.

cs.LO↗

arXiv2025

Proceedings of the International Workshop on Verification of Scientific Software

This volume contains the proceedings of the Verification of Scientific Software (VSS 2025) workshop, held on 4 May 2025 at McMaster University, Canada, as part of ETAPS 2025. VSS brings together researchers in software verification and scientific computing to address challenges in ensuring the correctness and reliability of large-scale scientific codes. The program featured five peer-reviewed papers, three invited contributions, and a set of challenge problems, covering themes such as deductive verification, floating-point error analysis, specification of coupled models, and domain-aware testing. VSS builds on the Correctness Workshop series at Supercomputing and the 2023 NSF/DOE report on scientific software correctness. It serves as yet another snapshot of this important area, showcasing a wide range of perspectives, problems and their solutions in progress, with the challenge problems having the potential to bring together separate verification tools into concerted action.

cs.LO↗

arXiv2023

Report of the DOE/NSF Workshop on Correctness in Scientific Computing, June 2023, Orlando, FL

This report is a digest of the DOE/NSF Workshop on Correctness in Scientific Computing (CSC'23) held on June 17, 2023, as part of the Federated Computing Research Conference (FCRC) 2023. CSC was conceived by DOE and NSF to address the growing concerns about correctness among those who employ computational methods to perform large-scale scientific simulations. These concerns have escalated, given the complexity, scale, and heterogeneity of today's HPC software and hardware. If correctness is not proactively addressed, there is the risk of producing flawed science on top of unacceptable productivity losses faced by computational scientists and engineers. HPC systems are beginning to include data-driven methods, including machine learning and surrogate models, and their impact on overall HPC system correctness was also felt urgent to discuss. Stakeholders of correctness in this space were identified to belong to several sub-disciplines of computer science; from computer architecture researchers who design special-purpose hardware that offers high energy efficiencies; numerical algorithm designers who develop efficient computational schemes based on reduced precision as well as reduced data movement; all the way to researchers in programming language and formal methods who seek methodologies for correct compilation and verification. To include attendees with such a diverse set of backgrounds, CSC was held during the Federated Computing Research Conference (FCRC) 2023.

cs.DC↗

arXiv2023

DataRaceBench V1.4.1 and DataRaceBench-ML V0.1: Benchmark Suites for Data Race Detection

Data races pose a significant threat in multi-threaded parallel applications due to their negative impact on program correctness. DataRaceBench, an open-source benchmark suite, is specifically crafted to assess these data race detection tools in a systematic and measurable manner. Machine learning techniques have recently demonstrated considerable potential in high-performance computing (HPC) program analysis and optimization. However, these techniques require specialized data formats for training and refinement. This paper presents the latest update to DataRaceBench, incorporating new data race contributions from Wu et al. \cite{wu2023model}, and introduces a derived dataset named DataRaceBench-ML (DRB-ML) \cite{drbml}. DRB-ML aligns with the emerging trend of machine learning and large language models. Originating from DataRaceBench, this dataset includes detailed labels that denote the presence of a data race and provides comprehensive details of associated variables, such as variable names, line numbers, and the operation (read/write). Unique to DRB-ML, we have also integrated a series of tailored prompt-response pairs specifically designed for LLM fine-tuning.

cs.SE↗

arXiv2023

Model Checking Race-freedom When "Sequential Consistency for Data-race-free Programs" is Guaranteed

Many parallel programming models guarantee that if all sequentially consistent (SC) executions of a program are free of data races, then all executions of the program will appear to be sequentially consistent. This greatly simplifies reasoning about the program, but leaves open the question of how to verify that all SC executions are race-free. In this paper, we show that with a few simple modifications, model checking can be an effective tool for verifying race-freedom. We explore this technique on a suite of C programs parallelized with OpenMP.

cs.PL↗

arXiv2017

Report of the HPC Correctness Summit, Jan 25--26, 2017, Washington, DC

Maintaining leadership in HPC requires the ability to support simulations at large scales and fidelity. In this study, we detail one of the most significant productivity challenges in achieving this goal, namely the increasing proclivity to bugs, especially in the face of growing hardware and software heterogeneity and sheer system scale. We identify key areas where timely new research must be proactively begun to address these challenges, and create new correctness tools that must ideally play a significant role even while ramping up toward exacale. We close with the proposal for a two-day workshop in which the problems identified in this report can be more broadly discussed, and specific plans to launch these new research thrusts identified.

cs.DC↗