Opportunities and Challenges in End-to-End Verification of Software Systems


February 18, 2005


Daniel Wang


Princeton University


I’ll start out by taking a brief tour that covers my past experience on various projects and how those experiences shape my current view of the importance and practicality of end-to-end system verification. My basic thesis is that end-to-end system verification is theoretically/technically possible, but often *economically* impractical. More importantly the marketplace for verified software systems is likely to significantly expand within this century.

I’ll will also discuss on going research in developing simpler and flexible semantic techniques for the verification of Foundational Proof-Carrying code systems. In particular, I will discuss how to build proofs of type soundness using higher-order abstract encodings of syntax without the need for meta-logical approaches to soundness.


Daniel Wang

Daniel Wang spent his formative years in the Florida, the Sunshine State. Spent 4 years in Pittsburgh, PA and received a B.S. in Math/CS with a Minor in Psychology from Carnegie Mellon. He was shocked to discover that Pittsburgh has 700 hours less sunshine per year than Florida! (Note: Seattle has 300 fewer hours than Pittsburgh.) He went on to receive a PhD, under Andrew Appel, in Computer Science from Princeton University. After graduation he worked for Agere Systems, formerly the microelectronics division of Lucent, helping to develop next-generation network-processors. Recently he has returned to Princeton as Research Staff working on the Foundational Proof-Carrying Code project.