VSL | Publications

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'19)
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, Ganesh Gopalakrishnan, 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