Matt Kaufmann - researchr alias

researchr

You are not signed in
Sign in
Sign up

Viewing Publication 1 - 57 from 57

2020

Limited Second-Order Functionality in a First-Order SettingMatt Kaufmann, J. Strother Moore. JAR, 64(3):391-422, 2020. [doi]

2019

A Hierarchical Approach to Self-Timed Circuit VerificationCuong K. Chau, Warren A. Hunt Jr., Matt Kaufmann, Marly Roncken, Ivan E. Sutherland. async 2019: 105-113 [doi]

2018

2017

Efficient Certified RAT VerificationLuís Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt Jr., Matt Kaufmann, Peter Schneider-Kamp. cade 2017: 220-236 [doi]

Engineering a Formal, Executable x86 ISA Simulator for Software VerificationShilpi Goel, Warren A. Hunt Jr., Matt Kaufmann. In Michael G. Hinchey, Jonathan P. Bowen, Ernst-Rüdiger Olderog, editors, Provably Correct Systems. NASA Monographs in Systems and Software Engineering, pages 173-209, Springer, 2017. [doi]

Efficient, Verified Checking of Propositional ProofsMarijn Heule, Warren A. Hunt Jr., Matt Kaufmann, Nathan Wetzler. itp 2017: 269-284 [doi]

2014

Simulation and formal verification of x86 machine-code programs that make system callsShilpi Goel, Warren A. Hunt Jr., Matt Kaufmann, Soumava Ghosh. FMCAD 2014: 91-98 [doi]

Rough Diamond: An Extension of Equivalence-Based RewritingMatt Kaufmann, J. Strother Moore. itp 2014: 537-542 [doi]

2013

A Parallelized Theorem Prover for a Logic with Parallel ExecutionDavid L. Rager, Warren A. Hunt Jr., Matt Kaufmann. itp 2013: 435-450 [doi]

2012

A formal model of a large memory that supports efficient executionWarren A. Hunt Jr., Matt Kaufmann. FMCAD 2012: 60-67 [doi]

2011

The Right Tools for the Job: Correctness of Cone of Influence Reduction Proved Using ACL2 and HOL4Michael J. C. Gordon, Matt Kaufmann, Sandip Ray. JAR, 47(1):1-16, 2011. [doi]

A Futures Library and Parallelism Abstractions for a Functional Subset of LispDavid L. Rager, Warren A. Hunt Jr., Matt Kaufmann. els 2011: 13-16 [doi]

2010

ACL2 and Its Applications to Digital System VerificationMatt Kaufmann, J. Strother Moore. In David S. Hardin, editor, Design and Verification of Microprocessor Systems for High-Assurance Applications. pages 1-21, Springer, 2010. [doi]

2009

Integrating external deduction tools with ACL2Matt Kaufmann, J. Strother Moore, Sandip Ray, Erik Reeber. japll, 7(1):3-25, 2009. [doi]

2008

2007

Proof Pearl: Wellfounded Induction on the Ordinals Up to ::::epsilon:::: ::0::Matt Kaufmann, Konrad Slind. tphol 2007: 294-301 [doi]

2006

An Integration of HOL and ACL2Michael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann. FMCAD 2006: 153-160 [doi]

An embedding of the ACL2 logic in HOLMichael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds. acl2 2006: 40-46 [doi]

Double rewriting for equivalential reasoning in ACL2Matt Kaufmann, J. Strother Moore. acl2 2006: 103-106 [doi]

2005

Meta Reasoning in ACL2Warren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J. Strother Moore, Eric Whitman Smith. tphol 2005: 163-178 [doi]

2001

Nonstandard Analysis in ACL2Ruben Gamboa, Matt Kaufmann. JAR, 27(4):323-351, 2001.

Structured Theory Development for a Mechanized LogicMatt Kaufmann, J. Strother Moore. JAR, 26(2):161-203, 2001.

2000

Verification of Year 2000 conversion rules using the ACL2 theorem proverMatt Kaufmann. STTT, 3(1):13-19, 2000. [doi]

1998

ACL2 Support for Verification Projects (Invited Talk)Matt Kaufmann. cade 1998: 220-238 [doi]

Design Constraints in Symbolic Model CheckingMatt Kaufmann, Andrew Martin, Carl Pixley. cav 1998: 477-487

A Mechanically Checked Proof of the AMD5::K::86:::TM::: Floating Point Division ProgramJ. Strother Moore, Thomas W. Lynch, Matt Kaufmann. TC, 47(9):913-926, 1998.

1997

Formal Verification of FIRE: A Case StudyJae-Young Jang, Shaz Qadeer, Matt Kaufmann, Carl Pixley. dac 1997: 173-177 [doi]

An Industrial Strength Theorem Prover for a Logic Based on Common LispMatt Kaufmann, J. Strother Moore. TSE, 23(4):203-213, 1997. [doi]

Intertwined Development and Formal Verification of a 60x Bus ModelMatt Kaufmann, Carl Pixley. iccd 1997: 25-30

1996

1992

An Extension of the Boyer-Moore Theorem Prover to Support First-Order QuantificationMatt Kaufmann. JAR, 9(3):355-372, 1992.

1991

Functional Instantiation in First-Order LogicRobert S. Boyer, David M. Goldschlag, Matt Kaufmann, J. Strother Moore. BIRTHDAY 1991: 7-26 [doi]

Generalization in the Presence of Free Variables: A Mechanically-Checked Correctness Proof for one AlgorithmMatt Kaufmann. JAR, 7(1):109-158, 1991.

An Informal Discussion of Issues in Mechanically-Assisted ReasoningMatt Kaufmann. tphol 1992: 318-337

1990

RCL: A Lisp Verification SystemMatt Kaufmann. cade 1990: 659-660

1988

An Interactive Enhancement to the Boyer-Moore Theorem ProverMatt Kaufmann. cade 1988: 735-736

1987

Remarks on Weak Notions of Saturation in Models of Peano ArithmeticMatt Kaufmann, James H. Schmerl. JSYML, 52(1):129-148, 1987.

1986

The Hanf number of stationary logicMatt Kaufmann, Saharon Shelah. ndjfl, 27(1):111-123, 1986. [doi]

1985

Meeting of the Association for Symbolic Logic: Notre Dame, Indiana, 1984John T. Baldwin, Matt Kaufmann, Julia F. Knight. JSYML, 50(1):284-286, 1985.

A prototype theorem-prover for a higher-order functional languageRobert S. Boyer, Matt Kaufmann. sigsoft, 10(4):72-74, 1985. [doi]

A note on the Hanf number of second-order logicMatt Kaufmann. ndjfl, 26(4):305-308, 1985. [doi]

On random models of finite power and monadic logicMatt Kaufmann, Saharon Shelah. DM, 54(3):285-293, 1985. [doi]

1984

The Strength of Nonstandard Methods in ArithmeticC. Ward Henson, Matt Kaufmann, H. Jerome Keisler. JSYML, 49(4):1039-1058, 1984.

Filter Logics on omegaMatt Kaufmann. JSYML, 49(1):241-256, 1984.

Some remarks on equivalence in infinitary and stationary logicMatt Kaufmann. ndjfl, 25(4):383-389, 1984. [doi]

Saturation and simple extensions of models of peano arithmeticMatt Kaufmann, James H. Schmerl. APAL, 27(2):109-136, 1984. [doi]

Definable Ultrapowers and Ultrafilters over Admissible OrdinalsMatt Kaufmann, Evangelos Kranakis. mlq, 30(7-8):97-118, 1984. [doi]

A nonconservativity result on global choiceMatt Kaufmann, Saharon Shelah. APAL, 27(3):209-214, 1984. [doi]

1983

Set Theory With a Filter QuantifierMatt Kaufmann. JSYML, 48(2):263-287, 1983.

Blunt and Topless End Extensions of Models of Set TheoryMatt Kaufmann. JSYML, 48(4):1053-1073, 1983.

1979

A New Omitting Types Theorem for L(Q)Matt Kaufmann. JSYML, 44(4):507-521, 1979.

Sign in or sign up to see more results.

runs on WebDSL