Roope Kaivola

27 papers A* 6A 1B 8C 1Journal 5Unranked 6
YearRankTypeTitle / Venue / Authors
2025 J jnl
Timed causal fanin analysis for symbolic simulation.
Formal Methods Syst. Des.
Roope Kaivola, Neta Bar Kama
2022 B conf
Error Correction Code Algorithm and Implementation Verification Using Symbolic Representations.
FMCAD
Aarti Gupta, Roope Kaivola, Mihir Parang Mehta, Vaibhav Singh
2022 B conf
Timed Causal Fanin Analysis for Symbolic Circuit Simulation.
FMCAD
Roope Kaivola, Neta Bar Kama
2021 B conf
Hardware Security Leak Detection by Symbolic Simulation.
FMCAD
Neta Bar Kama, Roope Kaivola
2015 B ed.
Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, September 27-30, 2015.
FMCAD
Roope Kaivola, Thomas Wahl
2013 B conf
Relational STE and theorem proving for formal verification of industrial circuit designs.
FMCAD
John W. O'Leary, Roope Kaivola, Tom Melham
2011 C conf
Intel Core
PADL
Roope Kaivola
2009 A* conf
Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation.
CAV
Roope Kaivola, Rajnish Ghughal, Naren Narasimhan, Amber Telfer, Jesse Whittemore, Sudhindra Pandav, Anna Slobodová, Christopher Taylor, Vladimir A. Frolov, Erik Reeber, Armaghan Naik
2005 A* conf
Formal Verification of Pentium® 4 Components with Symbolic Simulation and Inductive Invariants.
CAV
Roope Kaivola
2005 — conf
Formal verification of high-level conformance with symbolic simulation.
HLDVT
Roope Kaivola, Armaghan Naik
2005 J jnl
Stepwise Development of Process-Algebraic Specifications in Decorated Trace Semantics.
Formal Methods Syst. Des.
T. Karvi, Tienari Tienari, Roope Kaivola
2003 J jnl
Proof engineering in the large: formal verification of Pentium?4 floating-point divider.
Int. J. Softw. Tools Technol. Transf.
Roope Kaivola, Katherine R. Kohatsu
2002 A conf
Formal Verification of the Pentium ® 4 Floating-Point Multiplier.
DATE
Roope Kaivola, Naren Narasimhan
2001 — conf
Formal verification of the Pentium
HLDVT
Roope Kaivola, Naren Narasimhan
2001 — conf
Proof Engineering in the Large: Formal Verification of Pentium
CHARME
Roope Kaivola, Katherine R. Kohatsu
2000 — conf
Divider Circuit Verification with Model Checking and Theorem Proving.
TPHOLs
Roope Kaivola, Mark D. Aagaard
2000 A* conf
Formal verification of iterative algorithms in microprocessors.
DAC
Mark D. Aagaard, Robert B. Jones, Roope Kaivola, Katherine R. Kohatsu, Carl-Johan H. Seger
1998 J jnl
Axiomatising Extended Computation Tree Logic.
Theor. Comput. Sci.
Roope Kaivola
1997 A* conf
Using Compositional Preorders in the Verification of Sliding Window Protocal.
CAV
Roope Kaivola
1996 — conf
Axiomatising Extended Computation Tree Logic.
CAAP
Roope Kaivola
1996 A* conf
Fixpoints for Rabin Tree Automata Make Complementation Easy.
ICALP
Roope Kaivola
1995 — conf
A Simple Decision Method for the Linear Time Mu-calculus.
STRICT
Roope Kaivola
1995 B conf
Axiomatising Linear Time Mu-calculus.
CONCUR
Roope Kaivola
1995 J jnl
On Modal mu-Calculus and Büchi Tree Automata.
Inf. Process. Lett.
Roope Kaivola
1992 A* conf
Compositional Model Checking for Linear-Time Temporal Logic.
CAV
Roope Kaivola
1992 B conf
The Weakest Compositional Semantic Equivalence Preserving Nexttime-less Linear temporal Logic.
CONCUR
Roope Kaivola, Antti Valmari
1991 B conf
Using Truth-Preserving Reductions to Improve the Clarity of Kripke-Models.
CONCUR
Roope Kaivola, Antti Valmari