@InProceedings{yu03:cdsa,
  author =       {Dachuan Yu and Nadeem A. Hamid and Zhong Shao},
  title =        {Building Certified Libraries for {PCC}: Dynamic Storage Allocation},
  booktitle =    {Proc. 2003 European Symposium on Programming (ESOP'03)},
  year =         2003,
  month =        {April},
  abstract =     {
  Proof-Carrying Code (PCC) allows a code producer to provide to a host
  a program along with its formal safety proof. The proof attests a
  certain safety policy enforced by the code, and can be mechanically
  checked by the host. While this language-based approach to code
  certification is very general in principle, existing PCC systems have
  only focused on programs whose safety proofs can be automatically
  generated. As a result, many low-level system libraries (e.g., memory
  management) have not yet been handled.
  In this paper, we explore a complementary approach in which general
  properties and program correctness are semi-automatically certified.
  In particular, we introduce a low-level language CAP for building
  certified programs and present a certified library for dynamic storage
  allocation.} 
}