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. https://www.cs.princeton.edu/~appel/papers/verif-sha-2.pdf [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. https://www.cs.princeton.edu/~appel/papers/memmgr.pdf [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. https://www.cs.princeton.edu/~appel/papers/verified-hmac.pdf [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. https://www.cs.princeton.edu/~appel/papers/funspec_sub.pdf [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. https://dl.acm.org/doi/pdf/10.1145/1863543.1863590 [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. https://people.cs.kuleuven.be/~bart.jacobs/nfm2011.pdf [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 https://dl.acm.org/citation.cfm?doid=3293880.3294106 [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. https://www.cs.princeton.edu/~appel/papers/connecting-esop.pdf [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. https://doi.org/10.1145/3167092 [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. https://dl.acm.org/doi/pdf/10.1145/3360597 [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. https://www.cs.princeton.edu/~appel/papers/verified-hmac-drbg.pdf