| 2025 | CAV | Verifying PETSc Vector Components Using CIVL. | Venkata Dhavala, Jan Hckelheim, Paul D. Hovland, Stephen F. Siegel |
| 2024 | CAV | Collective Contracts for Message-Passing Parallel Programs. | Ziqing Luo, Stephen F. Siegel |
| 2023 | CAV | Model Checking Race-Freedom When "Sequential Consistency for Data-Race-Free Programs" is Guaranteed. | Wenhao Wu, Jan Hckelheim, Paul D. Hovland, Ziqing Luo, Stephen F. Siegel |
| 2022 | TACAS | Verifying Fortran Programs with CIVL. | Wenhao Wu, Jan Hckelheim, Paul D. Hovland, Stephen F. Siegel |
| 2020 | CAV | Action-Based Model Checking: Logic, Automata, and Reduction. | Stephen F. Siegel, Yihao Yan |
| 2019 | CAV | What's Wrong with On-the-Fly Partial Order Reduction. | Stephen F. Siegel |
| 2018 | ISoLA | Symbolic Execution and Deductive Verification Approaches to VerifyThis 2017 Challenges. | Ziqing Luo, Stephen F. Siegel |
| 2018 | ISoLA | Evaluating Tools for Software Verification (Track Introduction). | Markus Schordan, Dirk Beyer, Stephen F. Siegel |
| 2018 | SC | Towards Deductive Verification of Message-Passing Parallel Programs. | Ziqing Luo, Stephen F. Siegel |
| 2018 | SAS | Verifying Properties of Differentiable Programs. | Jan Hckelheim, Ziqing Luo, Sri Hari Krishna Narayanan, Stephen F. Siegel, Paul D. Hovland |
| 2017 | SC | Towards Self-Verification in Finite Difference Code Generation. | Jan Hckelheim, Ziqing Luo, Fabio Luporini, Navjot Kukreja, Michael Lange, Gerard Gorman, Stephen F. Siegel, Matthew B. Dwyer, Paul D. Hovland |
| 2016 | TACAS | 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, Stephen F. Siegel |
| 2015 | SC | 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 |
| 2012 | VMCAI | Loop Invariant Symbolic Execution for Parallel Programs. | Stephen F. Siegel, Timothy K. Zirkel |
| 2011 | PPoPP | Automatic formal verification of MPI-based parallel programs. | Stephen F. Siegel, Timothy K. Zirkel |
| 2011 | VMCAI | Formal Analysis of Message Passing - (Invited Talk). | Stephen F. Siegel, Ganesh Gopalakrishnan |
| 2011 | VMCAI | Collective Assertions. | Stephen F. Siegel, Timothy K. Zirkel |
| 2007 | VMCAI | Model Checking Nonblocking MPI Programs. | Stephen F. Siegel |
| 2006 | ISSTA | Using model checking with symbolic execution to verify parallel numerical programs. | Stephen F. Siegel, Anastasia Mironova, George S. Avrunin, Lori A. Clarke |
| 2005 | PPoPP | Modeling wildcard-free MPI programs for verification. | Stephen F. Siegel, George S. Avrunin |
| 2005 | VMCAI | Efficient Verification of Halting Properties for MPI Programs with Wildcard Receives. | Stephen F. Siegel |
| 2000 | ISSTA | Improving the precision of INCA by preventing spurious cycles. | Stephen F. Siegel, George S. Avrunin |