Safety Verification of Dynamic Storage Management in Coq

The increasing scale and complexity of software makes the software safety and security critical. Thus more and more research focuses on the development of high-assurance software. Since type system is not expressive enough, the existing research does not touch the verification of infrastructure codes. In this paper, a certified dynamic storage management library is built using Hoare-logic style reasoning at the assembly level with the assistance of a theorem formalization and proof tool called Coq, since Hoare logic is more expressive. This work is a significant application of program verification technique. The experiment shows that program verification can be applied in high-assurance software development.