Dynamic Software Updating (DSU) is a promising technique for updating running system without incurring downtime. Correctness during updating must be guaranteed because bugs or even crashes caused by dynamic updating may lead to fatal result. In this paper, we present a formal tool called KupC for modeling and verifying dynamic updating of C programs. The tool is built upon a semantic framework for programming languages called K. Using K, we formalize a patch-based dynamic updating strategy based on the formal executable operational semantics of C language which is defined in K. The formalization automatically yields an interpreter and formal verification tools, which enable us to verify the correctness of dynamic updating for C programs. According to our knowledge, KupC is the first formal tool that supports code-level verification of dynamic updating of programs.