Roope Kaivola

According to our database, Roope Kaivola authored at least 24 papers between 1991 and 2022.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2022

Timed Causal Fanin Analysis for Symbolic Circuit Simulation.

Roope Kaivola, Neta Bar Kama

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

Error Correction Code Algorithm and Implementation Verification Using Symbolic Representations.

Aarti Gupta, Roope Kaivola, Mihir Parang Mehta, Vaibhav Singh

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

2021

Hardware Security Leak Detection by Symbolic Simulation.

Neta Bar Kama, Roope Kaivola

Proceedings of the Formal Methods in Computer Aided Design, 2021

2013

Relational STE and theorem proving for formal verification of industrial circuit designs.

John W. O'Leary, Roope Kaivola, Tom Melham

Proceedings of the Formal Methods in Computer-Aided Design, 2013

2011

Intel Core^TM i7 Processor Execution Engine Validation in a Functional Language Based Formal Framework.

Roope Kaivola

Proceedings of the Practical Aspects of Declarative Languages, 2011

2009

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

Proceedings of the Computer Aided Verification, 21st International Conference, 2009

2005

Stepwise Development of Process-Algebraic Specifications in Decorated Trace Semantics.

T. Karvi, Tienari Tienari, Roope Kaivola

Formal Methods Syst. Des., 2005

Formal verification of high-level conformance with symbolic simulation.

Roope Kaivola, Armaghan Naik

Proceedings of the Tenth IEEE International High-Level Design Validation and Test Workshop 2005, Napa Valley, CA, USA, November 30, 2005

Formal Verification of Pentium® 4 Components with Symbolic Simulation and Inductive Invariants.

Roope Kaivola

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

2003

Proof engineering in the large: formal verification of Pentium?4 floating-point divider.

Roope Kaivola, Katherine R. Kohatsu

Int. J. Softw. Tools Technol. Transf., 2003

2002

Formal Verification of the Pentium ® 4 Floating-Point Multiplier.

Roope Kaivola, Naren Narasimhan

Proceedings of the 2002 Design, 2002

2001

Formal verification of the Pentium^(R) 4 multiplier.

Roope Kaivola, Naren Narasimhan

Proceedings of the Sixth IEEE International High-Level Design Validation and Test Workshop 2001, 2001

Proof Engineering in the Large: Formal Verification of Pentium^® 4 Floating-Point Divider.

Roope Kaivola, Katherine R. Kohatsu

Proceedings of the Correct Hardware Design and Verification Methods, 2001

2000

Divider Circuit Verification with Model Checking and Theorem Proving.

Roope Kaivola, Mark D. Aagaard

Proceedings of the Theorem Proving in Higher Order Logics, 13th International Conference, 2000

Formal verification of iterative algorithms in microprocessors.

Mark D. Aagaard, Robert B. Jones, Roope Kaivola, Katherine R. Kohatsu, Carl-Johan H. Seger

Proceedings of the 37th Conference on Design Automation, 2000

1998

Axiomatising Extended Computation Tree Logic.

Roope Kaivola

Theor. Comput. Sci., 1998

1997

Using Compositional Preorders in the Verification of Sliding Window Protocal.

Roope Kaivola

Proceedings of the Computer Aided Verification, 9th International Conference, 1997

1996

Fixpoints for Rabin Tree Automata Make Complementation Easy.

Roope Kaivola

Proceedings of the Automata, Languages and Programming, 23rd International Colloquium, 1996

1995

On Modal mu-Calculus and Büchi Tree Automata.

Roope Kaivola

Inf. Process. Lett., 1995

A Simple Decision Method for the Linear Time Mu-calculus.

Roope Kaivola

Proceedings of the International Workshop on Structures in Concurrency Theory, 1995

Axiomatising Linear Time Mu-calculus.

Roope Kaivola

Proceedings of the CONCUR '95: Concurrency Theory, 1995

1992

The Weakest Compositional Semantic Equivalence Preserving Nexttime-less Linear temporal Logic.

Roope Kaivola, Antti Valmari

Proceedings of the CONCUR '92, 1992

Compositional Model Checking for Linear-Time Temporal Logic.

Roope Kaivola

Proceedings of the Computer Aided Verification, Fourth International Workshop, 1992

1991

Using Truth-Preserving Reductions to Improve the Clarity of Kripke-Models.

Roope Kaivola, Antti Valmari

Proceedings of the CONCUR '91, 1991