VSL Publications
CIVL: Applying a General Concurrency Verification Framework to C/Pthreads Programs (Competition Contribution)
Manchun Zheng, John G. Edenhofner, Ziqing Luo, Mitchell J. Gerrard, Michael S. Rogers, Matthew B. Dwyer, and Stephen F. Siegel SVCOMP 2016

CIVL: The Concurrency Intermediate Verification Language
Stephen F. Siegel, Manchun Zheng, Ziqing Luo, Timothy K. Zirkel, Andre V. Marianiello, John G. Edenhofner, Matthew B. Dwyer, Michael S. Rogers, SC 2015

CIVL: Formal Verification of Parallel Programs
Manchun Zheng, Michael S. Rogers, Ziqing Luo, Matthew B. Dwyer, Stephen F. Siegel, ASE 2015

Using Symbolic Execution to Verify the Order of Accuracy of Numerical Approximations
Timothy K. Zirkel, Stephen F. Siegel, and Louis F. Rossi, Tech. Rep. UD-CIS 2014/002, 2014

CIVL: The Concurrency Intermediate Verification Language
Stephen F. Siegel, Matthew B. Dwyer, Ganesh Gopalakrishnan, Ziqing Luo, Zvonimir Rakamaric, Rajeev Thakur, Manchun Zheng, and Timothy K. Zirkel, Tech. Rep. UD-CIS 2014/001, 2014

Dynamic Barrier Relaxations for Explicit Stencil Computations
Adam Hammouda, Andrew R. Siegel, and Stephen F. Siegel, Tech. Rep. UDEL-CIS 2013/002, 2013

Automated Verification of Chapel Programs Using Model Checking and Symbolic Execution
Timothy K. Zirkel, Stephen F. Siegel, and Timothy McClory, NFM 2013

Loop Invariant Symbolic Execution for Parallel Programs
Stephen F. Siegel and Timothy K. Zirkel, VMCAI 2012

Transparent Partial Order Reduction
Stephen F. Siegel, Formal Methods in System Design 40(1):1–19, 2012.

Formal Analysis of MPI-based Parallel Programs
Ganesh Gopalakrishnan, Robert M. Kirby, Stephen Siegel, Rajeev Thakur, William Gropp, Ewing Lusk, Bronis R. De Supinski, Martin Schulz, and Greg Bronevetsky, Communications of the ACM 54(12):82--91, December 2011.

Reexamining Two Results in Partial Order Reduction
Stephen F. Siegel, Tech. Rep. UDEL-CIS 2011/06, 2011

Automatic Formal Verification of MPI-Based Parallel Programs
Stephen F. Siegel and Timothy K. Zirkel, PPoPP 2011

A Functional Equivalence Verification Suite for High-Performance Scientific Computing
Stephen F. Siegel and Timothy K. Zirkel, Mathematics in Computer Science 5(4):427–435, 2011.

Formal Analysis of Message Passing
Stephen F. Siegel and Ganesh Gopalakrishnan, VMCAI 2011

Collective Assertions
Stephen F. Siegel and Timothy K. Zirkel, VMCAI 2011

The Toolkit for Accurate Scientific Software
Stephen F. Siegel and Timothy K. Zirkel, Mathematics in Computer Science 5(4):395–426, 2011

MADRE: The Memory-Aware Data Redistribution Engine
Stephen F. Siegel and Andrew R. Siegel, International Journal of High Performance Computing Applications 24, Feb. 2010

A Memory-Efficient Data Redistribution Algorithm
Stephen F. Siegel and Andrew R. Siegel, EuroPVM/MPI 2009

Verification of MPI-based Computations
Stephen F. Siegel, Distributed Verification and Grid Computing, Dagstuhl Seminar Proceedings 08332, 2008

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

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