VSL | Publications

MADRE: The Memory-Aware Data Redistribution Engine
Stephen F. Siegel and Andrew R. Siegel, Tech. Rep. UDEL-CIS 2009/335, April 2009

UNIC Code: Algorithmic Specification of the Method of Long Characteristics
Stephen F. Siegel, Andrew R. Siegel and Cristian Rabiti, ANL/MCS-TM-301, 2008

MADRE: The Memory-Aware Data Redistribution Engine
Stephen F. Siegel and Andrew R. Siegel, EuroPVM/MPI 2008

Analyzing BlobFlow: A Case Study Using Model Checking to Verify Parallel Scientific Software
Stephen F. Siegel and Louis F. Rossi, EuroPVM/MPI 2008

Combining Symbolic Execution with Model Checking to Verify Parallel Numerical Programs
Stephen F. Siegel, Anastasia Mironova, George S. Avrunin, and Lori A. Clarke, ACM TOSEM 17, 2008

A Case Study in the Use of Model Checking to Verify Parallel Scientific Software
Stephen F. Siegel, Samuel E. Moelius III, and Louis F. Rossi, Tech. Rep. UDEL-CIS 2007/343, 2007

Transparent Partial Order Reduction
Stephen F. Siegel, Tech. Rep. UDEL-CIS 2007/341, 2007

Verification of Halting Properties for MPI Programs Using Nonblocking Operations
Stephen F. Siegel and George S. Avrunin, EuroPVM/MPI 2007

Verifying Parallel Programs with MPI-Spin
Stephen F. Siegel, EuroPVM/MPI 2007 (tutorial)

Model Checking Nonblocking MPI Programs
Stephen F. Siegel, VMCAI 2007

Using MPI-Spin to Model Check MPI Programs with Nonblocking Communication
Stephen F. Siegel, EuroPVM/MPI 2006 Late and Breaking Results

Using Model Checking with Symbolic Execution to Verify Parallel Numerical Programs
Stephen F. Siegel, Anastasia Mironova, George S. Avrunin, and Lori A. Clarke, ISSTA 2006

Finite-state verification for high performance computing
George S. Avrunin, Stephen F. Siegel, and Andrew R. Siegel, SE-HPCS 2005

Modeling wildcard-free MPI programs for verification
Stephen F. Siegel and George S. Avrunin, PPoPP 2005

Efficient verification of halting properties for MPI programs with wildcard receives
Stephen F. Siegel, VMCAI 2005

Modeling MPI programs for verification
Stephen F. Siegel and George S. Avrunin, Tech. Rep. UM-CS-2004-75, 2004

Verification of MPI-based software for scientific computation
Stephen F. Siegel and George S. Avrunin, SPIN 2004

Analysis of MPI programs
Stephen F. Siegel and George S. Avrunin, Tech. Rep. UM-CS-2003-036

Hochschild cohomology and elementary abelian subgroups
Stephen F. Siegel, Trans. Amer. Math. Soc. 358, 2006

The INCA Query Language
Stephen F. Siegel, Tech. Rep. CMPSCI TR 02-18, May 2002.

Improving the precision of INCA by eliminating solutions with spurious cycles
Stephen F. Siegel and George S. Avrunin, IEEE TSE, 2002 no. 2

Improving the precision of INCA by preventing spurious cycles
Stephen F. Siegel and George S. Avrunin ISSTA 2000

Comparing finite-state verification techniques for concurrent software
George S. Avrunin, James C. Corbett, Matthew B. Dwyer, Corina S. Pasareanu, and Stephen F. Siegel, Tech. Rep. UM-CS-1999-069, 1999.


VSL