| 2022 | FMCAD | Error Correction Code Algorithm and Implementation Verification Using Symbolic Representations. | Aarti Gupta, Roope Kaivola, Mihir Parang Mehta, Vaibhav Singh |
| 2022 | FMCAD | Timed Causal Fanin Analysis for Symbolic Circuit Simulation. | Roope Kaivola, Neta Bar Kama |
| 2021 | FMCAD | Hardware Security Leak Detection by Symbolic Simulation. | Neta Bar Kama, Roope Kaivola |
| 2013 | FMCAD | Relational STE and theorem proving for formal verification of industrial circuit designs. | John W. O'Leary, Roope Kaivola, Tom Melham |
| 2011 | PADL | Intel Core | Roope Kaivola |
| 2009 | CAV | Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation. | Roope Kaivola, Rajnish Ghughal, Naren Narasimhan, Amber Telfer, Jesse Whittemore, Sudhindra Pandav, Anna Slobodov, Christopher Taylor, Vladimir A. Frolov, Erik Reeber, Armaghan Naik |
| 2005 | CAV | Formal Verification of Pentium® 4 Components with Symbolic Simulation and Inductive Invariants. | Roope Kaivola |
| 2002 | DATE | Formal Verification of the Pentium 4 Floating-Point Multiplier. | Roope Kaivola, Naren Narasimhan |
| 2000 | DAC | Formal verification of iterative algorithms in microprocessors. | Mark D. Aagaard, Robert B. Jones, Roope Kaivola, Katherine R. Kohatsu, Carl-Johan H. Seger |
| 1997 | CAV | Using Compositional Preorders in the Verification of Sliding Window Protocal. | Roope Kaivola |
| 1996 | ICALP | Fixpoints for Rabin Tree Automata Make Complementation Easy. | Roope Kaivola |
| 1995 | CONCUR | Axiomatising Linear Time Mu-calculus. | Roope Kaivola |
| 1992 | CAV | Compositional Model Checking for Linear-Time Temporal Logic. | Roope Kaivola |
| 1992 | CONCUR | The Weakest Compositional Semantic Equivalence Preserving Nexttime-less Linear temporal Logic. | Roope Kaivola, Antti Valmari |
| 1991 | CONCUR | Using Truth-Preserving Reductions to Improve the Clarity of Kripke-Models. | Roope Kaivola, Antti Valmari |