Roope Kaivola

Publication Activity (10 Years)

Years Active: 1991-2022
Publications (10 Years): 3

Top Topics

Symbolic Representation

Distributed Search

Theorem Proving

Top Venues

Publications

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