W. R. Bevier, Kit: A Study in Operating System Verification,IEEE Transactions on Software Engineering, November, 1989.
An Approach to Systems Verification, W. R. Bevier, W. A. Hunt, J S. Moore and W. D. Young, Journal of Automated Reasoning, November, 1989. Also appears as CLI Technical Report 41.
W. R. Bevier, Kit and the Short Stack, Journal of Automated Reasoning, November, 1989.
Toward Verified Execution Environments, W. R. Bevier, W. A. Hunt and W. D. Young, Proc. IEEE Symposium on Security and Privacy, April, 1987. Reprinted in Rein Turn (editor), Advances in Computer System Security, Volume III, Artech House, Inc., 1988. Also appears as CLI Technical Report 5.
The Boyer-Moore Theorem Prover and Its Interactive Enhancement, R. S. Boyer, M. Kaufmann and J S. Moore, Computers and Mathematics with Applications, Vol 29, No. 2, pp. 27-62, 1995.
Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor, R. S. Boyer, Yuan Yu, in D. Kapur, editor, Automated Deduction -- CADE-11, Lecture Notes in Computer Science 607, Springer-Verlag, 1992, pp. 416-430.
A Biographical Sketch of W. W. Bledsoe, R. S. Boyer, Anne Boyer, in Robert S. Boyer, editor, Automated Reasoning: Essays in Honor of Woody Bledsoe. Kluwer Academic, Dordrecht, The Netherlands, 1991, pp. 1-29.
MJRTY - A Fast Majority Vote Algorithm, R. S. Boyer, J S. Moore, in Robert S. Boyer, editor, Automated Reasoning: Essays in Honor of Woody Bledsoe. Kluwer Academic, Dordrecht, The Netherlands, 1991, pp. 105-117.
Functional Instantiation in First Order Logic, R. S. Boyer, D. Goldschlag, M. Kaufmann, and J Moore, in V. Lifschitz (editor), Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy. Academic Press, 1991, pp. 7-26.
A Theorem Prover for a Computational Logic, R. S. Boyer, J S. Moore, keynote address, Automated Deduction -- CADE-10, Lecture Notes in Computer Science 449, Springer-Verlag, 1990, pp. 1-15.
The Use of a Formal Simulator to Verify a Simple Real Time Control Program, R. S. Boyer, M. W. Green and J S. Moore. in W. H. J. Feijen, A. J. M. van Gasteren, D. Gries, and J. Misra, editors, Beauty is Our Business, Springer-Verlag, 1990, pp. 54-66.
The Efficient Implementation of Lattice Operations, R. S. Boyer, H. Ait-Kaci, P. Lincoln, and R. Nasr. Association for Computing Machinery Transactions on Programming Languages and Systems, Vol. 11, No. 1, pp. 115-146, January 1988.
The Addition of Bounded Quantification and Partial Functions to a Computational Logic and Its Theorem Prover, R. S. Boyer, J S. Moore, Journal of Automated Reasoning, Volume 4, pp. 117-172, 1988.
Integrating Decision Procedures into Heuristic Theorem Provers: A Case Study of Linear Arithmetic, R. S. Boyer, J S. Moore. Machine Intelligence 11, Oxford University Press, 1988, pp. 83-124.
Set Theory in First Order Logic: Clauses for Goedel's Axioms, R. S. Boyer, E. Lusk, W. McCune, R. Overbeek, M. Stickel, and L. Wos, Journal of Automated Reasoning, Vol. 2, No. 3., pp. 287-327, 1986.
Program Verification, R. S. Boyer, J S. Moore. Automated Reasoning, Vol. 1, No. 1, 1985, pp. 17-23.
A Mechanical Proof of the Turing Completeness of PURE LISP, R. S. Boyer, J S. Moore. In W. W. Bledsoe and D. W. Loveland, editors, Contemporary Mathematics, Volume 29, Automated Theorem Proving: After 25 Years, American Mathematical Society, Providence, Rhode Island, 1984, pp. 132-168.
Proof-Checking, Theorem-Proving, and Program Verification, R. S. Boyer, J S. Moore. In W. W. Bledsoe and D. W. Loveland, editors, Contemporary Mathematics, Volume 29, Automated Theorem Proving: After 25 Years, American Mathematical Society, Providence, Rhode Island, 1984, pp. 119-132.
Proof Checking the RSA Public Key Encryption Algorithm, R. S. Boyer, J S. Moore. American Mathematical Monthly, Vol. 91, No. 3, March 1984, pp. 181-189.
A Mechanical Proof of the Unsolvability of the Halting Problem, R. S. Boyer, J S. Moore. Journal of the Association for Computing Machinery, Vol. 31, No. 3, July 1984, pp.441-458.
A Verification Condition Generator for FORTRAN, R. S. Boyer, J S. Moore. In R. S. Boyer and J S. Moore, editors, The Correctness Problem in Computer Science, Academic Press, London, 1981, pp. 9-101.
Metafunctions: Proving Them Correct and Using Them Efficiently as New Proof Procedures, R. S. Boyer, J S. Moore. In R. S. Boyer and J S. Moore, editors, The Correctness Problem in Computer Science, Academic Press, London, 1981, pp. 103-184.
A Lemma Driven Automatic Theorem Prover for Recursive Function Theory, R. S. Boyer, J S. Moore. Proceedings of the 5th International Joint Conference on Artificial Intelligence, pp. 511-519, 1977.
A Fast String Searching Algorithm, R. S. Boyer, J S. Moore. Communications of the Association for Computing Machinery, Vol. 20, No. 10, pp. 762-772, 1977.
Proving Theorems about LISP Functions, R. S. Boyer, J S. Moore. Journal of the Association for Computing Machinery, Vol. 22, No. 1, pp. 129-144, 1975.
The Sharing of Structure in Theorem-proving Programs, R. S. Boyer, J S. Moore. In B. Meltzer and D. Michie, editors, Machine Intelligence, Vol. 7, pp. 101-116, Edinburgh University Press, 1972.
Computer Proofs of Limit Theorems, R. S. Boyer, W. W. Bledsoe and W. H. Henneman, Artificial Intelligence, Vol. 3, No. 1, pp. 27-60, 1972.
R. S. Boyer, The preface to Machine Proofs in Geometry: Automated Production of Readable Proofs for Geometry Theorems, Shang-Ching Chou, Xiao-Shan Gao, and Jing-Zhong Zhang, World Scientific, 1994, pp. vii-viii. R. S. Boyer, Response, biographical sketch, and photo on the occasion of receipt of the 1991 AMS Current Award for Automatic Theorem Proving, Notices of the American Mathematical Society, vol. 38, no. 5, pp. 407-408.
A Theorem-Prover for Recursive Functions, R. S. Boyer, J S. Moore. Software Engineering Notes, Association for Computing Machinery, Vol. 5, No. 3, pp. 26-27, 1980.
The FORTRAN Verification System, R. S. Boyer, J S. Moore. Software Engineering Notes, Association for Computing Machinery, Vol. 5, No. 3, pp. 16-17, 1980.
(D. I. Good, R.L. London, W.W. Bledsoe) An Interactive Program Verification System, IEEE Transactions on Software Engineering, Vol. 1, No. 1, March 1975.
(D. I. Good, L.C. Ragland) Certification of Algorithm 386(AI), Greatest Common Division of Integers and Multipliers, Communications of the ACM, Vol. 16, No. 4, April, 1973.
(D. I. Good, R.L. London) Computer Interval Arithmetic: Definition and Proof of Correct Implication. Journal of the ACM, Vol. 17, No. 4, October, 1970.
(D. I. Good, A.R. Tripathi, W. D. Young, J.C. Browne) HAL/S/V: A Verifiable Subset of HAL/S, in Sigplan Notices, March, 1981.
(D. I. Good, W. D. Young) Steelman and the Verifiability of (Preliminary) Ada, In Sigplan Notices, February, 1981.
(D. I. Good, W. D. Young, A.R. Tripathi, J.C. Browne) Design of a Verifiable Subset for HAL/S, [Technical Note] In Journal of Guidance and Control, January, 1981.
(D. I. Good, D.R. Musser, R.T. Yeh) New Directions in Teaching in the Fundamentals of Computer Science - Discrete Structures and Computational Analysis, SIGSCE Bulletin, Vol. 5, ACM, February 1973.
(D. I. Good, L.C. Ragland) Nucleus - A Language of Provable Programs, In Program Test Methods, Prentice Hall, 1972.
D. I. Good, Constructing Verified and Reliable Communications Processing Systems, ACM Software Engineering Notes, October, 1977.
Introduction to a Formally Defined Hardware Description Language, W. H. Hunt, Bishop C. Brock and W. D. Young, Theorem Provers in Circuit Design, IFIP, North-Holland, 1992.
The Formalization of an HDL and its use in the FM8502 Microprocessor Fabrication, W. H. Hunt, Bishop C. Brock, Philosophical Transactions of the Royal Society, Volume 339, 1992.
Report on the Formal Specification and Partial Verification of the VIPER Microprocessor, W. H. Hunt, Bishop C. Brock, COMPASS 1991 Proceedings, IEEE, 1991.
An Introduction to a Simple HDL, W. H. Hunt, Bishop C. Brock, Formal Methods for VLSI Design, Elsevier Science Publishers, 1990.
The Verification of a Bit-Slice ALU, W. H. Hunt, Bishop C. Brock, Workshop on Hardware Specification, Verification and Synthesis: Mathematical Aspects, Lecture Notes in Computer Science, Volume 408, Springer Verlag, 1989.
W. H. Hunt, Microprocessor Design Verification, Journal of Automated Reasoning, Volume 5, 1989.
An Approach to Systems Verification, W. H. Hunt, William R. Bevier, J Strother Moore, and W. D. Young, Journal of Automated Reasoning, Volume 5, 1989.
The Boyer-Moore Theorem Prover and Its Interactive Enhancement (M. Kaufmann, Robert S. Boyer and J Strother Moore), Computers and Mathematics with Applications, Vol. 29, No. 2, pp. 27-62, 1995.
M. Kaufmann, An Extension of the Boyer-Moore Theorem Prover to Support First-Order Quantification, Journal of Automated Reasoning, Vol. 9, No. 3., December 1992, pp. 355-372.
Functional Instantiation in First Order Logic (M. Kaufmann, Robert S. Boyer, David M. Goldschlag, and J Strother Moore), in: Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, Academic Press, 1991, pp. 7 - 26.
M. Kaufmann, Generalization in the Presence of Free Variables: a Mechanically-Checked Correctness Proof for One Algorithm. Journal of Automated Reasoning 7(1991), pp. 109-158.
Remarks on Weak Notions of Saturation in Models of Peano Arithmetic (M. Kaufmann, J. Schmerl). Journal Symbolic Logic, 52 (1987), pp. 129-148.
The Hanf Number of Stationary Logic (M. Kaufmann, S. Shelah). Notre Dame J. Formal Logic, 27 (1986), pp. 111-123.
M. Kaufmann, A Note on the Hanf Number of Second-Order Logic. Notre Dame J. Formal Logic, 26 (1985), 305-308.
M. Kaufmann, The Quantifier There Exist Uncountably Many and Some of Its Relatives. In Model-Theoretic Logics, (J. Barwise and S. Feferman, editors). Springer-Verlag, 1985, pp. 123-176.
On Random Models of Finite Power and Monadic Logic (M. Kaufmann, S. Shelah). Discrete Mathematics, 54 (1985), pp. 285-293.
M. Kaufmann, On Expandability of Models of Arithmetic and Set Theory to Models of Weak Second-Order Theories. Fund. Math., CXXII (1984), pp. 57-60.
M. Kaufmann, Some Remarks on Equivalence in Infinitary and Stationary Logic. Notre Dame J. Formal Logic, 25 (1984), pp. 383-389.
Saturation and Simple Extensions of Models of Peano Arithmetic (M. Kaufmann, J. Schmerl) Ann. Pure and Applied Logic, 27 (1984), pp.109-136.
The Strength of Nonstandard Methods in Arithmetic (M. Kaufmann, C.W. Henson and H.J. Keisler). J. Symbolic Logic, 49 (1984), pp. 1039-1058.
A Nonconservativity Result on Global Choice (M. Kaufmann, S. Shelah). Ann. Pure and Applied Logic, 27 (1984), pp. 209-214.
M. Kaufmann, Mutually Generic Classes and Incompatible Expansions. Fund. Math., CXXI (1984), pp. 213-218.
Definable Ultrapowers and Ultrafilters over Admissible Ordinals (M. Kaufmann, E. Kranakis). Zeitschr.f. Math. Logik und Grund., d. Math. 30 (1984), pp.97-118.
M. Kaufmann, Filter Logics on W. J. Symbolic Logic, 49 (1984), pp. 241-256.
M. Kaufmann, Blunt and Topless End Extensions of Models of Set Theory. J Symbolic Logic, 48 (1983), pp. 1053-1071.
M. Kaufmann, Set Theory with a Filter Quantifier. J. of Symbolic Logic, 48 (1983), pp. 263-287.
SUM-1-Well-founded Compactness (M. Kaufmann, N. Cutland). Ann. Math Logic, 18 (1980), pp. 271-296.
M. Kaufmann, Filter logics: Filters on W-1. Ann. Math. Logic, 20 (1980), pp. 155-200.
M. Kaufmann, A New Omitting Types Theorem for L(Q). J. Symbolic Logic, 44 (1979), pp. 217-231.
Stationary Logic (M. Kaufmann, J. Barwise and M. Makkai). Ann. Math. Logic, 13 (1978), pp. 171-224.
A Correction to Stationary Logic (M. Kaufmann, J. Barwise and M. Makkai). Ann. Math. Logic, 20 (1981), pp. 231-232.
M. Kaufmann, A Rather Classless Model. Proceedings Amer. Math. Soc., 62 (1977), pp. 330-333.
Smith, M. K., Siebert, A., DiVito, B. and Good, D. A verified encrypted packet interface, Software Engineering Notes, Volume 6, Number 3, July 1981.
Good, D. and Smith, M. K. A verified distributed system, Software Engineering Notes, Volume 5, Number 3, July 1980.
J S. Moore, A Formal Model of Asynchronous Communication and Its Use in Mechanically Verifying a Biphase Mark Protocol. In
Formal Aspects of Computing, Vol 6, #1, 1994, pp. 60-91.
J S. Moore, Introduction to the OBDD Algorithm for the ATP Community. In
Journal of Automated Reasoning, Kluwer Academic Publishers, Vol 6, #1, 1994, pp. 33-45.
Functional Instantiation in First Order Logic, J S. Moore, R.S. Boyer, D.M. Goldschlag, and M. Kaufmann. In V. Lifschitz, editor,
Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, Academic Press, 1991, pp. 7-26.
MJRTY - A Fast Majority Vote Algorithm, J S. Moore, R.S. Boyer. In R.S. Boyer, editor,
Automated Reasoning: Essays in Honor of Woody Bledsoe, Automated Reasoning Series, Kluwer Academic Publishers, Dordrecht, The Netherlands, 1991, pp. 105-117.
The Use of a Formal Simulator to Verify a Simple Real Time Control Program,
J S. Moore, R.S. Boyer and M.W. Green, in W.H.J. Feijen, A.J.M. van Gasteren, D.
Gries, and J. Misra editors, Beauty is Our Business: A Birthday Salute to
Edsger W. Dijkstra
Special Issue on System Verification, J S. Moore, W.R. Bevier, W. A. Hunt, and W.D. Young. Journal of Automated Reasoning, Kluwer Academic Publishers, Vol 5, #4, 1989, pp. 461-492.
J S. Moore, A Mechanically Verified Language Implementation. In Journal of Automated Reasoning, Kluwer Academic Publishers, Vol 5, #4, 1989, pp. 461-492.
The Addition of Bounded Quantification and Partial Functions to A Computational Logic and Its Theorem Prover, J S. Moore, R. S. Boyer. In Journal of Automated Reasoning, Kluwer Academic Publishers, Vol 4, #2, 1988, pp. 117-172.
Integrating Decision Procedures into Heuristic Theorem Provers: A Case Study of Linear Arithmetic, J S. Moore, R.S. Boyer. In Machine Intelligence, Oxford University Press (1988)
Program Verification, J S. Moore, R.S. Boyer. Automated Reasoning, Vol. 1, #1, 1985, pp. 17-23.
A Mechanical Proof of the Turing Completeness of PURE LISP, J S. Moore, R. S. Boyer. In W. W. Bledsoe and D. W. Loveland, editors, Contemporary Mathematics, Volume 29, Automated Theorem Proving: After 25 Years, American Mathematical Society, Providence, Rhode Island, 1984, pp. 133-168.
Proof-Checking, Theorem-Proving, and Program Verification, J S. Moore, R. S. Boyer. In W. W. Bledsoe and D. W. Loveland, editors, Contemporary Mathematics, Volume 29, Automated Theorem Proving: After 25 Years, American Mathematical Society, Providence, Rhode Island, 1984, pp. 119-132.
A Mechanical Proof of the Unsolvability of the Halting Problem, J S. Moore, R. S. Boyer. Journal of the Association for Computing Machinery, Vol. 31, No. 3, July 1984, pp. 441-458.
Proof Checking the RSA Public Key Encryption Algorithm, J S. Moore, R. S. Boyer. American Mathematical Monthly, Vol. 91, No. 3, March 1984, pp. 181-189.
A Verification Condition Generator for FORTRAN, J S. Moore, R.S. Boyer. In R.S. Boyer and J S. Moore, editors, The Correctness Problem in Computer Science, Academic Press, London, 1981.
Metafunctions: Proving Them Correct and Using Them Efficiently as New Proof Procedures, J S. Moore, R.S. Boyer. In R.S. Boyer and J S. Moore, editors, The Correctness Problem in Computer Science, Academic Press, London, 1981.
J S. Moore, A Mechanical Proof of the Termination of Takeuchi's Function. Information Processing Letters, Vol. 9, No. 4, pp. 176-181, 1979.
A Fast String Searching Algorithm, J S. Moore, R.S. Boyer. Communications of the Association for Computing Machinery, Vol. 20, No. 10, pp. 762-772, 1977.
J S. Moore, Introducing Iteration into the Pure LISP Theorem-Prover. IEEE Transactions on Software Engineering, Vol. SE-1, No. 3, pp. 328-338, 1975.
Proving Theorems about LISP Functions, J S. Moore, R.S. Boyer. Journal of the Association for Computing Machinery, Vol. 22, No. 1, pp.129-144, 1975.
The Sharing of Structure in Theorem-proving Programs, J S. Moore, R.S. Boyer. In B. Meltzer and D. Michie, editors, Machine Intelligence, Vol. 7, pp. 101-116, Edinburgh University Press, 1972.
Program Verification: An Approach to Reliable Hardware and Software, J S. Moore, L. Lamport. Transactions of the American Nuclear Society, American Nuclear Society, Vol. 35, pp 252-253, November, 1980.
A Theorem-Prover for Recursive Functions, J S. Moore, R.S. Boyer. Software Engineering Notes, Association for Computing Machinery, Vol. 5, No. 3, pp. 26-27, 1980.
The FORTRAN Verification System, J S. Moore, R.S. Boyer. Software Engineering Notes, Association for Computing Machinery, Vol. 5, No. 3, pp. 16-17, 1980.
J S. Moore, A Statement of Position. Software Engineering Notes, Association for Computing Machinery, Vol. 5, No. 3, pp 23-24, 1980.
J S. Moore, Automatic Proof of the Correctness of a Binary Addition Algorithm. SIGART Newsletter, Association for Computing Machinery, No. 52, pp. 13-14, 1975.
W. D. Young. Verifying a Simple Real-Time System with Nqthm, CLI technical report 93, September, 1993. Also to appear in Michael Hinchey and Jonathan Bowen, editors, Applications of Formal Methods, Prentice-Hall Series in Computer Science, 1995.
W. D. Young. System Verification and the CLI Stack, to appear in Jonathan Peter Bowen, editor, Towards Verified Systems, Elsevier Science Publishers Series on Real-Time Safety Critical Systems: Amsterdam, 1993.
Mathematical Methods for Digital Systems Development, W. D. Young, Donald I. Good, in VDM'91 Formal Software Development Methods, S. Prehn, W.J. Toetenel, editors, Springer-Verlag Lecture Notes in Computer Science 552, pp. 406-430, 1991. Also appears as CLI technical report 67, August, 1991.
Machine Checked Proofs of the Design of a Fault-Tolerant Circuit, W. D. Young, William R. Bevier, to appear in Formal Aspects of Computing. Also appears as CLI technical report 62, Computational Logic, Inc., August, 1990.
The Design and Proof of Correctness of a Fault-Tolerant Circuit, W. D. Young, William R. Bevier, in Dependable Computing for Critical Applications, J.F. Meyer and R.D. Schlichting, editors, Springer-Verlag, Vienna, 1991, pp. 243-260. Also appears as CLI technical report 57, August, 1990.
An Approach to Systems Verification, W. D. Young, W.R. Bevier, W. A. Hunt, and J S. Moore, Journal of Automated Reasoning , Vol. 5, Number 4, (December, 1989), pp. 411-428. Also available from Computational Logic as CLI technical report 41.
W. D. Young, A Mechanically Verified Code Generator, Journal of Automated Reasoning, Vol. 5, Number 4, (December, 1989), pp. 493-518. Also available from Computational Logic as CLI technical report 37.
Toward Verified Execution Environments, W. D. Young, W.R. Bevier and W.A. Hunt, Proc. IEEE Symposium on Security and Privacy, April, 1987. Reprinted in Rein Turn (editor), Advances in Computer System Security, Volume III, Artech House, Inc., 1988. Also available from Computational Logic as CLI technical report 5.
Experience using Two Covert Channel Analysis Techniques on a Real System Design, W. D. Young, J.T. Haigh, J. McHugh and R.A. Kemmerer, Proc. IEEE Symposium on Security and Privacy, April, 1986, pp. 14-24. Reprinted in IEEE Transactions on Software Engineering, January, 1987.
Extending the Non-Interference Version of MLS for SAT, W. D. Young, J.T. Haigh, Proc. IEEE Symposium on Security and Privacy, April, 1986, pp. 232-239. Received best paper award at the Symposium. Reprinted in IEEE Transactions on Software Engineering, January, 1987. Reprinted in Rein Turn (editor), Advances in Computer System Security, Volume III, Artech House, Inc., 1988.
The Extended Access Matrix Model of Computer Security, W. D. Young, W.E. Boebert and R.Y. Kain, Software Engineering Notes, (August, 1985), vol. 10, no. 4, pp. 119-125.
Proving a Computer System Secure, W. D. Young, W.E. Boebert and R.Y. Kain, The Scientific Honeyweller (July, 1985), vol. 6, no. 2, pp. 18-27. Reprinted in Tutorial: Computer and Network Security, eds. Marshall D. Abrams and Harold J. Podell, IEEE Computer Society Press, Washington, D.C., October, 1986. Reprinted in Rein Turn (editor), Advances in Computer System Security, Volume III, Artech House, Inc., 1988.
Secure Computing: The Secure Ada Target Approach, W. D. Young, W.E. Boebert and R.Y. Kain, The Scientific Honeyweller (July, 1985), vol. 6, no. 2, pp. 1017. Reprinted in Tutorial: Computer and Network Security, eds. Marshall D. Abrams and Harold J. Podell, IEEE Computer Society Press, Washington, D.C., October, 1986. Reprinted in Rein Turn (editor), Advances in Computer System Security, Volume III, Artech House, Inc., 1988.
The Role of the Family in `There Are No Madmen Here' by Gina Valdes, W. D. Young, Dolly J. Young, presented at Third Student Conference on Latin America, The University of Texas at Austin, April, 1983. Also appeared as a review in Revista Chicano-Riquena, vol. XIII, no. 1 (Spring, 1985), pp. 97-99.
The New Journalism in Mexico: Two Women Writers, W. D. Young, Dolly J. Young, Chasqui Revista de Literatura Latinoamericana 12:2, Febrero/Mayo, 1983, pp. 72-80. Also presented at the Southwest Conference on Latin American Studies, Abilene, Texas, March, 1982.
HAL/S/V: A Verifiable Subset of HAL/S, W. D. Young, A.R. Tripathi, D.I. Good, J.C. Browne, Sigplan Notices (March, 1981), pp. 102-113.
Steelman and the Verifiability of (Preliminary) Ada, W. D. Young, D.I. Good, Sigplan Notices (February, 1981), pp. 113-119.
Design of a Verifiable Subset for HAL/S, W. D. Young, A.R. Tripathi, D.I. Good, J.C. Browne, Technical note in Journal of Guidance and Control (January, 1981), pp. 86-87.
http://dirleton.csres.utexas.edu/staff/publications/refereed.html