dblp.uni-trier.dewww.uni-trier.de

Matt Kaufmann Vis

List of publications from the DBLP Bibliography Server - FAQ
Coauthor Index - Ask others: ACM DL/Guide - CiteSeerX - CSB - MetaPress - Google - Bing - Yahoo
Home Page

*2009
34EEMatt Kaufmann, J. Strother Moore, Sandip Ray, Erik Reeber: Integrating external deduction tools with ACL2. J. Applied Logic 7(1): 3-25 (2009)
2008
33EEMatt Kaufmann, J. Strother Moore: An ACL2 Tutorial. TPHOLs 2008: 17-21
32EEBishop Brock, Matt Kaufmann, J. Strother Moore: Rewriting with Equivalence Relations in ACL2. J. Autom. Reasoning 40(4): 293-306 (2008)
31EEDavid A. Greve, Matt Kaufmann, Panagiotis Manolios, J. Strother Moore, Sandip Ray, José-Luis Ruiz-Reina, Rob Sumners, Daron Vroon, Matthew Wilding: Efficient execution in an automated reasoning environment. J. Funct. Program. 18(1): 15-46 (2008)
2007
30EEMatt Kaufmann, Konrad Slind: Proof Pearl: Wellfounded Induction on the Ordinals Up to epsilon 0. TPHOLs 2007: 294-301
2006
29EEMatt Kaufmann, J. Strother Moore: Double rewriting for equivalential reasoning in ACL2. ACL2 2006: 103-106
28EEMichael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds: An embedding of the ACL2 logic in HOL. ACL2 2006: 40-46
27EEMichael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann: An Integration of HOL and ACL2. FMCAD 2006: 153-160
2005
26EEWarren 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
23EEMatt Kaufmann: Verification of Year 2000 conversion rules using the ACL2 theorem prover. STTT 3(1): 13-19 (2000)
1998
22EEMatt Kaufmann: ACL2 Support for Verification Projects (Invited Talk). CADE 1998: 220-238
21EEMatt 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
19EEJae-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
17EEMatt 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
10EEMatt Kaufmann: RCL: A Lisp Verification System. CADE 1990: 659-660
1988
9EEMatt 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
7EEMatt 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

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

Colors in the list of coauthors

Copyright © Tue Nov 3 08:52:44 2009 by Michael Ley (ley@uni-trier.de)