Matt Kaufmann

2009
34	EE	Matt Kaufmann, J. Strother Moore, Sandip Ray, Erik Reeber: Integrating external deduction tools with ACL2. J. Applied Logic 7(1): 3-25 (2009)
2008
33	EE	Matt Kaufmann, J. Strother Moore: An ACL2 Tutorial. TPHOLs 2008: 17-21
32	EE	Bishop Brock, Matt Kaufmann, J. Strother Moore: Rewriting with Equivalence Relations in ACL2. J. Autom. Reasoning 40(4): 293-306 (2008)
31	EE	David A. Greve, Matt Kaufmann, Panagiotis Manolios, J. Strother Moore, Sandip Ray, José-Luis Ruiz-Reina, R. O. B. Sumners, Daron Vroon, Matthew Wilding: Efficient execution in an automated reasoning environment. J. Funct. Program. 18(1): 15-46 (2008)
2007
30	EE	Matt Kaufmann, Konrad Slind: Proof Pearl: Wellfounded Induction on the Ordinals Up to epsilon 0. TPHOLs 2007: 294-301
2006
29	EE	Matt Kaufmann, J. Strother Moore: Double rewriting for equivalential reasoning in ACL2. ACL2 2006: 103-106
28	EE	Michael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds: An embedding of the ACL2 logic in HOL. ACL2 2006: 40-46
27	EE	Michael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann: An Integration of HOL and ACL2. FMCAD 2006: 153-160
2005
26	EE	Warren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J. Strother Moore, Eric Whitman Smith: Meta Reasoning in ACL2. TPHOLs 2005: 163-178
2001
25		Matt Kaufmann, J. Strother Moore: Structured Theory Development for a Mechanized Logic. J. Autom. Reasoning 26(2): 161-203 (2001)
24		Ruben Gamboa, Matt Kaufmann: Nonstandard Analysis in ACL2. J. Autom. Reasoning 27(4): 323-351 (2001)
2000
23	EE	Matt Kaufmann: Verification of Year 2000 conversion rules using the ACL2 theorem prover. STTT 3(1): 13-19 (2000)
1998
22	EE	Matt Kaufmann: ACL2 Support for Verification Projects (Invited Talk). CADE 1998: 220-238
21		Matt Kaufmann, Andrew Martin, Carl Pixley: Design Constraints in Symbolic Model Checking. CAV 1998: 477-487
20		J. Strother Moore, Thomas W. Lynch, Matt Kaufmann: A Mechanically Checked Proof of the AMD5K86TM Floating Point Division Program. IEEE Trans. Computers 47(9): 913-926 (1998)
1997
19	EE	Jae-Young Jang, Shaz Qadeer, Matt Kaufmann, Carl Pixley: Formal Verification of FIRE: A Case Study. DAC 1997: 173-177
18		Matt Kaufmann, Carl Pixley: Intertwined Development and Formal Verification of a 60x Bus Model. ICCD 1997: 25-30
17	EE	Matt Kaufmann, J. Strother Moore: An Industrial Strength Theorem Prover for a Logic Based on Common Lisp. IEEE Trans. Software Eng. 23(4): 203-213 (1997)
1996
16		Bishop Brock, Matt Kaufmann, J. Strother Moore: ACL2 Theorems About Commercial Microprocessors. FMCAD 1996: 275-293
15		Carl Pixley, Noel R. Strader, W. C. Bruce, Jaehong Park, Matt Kaufmann, Kurt Shultz, Michael Burns, Jainendra Kumar, Jun Yuan, Janet Nguyen: Commercial Design Verification: Methodology and Tools. ITC 1996: 839-848
14		Matt Kaufmann, Paolo Pecchiari: Interaction with the Boyer-Moore Theorem Prover: A Tutorial Study Using the Arithmetic-Geometric Mean Theorem. J. Autom. Reasoning 16(1-2): 181-222 (1996)
1992
13		Matt Kaufmann: An Extension of the Boyer-Moore Theorem Prover to Support First-Order Quantification. J. Autom. Reasoning 9(3): 355-372 (1992)
1991
12		Matt Kaufmann: An Informal Discussion of Issues in Mechanically-Assisted Reasoning. TPHOLs 1991: 318-337
11		Matt Kaufmann: Generalization in the Presence of Free Variables: A Mechanically-Checked Correctness Proof for one Algorithm. J. Autom. Reasoning 7(1): 109-158 (1991)
1990
10		Matt Kaufmann: RCL: A Lisp Verification System. CADE 1990: 659-660
1988
9		Matt Kaufmann: An Interactive Enhancement to the Boyer-Moore Theorem Prover. CADE 1988: 735-736
1987
8		Matt Kaufmann, James H. Schmerl: Remarks on Weak Notions of Saturation in Models of Peano Arithmetic. J. Symb. Log. 52(1): 129-148 (1987)
1985
7	EE	Matt Kaufmann, Saharon Shelah: On random models of finite power and monadic logic. Discrete Mathematics 54(3): 285-293 (1985)
6		John T. Baldwin, Matt Kaufmann, Julia F. Knight: Meeting of the Association for Symbolic Logic: Notre Dame, Indiana, 1984. J. Symb. Log. 50(1): 284-286 (1985)
1984
5		Matt Kaufmann: Filter Logics on omega. J. Symb. Log. 49(1): 241-256 (1984)
4		C. Ward Henson, Matt Kaufmann, H. Jerome Keisler: The Strength of Nonstandard Methods in Arithmetic. J. Symb. Log. 49(4): 1039-1058 (1984)
1983
3		Matt Kaufmann: Set Theory With a Filter Quantifier. J. Symb. Log. 48(2): 263-287 (1983)
2		Matt Kaufmann: Blunt and Topless End Extensions of Models of Set Theory. J. Symb. Log. 48(4): 1053-1073 (1983)
1979
1		Matt Kaufmann: A New Omitting Types Theorem for L(Q). J. Symb. Log. 44(4): 507-521 (1979)

Coauthor Index

1	John T. Baldwin	[6]
2	Bishop Brock	[16] [32]
3	W. C. Bruce	[15]
4	Michael Burns	[15]
5	Ruben Gamboa	[24]
6	Michael J. C. Gordon	[27] [28]
7	David A. Greve	[31]
8	C. Ward Henson	[4]
9	Warren A. Hunt Jr.	[26] [27] [28]
10	Jae-Young Jang	[19]
11	H. Jerome Keisler	[4]
12	Julia F. Knight	[6]
13	Robert Bellarmine Krug	[26]
14	Jainendra Kumar	[15]
15	Thomas W. Lynch	[20]
16	Panagiotis Manolios	[31]
17	Andrew Martin	[21]
18	J. Strother Moore	[16] [17] [20] [25] [26] [29] [31] [32] [33] [34]
19	Janet Nguyen	[15]
20	Jaehong Park	[15]
21	Paolo Pecchiari	[14]
22	Carl Pixley	[15] [18] [19] [21]
23	Shaz Qadeer	[19]
24	Sandip Ray	[31] [34]
25	Erik Reeber	[34]
26	James Reynolds	[27] [28]
27	José-Luis Ruiz-Reina	[31]
28	James H. Schmerl	[8]
29	Saharon Shelah	[7]
30	Kurt Shultz	[15]
31	Konrad Slind	[30]
32	Eric Whitman Smith	[26]
33	Noel R. Strader	[15]
34	R. O. B. Sumners	[31]
35	Daron Vroon	[31]
36	Matthew Wilding	[31]
37	Jun Yuan	[15]

Colors in the list of coauthors