Matt Kaufmann
#27,652
Most Influential Person Now
American computer scientist
Matt Kaufmann's AcademicInfluence.com Rankings
Matt Kaufmanncomputer-science Degrees
Computer Science
#1703
World Rank
#1764
Historical Rank
#814
USA Rank
Automated Reasoning
#3
World Rank
#3
Historical Rank
#2
USA Rank
Database
#8570
World Rank
#8981
Historical Rank
#1142
USA Rank
Download Badge
Computer Science
Matt Kaufmann's Degrees
- PhD Computer Science Stanford University
- Masters Computer Science Stanford University
- Bachelors Computer Science Stanford University
Similar Degrees You Can Earn
Why Is Matt Kaufmann Influential?
(Suggest an Edit or Addition)According to Wikipedia, Matt Kaufmann is a senior research scientist in the department of computer sciences at the University of Texas at Austin, United States. He was a recipient of the 2005 ACM Software System Award along with Robert S. Boyer and J Strother Moore, for his work on the Boyer-Moore Theorem Prover.
Matt Kaufmann's Published Works
Number of citations in a given year to any of this author's works
Total number of citations to an author for the works they published in a given year. This highlights publication of the most important work(s) by the author
Published Works
- Computer-Aided Reasoning: An Approach (2011) (401)
- An Industrial Strength Theorem Prover for a Logic Based on Common Lisp (1997) (272)
- Computer-aided reasoning : ACL2 case studies (2000) (265)
- ACL2 Theorems About Commercial Microprocessors (1996) (160)
- The Boyer-Moore theorem prover and its interactive enhancement (1995) (109)
- A Mechanically Checked Proof of the AMD5K86TM Floating Point Division Program (1998) (102)
- SOLPS modelling of ASDEX upgrade H-mode plasma (2006) (92)
- Structured Theory Development for a Mechanized Logic (2001) (83)
- A Mechanically Checked Proof of the (1998) (81)
- Efficient Certified RAT Verification (2016) (74)
- Functional Instantiation in First-Order Logic (1991) (72)
- Pellet injection with improved confinement in ASDEX (1988) (69)
- Effects of lateral reticular nucleus lesions on the exercise pressor reflex in cats. (1982) (63)
- Drawing Planar Graphs Using the Canonical Ordering (1996) (60)
- Experimental studies of toroidal momentum transport in ASDEX Upgrade (2004) (56)
- On random models of finite power and monadic logic (1985) (55)
- Plasma shielding of hydrogen pellets (1986) (54)
- Integrating Testing and Interactive Theorem Proving (2011) (52)
- Design Constraints in Symbolic Model Checking (1998) (49)
- Nonstandard Analysis in ACL2 (2001) (47)
- An Interactive Enhancement to the Boyer-Moore Theorem Prover (1988) (45)
- Computer-Aided Reasoning (2000) (43)
- Simulation and formal verification of x86 machine-code programs that make system calls (2014) (41)
- Efficient execution in an automated reasoning environment (2008) (39)
- Industrial hardware and software verification with ACL2 (2017) (38)
- Meta Reasoning in ACL2 (2005) (37)
- Discrepancy between modelled and measured radial electric fields in the scrape-off layer of divertor tokamaks: a challenge for 2D fluid codes? (2007) (37)
- A Precise Description of the ACL2 Logic (1998) (36)
- Efficient, Verified Checking of Propositional Proofs (2017) (35)
- A rather classless model (1977) (34)
- The Boyer-Moore Prover and Nuprl: an experimental comparison (1991) (30)
- Integrating external deduction tools with ACL2 (2006) (28)
- An ACL2 Tutorial (2008) (27)
- Commercial design verification: methodology and tools (1996) (27)
- An Integration of HOL and ACL2 (2006) (25)
- High-beta stellarator experiments on ISAR T1 (1975) (24)
- The strength of nonstandard methods in arithmetic (1984) (24)
- Engineering a Formal, Executable x86 ISA Simulator for Software Verification (2017) (21)
- Blunt and topless end extensions of models of set theory (1983) (21)
- A Counterexample to the 0-1 Law for Existential Monadic Second-Order Logic (1987) (21)
- Abstract Stobjs and Their Application to ISA Modeling (2013) (21)
- Modular proof: the fundamental theorem of calculus (2000) (20)
- Formal Verification of Floating-Point RTL at AMD Using the ACL 2 Theorem Prover (2005) (20)
- An embedding of the ACL2 logic in HOL (2006) (19)
- Refuelling and helium pumping in a tokamak reactor (1985) (18)
- A Computational Logic for Applicative Common LISP (2007) (17)
- Saturation and simple extensions of models of peano arithmetic (1984) (17)
- Formal Verification Of FIRE: A Case Study (1997) (17)
- Adding a Total Order to ACL2 (2002) (16)
- On existence of Σn end extensions (1981) (16)
- Remarks on weak notions of saturation in models of Peano arithmetic (1987) (15)
- Finite-Larmor-radius stabilization of the m = 2 instability in the Isar T1-B high-beta stellarator (1977) (15)
- Damping of Alfvén and magnetoacoustic waves at high beta (1973) (15)
- A correction to “stationary logic” (1981) (15)
- Rewriting with Equivalence Relations in ACL2 (2008) (14)
- Efficient Rewriting of Operations on Finite Structures in ACL2 (2002) (13)
- ACL2 Support for Verification Projects (Invited Talk) (1998) (13)
- Quasi-stationary pellet fuelled Ohmic discharges with medium density in ASDEX (1987) (12)
- An extension of the Boyer-Moore Theorem Prover to support first-order quantification (1992) (12)
- Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings (2010) (11)
- DEFN-SK: An Extension of the Boyer-Moore Theorem Prover to Handle First-Order Quantifiers ***DRAFT*** (1989) (11)
- The Hanf number of stationary logic (1986) (10)
- A Parallelized Theorem Prover for a Logic with Parallel Execution (2013) (10)
- A formal model of a large memory that supports efficient execution (2012) (9)
- Set theory with a filter quantifier (1983) (9)
- Factors influencing GPs’ perception of specialised palliative homecare (SPHC) importance – results of a cross-sectional study (2020) (9)
- Towards a Formal Model of the X86 ISA (2012) (9)
- ACL2 support for verification projects (1998) (8)
- Templated cluster assembly for production of metallic nanowires in passivated Silicon V-grooves (2004) (8)
- Inhalational Chlorine Injuries at Public Aquatic Venues — California, 2008–2015 (2017) (7)
- Non-Standard Analysis in ACL2 (2001) (7)
- A Versatile, Sound Tool for Simplifying Definitions (2017) (7)
- A prototype theorem-prover for a higher-order functional language (1985) (7)
- Largest initial segments pointwise fixed by automorphisms of models of set theory (2016) (7)
- Rough Diamond: An Extension of Equivalence-Based Rewriting (2014) (6)
- AN INTEGER LIBRARY FOR NQTHM (1990) (6)
- Formal Verification of Microprocessors at AMD (2002) (6)
- The Right Tools for the Job: Correctness of Cone of Influence Reduction Proved Using ACL2 and HOL4 (2011) (6)
- Integrating CCG Analysis into ACL 2 ⋆ (2006) (6)
- Should We Begin a Standardization Process for Interface Logics (1992) (6)
- A Parallel Version of the Boyer-Moore Prover (1989) (5)
- Proof Search Debugging Tools in ACL 2 (2008) (5)
- Mutually generic classes and incompatible expansions (1984) (5)
- Formal verification of LabVIEW programs using the ACL2 Theorem Prover (2009) (5)
- Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1 (2013) (5)
- Industrial-Strength Documentation for ACL2 (2014) (5)
- How Can I Do That with ACL2? Recent Enhancements to ACL2 (2011) (5)
- A Tool for Simplifying Files of ACL2 De nitions (2003) (5)
- Filter logics: Filters on ω1 (1981) (4)
- Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem (1996) (4)
- An Example in Nqthm: Ramsey's Theorem (1992) (4)
- Limited Second-Order Functionality in a First-Order Setting (2018) (4)
- Iterated ultrapowers for the masses (2017) (4)
- Abbreviated output for input in ACL2: an implementation case study (2009) (4)
- Generalization in the presence of free variables: A mechanically-checked correctness proof for one algorithm (1991) (4)
- A nonconservativity result on global choice (1984) (4)
- Definable Ultrapowers and Ultrafilters over Admissible Ordinals (1984) (4)
- Double rewriting for equivalential reasoning in ACL2 (2006) (3)
- Proof Pearl: Wellfounded Induction on the Ordinals Up to epsilon 0 (2007) (3)
- Meta-extract: Using Existing Facts in Meta-reasoning (2017) (3)
- Well-Formedness Guarantees for ACL2 Metafunctions and Clause Processors (2015) (3)
- Busbar protection: a critical review of methods and practice (1943) (3)
- A Hierarchical Approach to Self-Timed Circuit Verification (2019) (3)
- Generalization in the presence of free variables: A mechanically-checked proof for one algorithm (1991) (3)
- Intertwined development and formal verification of a 60/spl times/ bus model (1997) (3)
- Addition of Free Variables to the PC-NQTHM Interactive Enhancement of the Boyer-Moore Theorem Prover (1989) (2)
- Fourier Series Formalization in ACL2(r) (2015) (2)
- Industrial Proofs with ACL 2 (2005) (2)
- A new omitting types theorem for L(Q) (1979) (2)
- Data-Loop-Free Self-Timed Circuit Verification (2018) (2)
- Filter Logics on ω (1984) (2)
- Some remarks on equivalence in infinitary and stationary logic (1984) (2)
- Maintaining the ACL2 theorem proving system (2006) (2)
- ACL2 and Its Applications to Digital System Verification (2010) (2)
- An Informal Discussion Of Issues In Mechanically-assisted Reasoning (1991) (2)
- Quantification in Nqthm: A Recognizer and Some Constructive Implementations (1992) (2)
- The Role of Automated Reasoning in Integrated System Verification Environments (2006) (2)
- A Futures Library and Parallelism Abstractions for a Functional Subset of Lisp (2011) (2)
- Iteration in ACL2 (2020) (2)
- DefunT: A Tool for Automating Termination Proofs by Using the Community Books (Extended Abstract) (2018) (2)
- On expandability of models of arithmetic and set theory to models of weak second-order theories (1984) (2)
- Combining an Interpeter-Based Approach to Software Verification with Verification Condition Generation (1994) (2)
- Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4 (2014) (2)
- Comparing Gypsy and the Boyer-Moore Logic for Specifying Secure Systems (1987) (2)
- A note on the Hanf number of second-order logic (1985) (2)
- Verification of Year 2000 conversion rules using the ACL2 theorem prover (2000) (1)
- Development of high-current RF-plasma sources for neutral particle injectors (1988) (1)
- ACL2 essentials (2000) (1)
- Appendix to “ Iterated Ultrapowers for the Masses ” (2017) (1)
- An Extension of Equivalence-based Rewriting (2014) (1)
- RCL: A Lisp Verification System (1990) (1)
- Parallel version of the Boyer-Moore prover. Technical report (1989) (1)
- Formalizing Routing Models in ACL2 (2008) (1)
- ACL2 Workshop 2000 Proceedings, Part A (2000) (1)
- Veriication of Pipeline Circuits (2000) (1)
- A simple example for nqthm: modeling locking (1991) (1)
- -Invited Talk- ACL2 support for verification projects (1998) (1)
- Compiler Verificaton Revisted (2000) (0)
- Iterated ultrapowers for the masses (2017) (0)
- Introduction to ACL2 (2015) (0)
- Ååøø Êêê×óòòòò Ò Ä¾ Ïöööò º Àùòø¸âöº¸ååøø Ããùùññòò¸êóóöø Ðððöññòò Ãöùù¸â Åóóöö¸òò Öö Ïïïøññò Ëññøø (2005) (0)
- Building Software Systems Economically with Mechanized Logic: Initial Design Proposal (1987) (0)
- 8 Th International Workshop User Interfaces for Theorem Provers (uitp'08) Tphols'08 Satellite Workshop List of Contributions an Interactive Driver for Goal Directed Proof Strategies Managing Proof Documents for Asynchronous Processing a Lightweight Theorem Prover Interface for Eclipse Panoptes: an E (2008) (0)
- Version 1 . 5 Connecting HOL to ACL 2 (0)
- Summaries of the Case Studies (2000) (0)
- Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications (2022) (0)
- Backfill operation planning utilising power plant ashes to minimize mine damages (2020) (0)
- Meeting of the Association for Symbolic Logic (1985) (0)
- Meeting of the Association for Symbolic Logic: Notre Dame, Indiana, 1984 (1985) (0)
- High-beta stellarator experiments in Garching (1985) (0)
- How to Use the Theorem Prover (2000) (0)
- The authors' reply to the discussion on "Busbar protection: a critical review of methods and practice" (1943) (0)
- 0 10 50 01 v 1 3 M ay 2 00 1 A Measurement of the Electric Form Factor of the Neutron through (2019) (0)
- ACL2 Workshop 2000 Proceedings, Part B, Goerigk-Kaufman (2000) (0)
- Proceedings of the First international conference on Interactive Theorem Proving (2010) (0)
- Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): Preface (2010) (0)
- Formulating, mixing, degassing, casting. The new generation of vacuum systems (1999) (0)
- Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015 (2015) (0)
- Problems in Automated Theorem Proving for Hardware and Software Verification (0)
- The Mechanical Theorem Prover (2000) (0)
- Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications (2018) (0)
- ACL2 Workshop 2000 Proceedings, Part A, Lusk et al-Ruiz-Reina et al (2000) (0)
- Theorem Prover Examples (2000) (0)
- Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018 (2018) (0)
- Limited Second-Order Functionality in a First-Order Setting (2018) (0)
- Theorem Prover Exercises (2000) (0)
- L O ] 8 D ec 2 01 6 Efficient Certified RAT Verification (0)
- A Note on the Hαnf Number of Second-Order Logic (2003) (0)
This paper list is powered by the following services:
Other Resources About Matt Kaufmann
What Schools Are Affiliated With Matt Kaufmann?
Matt Kaufmann is affiliated with the following schools:
