
What's wrong with onthefly partial order reduction

Stephen F. Siegel. In Proceedings
of the 31st International Conference on ComputerAided Verification (CAV'19)

Towards Deductive Verification of MessagePassing Parallel Programs

Ziqing Luo and Stephen F. Siegel. In Proceedings
of the 2nd International Workshop on Software Correctness for HPC Applications (Correctness'18)

Symbolic Execution
and Deductive Verification Approaches to VerifyThis 2017
Challenges

Ziqing Luo and Stephen F. Siegel. In Proceedings
of 8th international symposium on leveraging
applications of formal methods, verification and
validation (ISoLA'18)

Verifying Properties of Differentiable Programs

Jan Hückelheim, Ziqing Luo, Sri Hari Krishna Narayanan,
Stephen Siegel, Paul D. Hovland. In Proceedings
of 25th Static Analysis
Symposium (SAS'18)

Report of the HPC Correctness Summit

Ganesh Gopalakrishnan, Ganesh Gopalakrishnan, Ganesh Gopalakrishnan
, Sriram Krishnamoorthy, Ignacio Laguna, Richard A. Lethin,
Koushik Sen, Stephen F. Siegel, Armando SolarLezama,
Report of the HPC Correctness Summit Jan 2526, 2017, Washington, DC

Towards SelfVerification in Finite Difference Code Generation

Jan Hückelheim, Ziqing Luo, Fabio Luporini, Navjot
Kukreja, Michael Lange, Gerard Gorman, Stephen Siegel,
Matthew Dwyer, and Paul Hovland. In Proceedings
of the First International Workshop on Software
Correctness for HPC Applications (Correctness'17)

Verification of MPI programs using CIVL

Ziqing Luo, Manchun Zheng, and Stephen F. Siegel. 2017. In Proceedings of the 24th European MPI Users' Group Meeting (EuroMPI '17).ACM, New York, NY, USA, Article 6, 11 pages.

CIVL Solutions to VerifyThis
2016 Challenges

Stephen F. Siegel (2017, April). CIVL Solutions to VerifyThis 2016
Challenges. ACM SIGLOG News, 4, 55–75.

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. UDCIS 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. UDCIS 2014/001, 2014

Dynamic Barrier Relaxations
for Explicit Stencil Computations

Adam Hammouda, Andrew R. Siegel, and Stephen F. Siegel, Tech.
Rep. UDELCIS 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 MPIbased
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):8291, December 2011.

Reexamining Two Results in Partial
Order Reduction

Stephen F. Siegel, Tech. Rep. UDELCIS 2011/06, 2011

Automatic Formal Verification of
MPIBased Parallel Programs

Stephen F. Siegel and Timothy K. Zirkel, PPoPP 2011

A Functional Equivalence
Verification Suite for HighPerformance 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 MemoryAware Data
Redistribution Engine

Stephen F. Siegel and Andrew R. Siegel, International
Journal of High Performance Computing Applications 24,
Feb. 2010

A MemoryEfficient Data
Redistribution Algorithm

Stephen F. Siegel and Andrew R. Siegel, EuroPVM/MPI 2009

Verification of
MPIbased 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/MCSTM301,
2008

MADRE: The MemoryAware 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. UDELCIS 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 MPISpin

Stephen F. Siegel, EuroPVM/MPI 2007 (tutorial)

Model Checking
Nonblocking MPI Programs

Stephen F. Siegel, VMCAI 2007

Using MPISpin 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

Finitestate
verification for high performance computing

George S. Avrunin, Stephen F. Siegel, and Andrew R. Siegel, SEHPCS
2005

Modeling wildcardfree 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.
UMCS200475, 2004

Verification of MPIbased
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.
UMCS2003036

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 0218, 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 finitestate
verification techniques for concurrent software

George S. Avrunin, James C. Corbett, Matthew B. Dwyer, Corina S.
Pasareanu, and Stephen F. Siegel, Tech. Rep.
UMCS1999069, 1999.
VSL