Travelled to:1 × Canada
1 × Germany
1 × Israel
1 × United Kingdom
2 × France
2 × USA
Collaborated with:∅ N.Narasimhan M.Aagaard R.B.Jones K.R.Kohatsu C.H.Seger R.Ghughal A.Telfer J.Whittemore S.Pandav A.Slobodová C.Taylor V.Frolov E.Reeber A.Naik
Talks about:formal (5) verif (5) processor (2) composit (2) pentium (2) execut (2) valid (2) intel (2) engin (2) core (2)
Person: Roope Kaivola
DBLP: Kaivola:Roope
Contributed to:
2011
20092005
2002
20001997
19961992Wrote 8 papers:
- PADL-2011-Kaivola #execution #framework #functional #validation
- Intel CoreTM i7 Processor Execution Engine Validation in a Functional Language Based Formal Framework (RK), p. 1.
- CAV-2009-KaivolaGNTWPSTFRN #execution #testing #validation #verification
- Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation (RK, RG, NN, AT, JW, SP, AS, CT, VF, ER, AN), pp. 414–429.
- CAV-2005-Kaivola #component #induction #invariant #simulation #verification
- Formal Verification of Pentium® 4 Components with Symbolic Simulation and Inductive Invariants (RK), pp. 170–184.
- DATE-2002-KaivolaN #float #multi #verification
- Formal Verification of the Pentium ® 4 Floating-Point Multiplier (RK, NN), pp. 20–27.
- DAC-2000-AagaardJKKS #algorithm #verification
- Formal verification of iterative algorithms in microprocessors (MA, RBJ, RK, KRK, CJHS), pp. 201–206.
- CAV-1997-Kaivola #composition #using #verification
- Using Compositional Preorders in the Verification of Sliding Window Protocal (RK), pp. 48–59.
- ICALP-1996-Kaivola #automaton #fixpoint
- Fixpoints for Rabin Tree Automata Make Complementation Easy (RK), pp. 312–323.
- CAV-1992-Kaivola #composition #linear #logic #model checking
- Compositional Model Checking for Linear-Time Temporal Logic (RK), pp. 248–259.