| 2005 |
|---|
| 16 | EE | Roope Kaivola:
Formal Verification of Pentium® 4 Components with Symbolic Simulation and Inductive Invariants.
CAV 2005: 170-184 |
| 15 | EE | 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) |
| 2003 |
|---|
| 14 | EE | Roope Kaivola,
Katherine R. Kohatsu:
Proof engineering in the large: formal verification of Pentium?4 floating-point divider.
STTT 4(3): 323-334 (2003) |
| 2002 |
|---|
| 13 | EE | Roope Kaivola,
Naren Narasimhan:
Formal Verification of the Pentium ® 4 Floating-Point Multiplier.
DATE 2002: 20-27 |
| 2001 |
|---|
| 12 | EE | Roope Kaivola,
Katherine R. Kohatsu:
Proof Engineering in the Large: Formal Verification of Pentium® 4 Floating-Point Divider.
CHARME 2001: 196-211 |
| 2000 |
|---|
| 11 | EE | 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 |
| 10 | | Roope Kaivola,
Mark Aagaard:
Divider Circuit Verification with Model Checking and Theorem Proving.
TPHOLs 2000: 338-355 |
| 1998 |
|---|
| 9 | EE | Roope Kaivola:
Axiomatising Extended Computation Tree Logic.
Theor. Comput. Sci. 190(1): 41-60 (1998) |
| 1997 |
|---|
| 8 | | Roope Kaivola:
Using Compositional Preorders in the Verification of Sliding Window Protocal.
CAV 1997: 48-59 |
| 1996 |
|---|
| 7 | | Roope Kaivola:
Axiomatising Extended Computation Tree Logic.
CAAP 1996: 87-101 |
| 6 | | Roope Kaivola:
Fixpoints for Rabin Tree Automata Make Complementation Easy.
ICALP 1996: 312-323 |
| 1995 |
|---|
| 5 | | Roope Kaivola:
Axiomatising Linear Time Mu-calculus.
CONCUR 1995: 423-437 |
| 4 | EE | Roope Kaivola:
On Modal mu-Calculus and Büchi Tree Automata.
Inf. Process. Lett. 54(1): 17-22 (1995) |
| 1992 |
|---|
| 3 | | Roope Kaivola:
Compositional Model Checking for Linear-Time Temporal Logic.
CAV 1992: 248-259 |
| 2 | | Roope Kaivola,
Antti Valmari:
The Weakest Compositional Semantic Equivalence Preserving Nexttime-less Linear temporal Logic.
CONCUR 1992: 207-221 |
| 1991 |
|---|
| 1 | | Roope Kaivola,
Antti Valmari:
Using Truth-Preserving Reductions to Improve the Clarity of Kripke-Models.
CONCUR 1991: 361-375 |
