Paper critique and presentation guidelines.
 

Date	Presenter	Paper
04/20	Aaron Tetens	Foundational proof-carrying code by Appel, Andrew W @inproceedings{appel2001foundational, title={Foundational proof-carrying code}, author={Appel, Andrew W}, booktitle={Logic in Computer Science, 2001. Proceedings. 16th Annual IEEE Symposium on}, pages={247--256}, year={2001}, organization={IEEE} }
	Joseph Iaquinto	A framework for analysing the effect of `change' in legacy code by S. Zhou, H. Zedan and A. Cau Software Maintenance, 1999. (ICSM '99) Proceedings. IEEE International Conference on, Oxford, 1999, pp. 411-420. doi: 10.1109/ICSM.1999.792639
	Muhammad Ishaq	A Fast and Verified Software Stack for Secure Function Evaluation by José Bacelar Almeida and Manuel Barbosa and Gilles Barthe and François Dupressoir and Benjamin Grégoire and Vincent Laporte and Vitor Pereira Cryptology ePrint Archive, Report 2017/821 @misc{cryptoeprint:2017:821, author = {José Bacelar Almeida and Manuel Barbosa and Gilles Barthe and François Dupressoir and Benjamin Grégoire and Vincent Laporte and Vitor Pereira}, title = {A Fast and Verified Software Stack for Secure Function Evaluation}, howpublished = {Cryptology ePrint Archive, Report 2017/821}, year = {2017}, note = {\url{https://eprint.iacr.org/2017/821}}, } @misc{cryptoeprint:2017:879, author = {Jean-Sebastien Coron}, title = {Formal Verification of Side-channel Countermeasures via Elementary Circuit Transformations}, howpublished = {Cryptology ePrint Archive, Report 2017/879}, year = {2017}, note = {\url{https://eprint.iacr.org/2017/879}}, }
	Avi Weinstock	Foundations of Garbled Circuits by Mihir Bellare, Viet Tung Hoang, and Phillip Rogaway ACM Computer and Communications Security (CCS’12). ACM, 2012
04/24	Saswata Paul	Predicate abstraction for software verification by Flanagan, Cormac and Qadeer, Shaz ACM SIGPLAN Notices
	Daniel Park	Software Verification for Weak Memory via Program Transformation by Jade Alglave and Daniel Kroening and Vincent Nimal and Michael Tautschnig. CoRR
	Samuel Breese	Idris, a general-purpose dependently typed programming language: Design and implementation by Brady, Edwin Journal of Functional Programming @article{brady2013idris, title={Idris, a general-purpose dependently typed programming language: Design and implementation}, author={Brady, Edwin}, journal={Journal of Functional Programming}, volume={23}, number={5}, pages={552--593}, year={2013}, publisher={Cambridge University Press} }
	Ayushi Mishra	A Calculus for Cryptographic Protocols: The Spi Calculus by Martin Abadi and Andrew D. Gordon @article{ABADI19991,title = "A Calculus for Cryptographic Protocols: The Spi Calculus",journal = "Information and Computation",volume = "148",number = "1",pages = "1 - 70",year = "1999",issn = "0890-5401",doi = "https://doi.org/10.1006/inco.1998.2740",url = "http://www.sciencedirect.com/science/article/pii/S0890540198927407",author = "Mart n Abadi and Andrew D. Gordon"}
	Richie Young	Formalization and Verification of REST on HTTP Using CSP by Ting Yuan and Yiting Tang and Xi Wu and Yue Zhang and Huibiao Zhu and Jian Guo and Weijun Qin Proceedings of the Sixth International Workshop on Harnessing Theories for Tool Support for Software (TTSS) @article{YUAN201475, title = "Formalization and Verification of REST on HTTP Using CSP", journal = "Electronic Notes in Theoretical Computer Science", volume = "309", pages = "75 - 93", year = "2014", note = "Proceedings of the Sixth International Workshop on Harnessing Theories for Tool Support for Software (TTSS)", issn = "1571-0661", doi = "https://doi.org/10.1016/j.entcs.2014.12.007", url = "http://www.sciencedirect.com/science/article/pii/S1571066114000917", author = "Ting Yuan and Yiting Tang and Xi Wu and Yue Zhang and Huibiao Zhu and Jian Guo and Weijun Qin", keywords = "REST, HTTP, CSP, Stateless, Hypertext-driven", abstract = "Representational State Transfer (REST), as a promising software architecture style, has been used in large scale since proposed. But considerable confusions about REST exist and many examples of supposedly RESTful applications violate key REST constraints. In this paper, we focus on the most important constraints of REST, stateless property and hypertext-driven property. First we establish a formal model for REST on HTTP in CSP. In the model, components in RESTful systems communicate with each other using standard HTTP methods and are modeled as CSP processes. From the model we can find the effects of HTTP methods on resources. Then we give formal descriptions for failure cases of stateless, hypertext-driven constraints of REST, and safe, idempotent properties of HTTP methods, within which whether a system breaks REST constraints or basic HTTP requirements can be checked. Furthermore, we use model checker PAT to prove all the constraints hold in our model. In the end, a case study about the process of buying food is mapped to our model to better illustrate the REST concepts and our approach." }