Publications by Topic

I have divided my publications into the following general topics:

• industrial applications of formal verification
• applications of symbolic simulation
• pipelined processor verification
• combined model checking and theorem proving
• automated deduction
• simulation-based verification

You may also view a list of my papers in reverse chronological order.

Industrial Applications of Formal Verification

• [Jon02] Robert B. Jones. Symbolic Simulation Methods for Industrial Formal Verification. Kluwer Academic Publishers, 2002.

• [JOS+01] Practical formal verification in microprocessor design. Robert B. Jones, John W. O'Leary, Carl-Johan H. Seger, Mark D. Aagaard, and Thomas F. Melham. IEEE Design and Test, 18(4):18-25, July/August 2001.

• [AJM+00] A methodology for large-scale hardware verification. Mark D. Aagaard, Robert B. Jones, Thomas F. Melham, John W. O'Leary, and Carl-Johan H. Seger. In Warren A. Hunt Jr. and Steven D. Johnson, editors, Formal Methods in Computer-Aided Design (FMCAD), volume 1954 of Lecture Notes in Computer Science, pages 263-282. Springer-Verlag, November 2000.

• [AJK+00] Formal verification of iterative algorithms in microprocessors. Mark D. Aagaard, Robert B. Jones, Roope Kaivola, Katherine R. Kohatsu, and Carl-Johan H. Seger. In Design Automation Conference (DAC), pages 201-206. ACM Press, June 2000.

Applications of Symbolic Simulation

• [MJ02] Abstraction by symbolic indexing transformations. Tom Melham and Robert B. Jones. In Mark D. Aagaard and John W. O'Leary, editors, Formal Methods in Computer-Aided Design (FMCAD), volume 2517 of Lecture Notes in Computer Science, pages 1-18. Springer-Verlag, November 2002.

• [Jon99] Applications of Symbolic Simulation to the Formal Verification of Microprocessors. Robert B. Jones. PhD thesis, Computer Systems Laboratory, Stanford University, August 1999.

• [AJS99] Formal verification using parametric representations of Boolean constraints. Mark D. Aagaard, Robert B. Jones, and Carl-Johan H. Seger. In Design Automation Conference (DAC), pages 402-407. ACM Press, June 1999.

• [JSD96] Self consistency checking. Robert B. Jones, Carl-Johan H. Seger, and David L. Dill. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer-Aided Design (FMCAD), volume 1166 of Lecture Notes in Computer Science, pages 159-171. Springer-Verlag, November 1996.

Pipelined Processor Verification

• [ACDJ03] A framework for superscalar microprocessor correctness statements. Mark D. Aagaard, Byron Cook, Nancy A. Day, and Robert B. Jones. Software Tools for Technology Transfer, 4(3):298-312, 2003. (on-line publication was in 2002).

• [JSD02] Formal verification of out-of-order execution with incremental flushing. Robert B. Jones, Jens U. Skakkebæk, and David L. Dill. Formal Methods in System Design, Special Issue on Microprocessor Verification, 20(2):139-158, March 2002.

• [ACDJ01] A framework for microprocessor correctness statements. Mark D. Aagaard, Byron Cook, Nancy A. Day, and Robert B. Jones. In Tiziana Margaria and Tom Melham, editors, Correct Hardware Design and Verification Methods ({CHARME} '01), volume 2144 of Lecture Notes in Computer Science, pages 433-448. Springer-Verlag, September 2001.

• [JSD98] Reducing manual abstraction in formal verification of out-of-order execution. Robert B. Jones, Jens U. Skakkebæk, and David L. Dill. In Ganesh Gopalakrishnan and Phillip Windley, editors, Formal Methods in Computer-Aided Design (FMCAD), volume 1522 of Lecture Notes in Computer Science, pages 2-17. Springer-Verlag, November 1998.

• [SJD98] Formal verification of out-of-order execution using incremental flushing. Jens U. Skakkebæk, Robert B. Jones, and David L. Dill. In Alan J. Hu and Moshe Y. Vardi, editors, Computer-Aided Verification (CAV), volume 1427 of Lecture Notes in Computer Science, pages 98-109. Springer-Verlag, June-July 1998.

Combined Model Checking and Theorem Proving

• [AJS99] Lifted-fl: A pragmatic implementation of combined model checking and theorem proving. Mark D. Aagaard, Robert B. Jones, and Carl-Johan H. Seger. In Theorem Proving in Higher-Order Logics. Springer-Verlag, September 1999.

• [AJS98] Combining theorem proving and trajectory evaluation in an industrial environment. Mark D. Aagaard, Robert B. Jones, and Carl-Johan H. Seger. In Design Automation Conference (DAC), pages 538-541. ACM Press, June 1998.

Automated Deduction

• [JDB95] Efficient validity checking for processor verification. Robert B. Jones, David L. Dill, and Jerry R. Burch. In International Conference on Computer-Aided Design (ICCAD), pages 2-6. IEEE Computer Society Press, November 1995.

Simulation-Based Verification

• [NJK94] Simulation event pattern checking with proto. Brent E. Nelson, Robert B. Jones, and Desmond A. Kirkpatrick. In Conference on Simulation and Hardware Description Languages (SHDL), January 1994.