Joey Dodds will present his pre-FPO on Tuesday, November 11 at 9am in Room 402. The members of his committee are: Andrew Appel (advisor); David Walker and Jesper Bengtson, I.T. University of Copenhagen (readers); Sharad Malik and Aarti Gupta, NEC Labs America (nonreaders). Everyone is invited to attend his talk. The talk title and abstract follow below: "Symbolic Execution of C Programs by Computational Reflection" Verified Software Toolchain (VST) is a system for proving functional properties about C programs. It is completely implemented and proved correct in the Coq interactive proof assistant. VST is composed of a logic which allows a user to specify and reason about C programs, and Floyd, a proof automation system that allows forward symbolic execution of programs with their specifications. Floyd is implemented in Coq's tactic language, Ltac. There are two major problems with Ltac: as automation built in Ltac proceeds, Coq keeps a record of the steps that have been taken, called proof objects, that allow proofs to be checked once they are complete. These proofs can be large and very complex, causing Ltac automation to be both slow and memory hungry. The second problem with Ltac is that the flexibility of the language can lead to poor practices and slow execution. The Ltac match statement is the main cause of this issue. It allows matches against expressions of arbitrary type, and it allows backtracking when the body of a match fails. These combine to lead to confusing control flows, and slower execution than would be expected for a typed match with no backtracking. Fortunately, a technique known as computational reflection solves the problems associated with Ltac automation. Computational reflection allows automation without storing proof objects, greatly increasing speed while decreasing required memory. It also allows for principled and predictable implementations of algorithms that can be more robust and efficient than their Ltac counterparts. This thesis solves the problems with ltac by implementing reflective automation in two ways. The first is small-scale reflection. Small-scale reflection is built into the logic of VST, and uses computation to specify and check properties of programs within the logic rules. This has benefits regardless of the automation used because no proof objects need to be built about them because the computation itself is the proof. Large-scale reflection replaces the Ltac implementation of Floyd with symbolic execution by reflection. This is done using the MirrorCore library of Malecha et al. MirrorCore presents a general syntax capable of representing any Coq term, allowing computational reasoning where it would normally be impossible. Small-scale and large-scale reflection interact nicely because a well-designed large-scale reflection library will immediately be able to make use of the computation that is done as part of small-scale reflection.