A formal model of Checked C. - Liyi Li 002; Yiyun Liu; Deena L. Postol; Leonidas Lampropoulos; David Van Horn; Michael Hicks 001 (J. Comput. Secur., 2023)