Roope Kaivola

	2009
17		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
	2005
16		Roope Kaivola: Formal Verification of Pentium® 4 Components with Symbolic Simulation and Inductive Invariants. CAV 2005: 170-184
15		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		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		Roope Kaivola, Naren Narasimhan: Formal Verification of the Pentium ® 4 Floating-Point Multiplier. DATE 2002: 20-27
	2001
12		Roope Kaivola, Katherine R. Kohatsu: Proof Engineering in the Large: Formal Verification of Pentium® 4 Floating-Point Divider. CHARME 2001: 196-211
	2000
11		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		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		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

Coauthor Index

1	Mark Aagaard	[10] [11]
2	Vladimir Frolov	[17]
3	Rajnish Ghughal	[17]
4	Robert B. Jones	[11]
5	T. Karvi	[15]
6	Katherine R. Kohatsu	[11] [12] [14]
7	Armaghan Naik	[17]
8	Naren Narasimhan	[13] [17]
9	Sudhindra Pandav	[17]
10	Erik Reeber	[17]
11	Carl-Johan H. Seger	[11]
12	Anna Slobodová	[17]
13	Christopher Taylor	[17]
14	Amber Telfer	[17]
15	Tienari Tienari	[15]
16	Antti Valmari	[1] [2]
17	Jesse Whittemore	[17]

Colors in the list of coauthors