Resources cited in this volume

[Appel 2014] Program Logics for Certified Compilers, by Andrew W. Appel with Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. Cambridge University Press, 2014.
[Appel 2015] Verification of a Cryptographic Primitive: SHA-256, by Andrew W. Appel, ACM Transactions on Programming Languages and Systems 37(2) 7:1-7:31, April 2015.
[Appel and Naumann 2020] Verified sequential malloc/free, by Andrew W. Appel and David A. Naumann, in 2020 ACM SIGPLAN International Symposium on Memory Management, June 2020.
[Beringer 2015] Verified Correctness and Security of OpenSSL HMAC, by Lennart Beringer, Adam Petcher, Katherine Q. Ye, and Andrew W. Appel. 24th USENIX Security Symposium, pages 207-221, August 2015.
[Beringer 2019] Abstraction and Subsumption in Modular Verification of C Programs, by Lennart Beringer and Andrew W. Appel. In: Maurice H. ter Beek and Annabelle McIver: Formal Methods -- the next 30 years. Proceedings of the 23rd International Symposium on Formal Methods (FM'19), pages 573-590, Springer, 2019.
[Chargueraud 2010] Program verification through characteristic formulae, by Arthur Chargueraud, in Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, pp. 321-332, 2010.
[Jacobs 2011] VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java, by Bart Jacobs, Jan Smans, Pieter Philippaerts, Frederic Vogels, Willem Penninckx, and Frank Piessens. In Proc. NASA Formal Methods (NFM) 2011.
[Koh 2020] From C To Interaction Trees: specifying, verifying and testing a networked server, by Nicolas Koh, Yao Li, Yishuai Li, Li-Yao Xia, Lennart Beringer, Wolf Honore, William Mansky, Benjamin C Pierce, and Steve Zdancewic. CPP 2019 Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Pages 234-248, ACM, 2019
[Kumar 2014] CakeML: a verified implementation of ML, by Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens, in POPL'14, ACM SIGPLAN Notices 49, no. 1 (2014): 179-191.
[Leino 2010] Dafny: An automatic program verifier for functional correctness, by K. Rustan M. Leino, International Conference on Logic for Programming Artificial Intelligence and Reasoning, pp. 348-370, 2010.
[Mansky 2017] A verified messaging system, by William Mansky, Andrew W. Appel, and Aleksey Nogin. OOPSLA'17: ACM Conference on Object-Oriented Programming Systems, Languages, and Applications, October 2017. PACM/PL volume 1, issue OOPSLA, paper 87, 2017.
[Mansky 2020] Connecting Higher-Order Separation Logic to a First-Order Outside World, by William Mansky, Wolf Honoré, and Andrew W. Appel, ESOP 2020: European Symposium on Programming, April 2020.
[Spector-Zabusky 2018] Total Haskell is reasonable Coq, by Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, and Stephanie Weirich. CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, January 2018.
[Wang 2019] Certifying Graph-Manipulating C Programs via Localizations within Data Structures, by Shengyi Wang, Qinxiang Cao, Anshuman Mohan, and Aquinas Hobor. OOPSLA: Conference on Object-Oriented Programming Systems, Languages, and Applications; PACM/PL volume 3, issue OOPSLA, 2019.
[Ye 2017] Verified Correctness and Security of mbedTLS HMAC-DRBG, by Katherine Q. Ye, Matthew Green, Naphat Sanguansin, Lennart Beringer, Adam Petcher, and Andrew W. Appel, CCS'17: ACM Conference on Computer and Communications Security, October 2017.
(* 2023-03-25 11:30 *)