The April 17, 2015 seminar is a PRACTICE TALK for the following Ph.D. proposal. ..... Ph.D. Proposal: Shilpi Goel Supervisor: Warren A. Hunt, Jr. Title: Analysis of x86 Application and System Programs via Machine-Code Verification Abstract: Ensuring the reliability of high-level programs is becoming more difficult with the ever-increasing complexity of computing systems. Although automatic program analysis tools have found great success in industrial applications, they have limited scope because they target specific kinds of undesirable behavior, such as buffer overflows. Incorrect compiler transformations and the absence of analysis systems for some high-level languages suggest that a lowest-common-denominator strategy, namely machine-code analysis, will facilitate extensive program verification. For this dissertation project, we are developing a general framework for the mechanical verification of software by analyzing its corresponding machine (binary) code. To this end, we are specifying a formal and executable model of the x86 instruction set architecture (ISA) using the ACL2 theorem-proving system. Notably, this model can be used for the functional verification of application as well as system programs. If successful, this project will provide the capability to mechanically verify a wide variety of properties of x86 programs, including their correctness with respect to behavior, security, and resource requirements. We have already used this x86 ISA model to prove the correctness of some application programs, such as a binary-level word-count program that makes system calls to obtain its input. This binary program was obtained by compiling the corresponding source program using the LLVM compiler. We will demonstrate the capabilities of this framework by verifying system programs that access and modify system data structures, such as memory management structures. ----------------------------------------------------------------------