3260 Hillview Avenue
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.
Tools: The tools I am working on these days include APT and Axe.
Axe: An Automated Formal Equivalence Checking Tool for Programs. Eric W. Smith. Ph.D. Dissertation. Stanford University. 2011.
Automatic Formal Verification of Block Cipher Implementations. Eric Smith and David Dill. FMCAD ‘08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, November, 2008.
Formal Verification of Floating-Point RTL at AMD Using the ACL2 Theorem Prover. David Russinoff, Matt Kaufmann, Eric Smith, and Robert Sumners. 17th IMACS World Congress: Scientific Computation, Applied Mathematics and Simulation. July, 2005.
Meta Reasoning in ACL2. Warren A. Hunt, Matt Kaufmann, Robert Bellarmine Krug, and Eric Whitman Smith. 18th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2005, J. Hurd and T. Melham (eds.), Springer Lecture Notes in Computer Science, 3603, pp. 163–178, 2005.
A Robust Machine Code Proof Framework for Highly Secure Applications. David S. Hardin, Eric W. Smith, and William D. Young. ACL2 ‘06: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, 2006.
Android Platform Modeling and Android App Verification in the ACL2 Theorem Prover, Eric Smith and Alessandro Coglio, Proc. 7th Working Conference on Verified Software: Tools, Techniques, and Experiments (VSTTE), 2015
A Versatile, Sound Tool for Simplifying Definitions, Alessandro Coglio, Matt Kaufmann, and Eric W. Smith. To appear in 14th International Workshop on the ACL2 Theorem Prover and Its Applications, 2017