Publications
Robert Jones
These papers are listed in reverse chronological order. Clicking on a
paper's citation will take you to the paper's "home page", where you
can view the abstract, the BibTeX entry, and/or download a copy of the
paper.
You may find it more useful to view these papers organized by topic or within the
context of my research.
Submitted/To Appear:
Publications:
-
[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).
-
[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.
- [Jon02]
Robert B. Jones.
Symbolic Simulation Methods for Industrial Formal
Verification.
Kluwer Academic Publishers, 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.
- [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.
- [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.
- [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.
-
[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.
- [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.
- [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.
- [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.
- [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.
- [GGJ91]
Extended subject access to hypertext online documentation. Parts I and
II: The search-support and maintenance problems.
Terry R. Girill, Thomas Griffen, and Robert B. Jones.
Journal of the American Society for Information Science (JASIS),
42(6):414-426, July 1991.
Robert Jones,
rjones @ ichips.intel.com
Last Modified: 10 January 2004