A formal semantics of Python 3.3

This thesis demonstrates the ability to formalize the operational semantics of complex programming languages in the K Semantic Framework, which provides an interpreter as well as analysis tools for exploring the state space of programs and performing static reasoning about programs. This is demonstrated by means of a partial semantics for the latest version of the popular Python programming language. With additional effort, this semantics will allow users to reason about Python programs, including sources of nondeterminism in the Python language specification, and formal reasoning about their behavior. While the semantics is incomplete, it is executable and has been thoroughly tested against a number of unit tests, and will be demonstrated to perform as well as the reference implementation of Python, CPython, on those features which have been completed. On these features, it also performs as well as or better than other comparable operational semantics of Python