3 citations · 4 across the 5 of their papers we have counts for
6 papers
Verification of PETSc with CIVL using LLM-generated ACSL contracts and deterministic driver generation
Hansol Suh, Jan Hückelheim, Stephen Siegel
Parallel numerical libraries such as PETSc are widely used in science and engineering applications where wrong results can have costly consequences. Despite this, numerical librari…
Parameterized Verification of Deterministic MPI Programs
Stephen F. Siegel
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…
LAP: Simple Command-line Tools for Teaching Logic, Algorithms, and Proof in Computer Science
Stephen F. Siegel, Yuxin Zhou
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, i…
DataRaceBench V1.4.1 and DataRaceBench-ML V0.1: Benchmark Suites for Data Race Detection
Le Chen, Wenhao Wu, Stephen F. Siegel +2
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…
Model Checking Race-freedom When "Sequential Consistency for Data-race-free Programs" is Guaranteed
Wenhao Wu, Jan Hückelheim, Paul D. Hovland +2
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 t…
Report of the HPC Correctness Summit, Jan 25--26, 2017, Washington, DC
Ganesh Gopalakrishnan, Paul D. Hovland, Costin Iancu +6
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…