Eric Smith

Dr. Eric W. Smith is a Senior Computer Scientist at Kestrel Institute with over 15 years of experience in formal methods. He currently leads Kestrel’s DerivationMiner effort, which uses synthesis techniques (derivations, specifications, and refinements) to construct correctness proofs of code found in large online repositories. He co-leads Kestrel’s related APT (Automated Program Transformations) project, which is developing proof-emitting program transformations in the ACL2 theorem prover. APT technology has been used in several Kestrel projects, including DerivationMiner, Flex, and Trusted and Resilient Systems. At Kestrel, Dr. Smith is continuing to develop the Axe tool originally written for his Ph.D. thesis. Axe includes a high-performance rewriter, theorem prover, and equivalence checker and a tool to “lift” Java bytecode programs into ACL2 logical functions. Dr. Smith is extending the Axe lifter to apply to x86 binaries for the purpose of malware detection. Dr. Smith led Kestrel’s DARPA APAC effort to find malware in Android apps and formally prove correctness of apps without malware.

Before joining Kestrel, Dr. Smith completed his Ph.D. in Computer Science at Stanford University under Prof. David Dill. He wrote Axe, a theorem prover and equivalence checker capable of highly automated proofs about real-world cryptographic programs. Dr. Smith has extensive experience with the ACL2 theorem prover, using it for microprocessor verification at AMD and for processor modeling and machine code proofs at Rockwell Collins. Dr. Smith did his undergraduate work at the University of Texas at Austin, where he earned bachelor’s degrees in Computer Science and Plan II Honors under thesis advisor J Moore.