-
Collective Contracts for Message-Passing
Parallel Programs
-
Ziqing Luo and Stephen F. Siegel. In Proceedings of the
36th International Conference on Computer-Aided Verification
(CAV 2024)
-
VerifyThis 2023: an International Program
Verification Competition
-
Xavier Denis and Stephen F. Siegel. In TOOLympics Challenge
2023.
-
DOE/NSF Workshop on Correctness in
Scientific Computing
-
Maya Gokhale, Ganesh Gopalakrishnan, Jackson Mayo, Santosh Nagarakatte,
Cindy Rubio-Gonzalez, and Stephen F. Siegel. In arXiv.
-
Model Checking Race-freedom when
“Sequential Consistency for Data-Race-Free Programs”
is Guaranteed
-
Wenhao Wu, Jan Hückelheim, Paul D. Hovland, Ziqing Luo, and
Stephen F. Siegel. In Proceedings of the 35th
International Conference on Computer-Aided Verification
(CAV 2023)
-
Verifying Fortran Programs with CIVL
-
Wenhao Wu, Jan Hückelheim, Paul D. Hovland, and Stephen
F. Siegel. In Tools and Algorithms for the Construction and
Analysis of Systems (TACAS 2022)
-
Action-Based Model Checking: Logic, Automata,
and Reduction
-
Stephen F. Siegel and Yihao Yan. In Computer Aided Verification:
32nd International Conference (CAV 2020)
-
Automated Verification of Scientific Software
-
Ziqing Luo, Wenhao Wu, Jan Hückelheim, Paul D. Hovland, and
Stephen F. Siegel. In Automated Software Verification 2019,
to appear.
-
What's wrong with on-the-fly partial
order reduction
-
Stephen F. Siegel. In Proceedings of the 31st
International Conference on Computer-Aided Verification
(CAV 2019)
- Towards Deductive Verification of
Message-Passing 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, Sriram Krishnamoorthy, Ignacio Laguna, Richard
A. Lethin, Koushik Sen, Stephen F. Siegel, Armando Solar-Lezama,
Report of the HPC Correctness Summit Jan 25-26, 2017,
Washington, DC
- Towards Self-Verification
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. 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