Roope Kaivola

Roope Kaivola: Intel Core^TM i7 Processor Execution Engine Validation in a Functional Language Based Formal Framework. PADL 2011: 1

Roope Kaivola, Rajnish Ghughal, Naren Narasimhan, Amber Telfer, Jesse Whittemore, Sudhindra Pandav, Anna Slobodová, Christopher Taylor, Vladimir Frolov, Erik Reeber, Armaghan Naik: Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation. CAV 2009: 414-429

T. Karvi, Tienari Tienari, Roope Kaivola: Stepwise Development of Process-Algebraic Specifications in Decorated Trace Semantics. Formal Methods in System Design 26(3): 293-317 (2005)

Roope Kaivola: Formal Verification of Pentium® 4 Components with Symbolic Simulation and Inductive Invariants. CAV 2005: 170-184

Roope Kaivola, Armaghan Naik: Formal verification of high-level conformance with symbolic simulation. HLDVT 2005: 153-159

Roope Kaivola, Katherine R. Kohatsu: Proof engineering in the large: formal verification of Pentium?4 floating-point divider. STTT 4(3): 323-334 (2003)

Roope Kaivola, Naren Narasimhan: Formal Verification of the Pentium ® 4 Floating-Point Multiplier. DATE 2002: 20-27

Roope Kaivola, Katherine R. Kohatsu: Proof Engineering in the Large: Formal Verification of Pentium^® 4 Floating-Point Divider. CHARME 2001: 196-211

Roope Kaivola, Naren Narasimhan: Formal verification of the Pentium^(R) 4 multiplier. HLDVT 2001: 115-120

Mark Aagaard, Robert B. Jones, Roope Kaivola, Katherine R. Kohatsu, Carl-Johan H. Seger: Formal verification of iterative algorithms in microprocessors. DAC 2000: 201-206

Roope Kaivola, Mark Aagaard: Divider Circuit Verification with Model Checking and Theorem Proving. TPHOLs 2000: 338-355

Roope Kaivola: Axiomatising Extended Computation Tree Logic. Theor. Comput. Sci. 190(1): 41-60 (1998)

Roope Kaivola: Using Compositional Preorders in the Verification of Sliding Window Protocal. CAV 1997: 48-59

Roope Kaivola: Axiomatising Extended Computation Tree Logic. CAAP 1996: 87-101

Roope Kaivola: Fixpoints for Rabin Tree Automata Make Complementation Easy. ICALP 1996: 312-323

Roope Kaivola: On Modal mu-Calculus and Büchi Tree Automata. Inf. Process. Lett. 54(1): 17-22 (1995)

Roope Kaivola: Axiomatising Linear Time Mu-calculus. CONCUR 1995: 423-437

Roope Kaivola: Compositional Model Checking for Linear-Time Temporal Logic. CAV 1992: 248-259

Roope Kaivola, Antti Valmari: The Weakest Compositional Semantic Equivalence Preserving Nexttime-less Linear temporal Logic. CONCUR 1992: 207-221

Roope Kaivola, Antti Valmari: Using Truth-Preserving Reductions to Improve the Clarity of Kripke-Models. CONCUR 1991: 361-375