Matt Kaufmann

E373588

computer scientist person

Matt Kaufmann is a computer scientist best known for his work on automated theorem proving and the ACL2 theorem prover, often in collaboration with J Strother Moore.

Try in SPARQL Jump to: Surface forms Statements Referenced by

All labels observed (1)

Label	Occurrences
Matt Kaufmann canonical	3

Statements (45)

Predicate	Object
instanceOf	computer scientist ⓘ person ⓘ
affiliation	Department of Computer Science, University of Texas at Austin ⓘ
almaMater	University of Texas at Austin ⓘ
awardReceived	ACM Software System Award ⓘ CAV Award ⓘ Herbrand Award ⓘ
basedOn	Boyer–Moore theorem prover ⓘ surface form: Boyer–Moore theorem prover (Nqthm)
coauthorOf	"Computer-Aided Reasoning: An Approach" ⓘ
coauthorWith	David M. Russinoff NERFINISHED ⓘ J Strother Moore ⓘ Panagiotis Manolios ⓘ Robert S. Boyer NERFINISHED ⓘ
coDeveloperOf	ACL2 theorem proving system ⓘ surface form: ACL2
collaboratesWith	J Strother Moore ⓘ
contributedTo	formal verification of industrial hardware and software using ACL2 ⓘ
developed	ACL2 theorem proving system ⓘ surface form: ACL2 logic and theorem prover
developsSoftwareIn	Common Lisp ⓘ
educatedAt	Massachusetts Institute of Technology ⓘ
fieldOfWork	automated theorem proving ⓘ computer science ⓘ formal methods ⓘ
hasAcademicAdvisor	Robert S. Boyer NERFINISHED ⓘ
hasGivenInvitedTalkOn	automated reasoning with ACL2 ⓘ
hasGivenTutorialOn	ACL2 theorem proving ⓘ
hasHomepage	http://www.cs.utexas.edu/users/kaufmann/ ⓘ
hasRole	researcher ⓘ software developer ⓘ university faculty member ⓘ
influencedBy	Boyer–Moore theorem prover ⓘ surface form: Nqthm theorem prover
knownFor	ACL2 theorem proving system ⓘ surface form: ACL2 theorem prover automated theorem proving ⓘ
languageUsed	Common Lisp ⓘ
mainWorkFocus	design and implementation of ACL2 ⓘ
memberOf	ACL2 theorem proving system ⓘ surface form: ACL2 community
nationality	American ⓘ
notablePublication	ACL2 theorem proving system ⓘ surface form: "ACL2: An Industrial Strength Version of Nqthm" "Computer-Aided Reasoning: An Approach" ⓘ
notableWork	ACL2 theorem proving system ⓘ surface form: ACL2
researchInterest	Lisp-based theorem proving ⓘ formal verification ⓘ mechanical theorem proving ⓘ program verification ⓘ
teachesAt	University of Texas at Austin ⓘ
workInstitution	University of Texas at Austin ⓘ

Referenced by (3)

Full triples — surface form annotated when it differs from this entity's canonical label.

J Strother Moore → coAuthorWith → Matt Kaufmann ⓘ

Robert S. Boyer → collaboratedWith → Matt Kaufmann ⓘ

Robert S. Boyer → coAuthor → Matt Kaufmann ⓘ