Publications


187-pencil Artem Khyzha, Mike Dodds, Alexey Gotsman, and Matthew Parkinson. Proving linearizability using partial orders. ESOP’17: European Symposium on Programming, 2017.


187-pencil Gilles Barthe, Gian Pietro Farina, Marco Gaboardi, Emilio Jesús Gallego Arias, Andy Gordon, Justin Hsu, Pierre-Yves Strub. Differentially Private Bayesian Programming. CCS’16: ACM Conference on Computer and Communications Security, 2016.


187-pencil Dario Fiore, Cédric Fournet, Esha Ghosh, Markulf Kohlweiss, Olga Ohrimenko, Bryan Parno. Hash First, Argue Later: Adaptive Verifiable Computations on Outsourced Data. CCS’16: ACM Conference on Computer and Communications Security, 2016.


187-pencil Artem Khyzha, Alexey Gotsman, and Matthew Parkinson. A generic logic for proving linearizability. FM’16: International Symposium on Formal Methods, 2016.


187-pencil Hagit Attiya, Sebastian Burckhardt, Alexey Gotsman, Adam Morrison, Hongseok Yang, and Marek Zawirski. Specification and complexity of collaborative text editing. PODC’16: Symposium on Principles of Distributed Computing, 2016.


187-pencil Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cedric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, Santiago Zanella-Beguelin. Dependent Types and Multi-Monadic Effects in F*. ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2016.


187-pencil Klaus von Gleissenthall, Boris Köpf, Andrey Rybalchenko. Symbolic Polytopes for Quantitative Interpolation and Verification. Proc. 27th International Conference on Computer Aided Verification (CAV ’15), Springer, 2015.


187-pencil Arvind Haran, Montgomery Carter, Michael Emmi, Akash Lal, Shaz Qadeer, Zvonimir Rakamaric. SMACK+Corral: A Modular Verifier. TACAS ’15: Proc. 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2015.


187-pencil A Messy State of the Union: Taming the Composite State Machines of TLS Benjamin Beurdouche (INRIA), Karthikeyan Bhargavan (INRIA), Antoine Delignat-Lavaud (INRIA), Cédric Fournet (Microsoft Research), Markulf Kohlweiss (Microsoft Research), Alfredo Pironti (INRIA), Pierre-Yves Strub (IMDEA), Jean Karim Zinzindohoue (INRIA). 36th IEEE Symposium on Security and Privacy, 2015


187-pencil
Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, and Gavin M. Bierman. Gradual typing embedded securely in javascript. In Suresh Jagannathan and Peter Sewell, editors, POPL, pages 425–438. ACM, 2014.


187-pencil Ilya Sergey, Dimitrios Vytiniotis and Simon Peyton Jones: Modular, Higher-Order Cardinality Analysis in Theory and Practice   41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2014). San Diego, CA, USA, January 2014. Pages 335-348, ACM.


187-pencilSebastian Burckhardt, Alexey Gotsman, Hongseok Yang, and Marek Zawirski Replicated data types: specification, verification, optimality POPL’14: Symposium on Principles of Programming Languages, San Diego, CA, USA, pages 271-284. ACM, 2014.


187-pencilGilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy and Santiago Zanella-Béguelin: Probabilistic Relational Verification for Cryptographic Implementations. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’14). 2014


187-pencil
Cédric Fournet, Nikhil Swamy, Juan Chen, Pierre-Évariste Dagand, Pierre-Yves Strub, and Benjamin Livshits. Fully abstract compilation to javascript. In Roberto Giacobazzi and Radhia Cousot, editors, POPL, pages 371–384. ACM, 2013.


187-pencil Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti and Pierre-Yves Strub: Implementing TLS with Verified Cryptographic Security In IEEE Symposium on Security and Privacy (S&P’13). 2013, pp. 445–459


187-pencil
Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, and Derek Dreyer. How to make ad hoc proof automation less ad-hoc. J. Funct. Program., 23(4):357–401, 2013.


187-pencil
Boris Köpf and Andrey Rybalchenko. Automation of quantitative information-flow analysis. In Marco Bernardo, Erik P. de Vink, Alessandra Di Pierro, and Herbert Wiklicky, editors, SFM, volume 7938 of Lecture Notes in Computer Science, pages 1–28. Springer, 2013.


187-pencil
Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, and Jean Yang. Secure distributed programming with value-dependent types. J. Funct. Program., 23(4):402–451, 2013.


187-pencil Gilles Barthe, George Danezis, Benjamin Grégoire, César Kunz and Santiago Zanella-Béguelin Verified Computational Differential Privacy with Applications to Smart Metering. In IEEE Computer Security Foundations Symposium (CSF’13). 2013, pp. 287–301.


187-pencilMark Marron, César Sánchez, Zhendong Su, Manuel Fähndrich. Abstracting Runtime Heaps for Program Understanding. IEEE Transactions on Software Engineering, Vol. 39, Num. 6, pages 774–786, IEEE Computer Society, 2013.


187-pencilSebastian Burckhardt, Alexey Gotsman, and Hongseok Yang Understanding eventual consistency, Microsoft Research Technical Report MSR-TR-2013-39


187-pencil
Pierre-Yves Strub, Nikhil Swamy, Cédric Fournet, and Juan Chen. Self-certification: bootstrapping certified typecheckers in F* with Coq. In John Field and Michael Hicks, editors, POPL, pages 571–584. ACM, 2012.


187-pencilAlexey Gotsman, Madanlal Musuvathi, and Hongseok Yang: Show no weakness: sequentially consistent specifications of TSO libraries DISC’12: International Symposium on Distributed Computing, Salvador, Bahia, Brazil, LNCS 7611, pages 31-45. Springer, 2012.


187-pencilSebastian Burckhardt, Alexey Gotsman, Madanlal Musuvathi, and Hongseok Yang Concurrent library correctness on the TSO memory model [PDF] ESOP’12: European Symposium on Programming, Tallinn, Estonia, LNCS 7211, pages 87-107. Springer, 2012.


187-pencilAlexey Gotsman, Josh Berdine, and Byron Cook Precision and the conjunction rule in concurrent separation logic [PDF] MFPS’11: Conference on the Mathematical Foundations of Programming Semantics, Pittsburgh, PA, USA, ENTCS 276:171-190. Elsevier, 2011.


187-pencil
Cédric Fournet, Markulf Kohlweiss and Pierre-Yves Strub: Modular Code-Based Cryptographic Verification , by In ACM Conference on Computer and Communications Security (CCS’11). 2011, pp. 341–350.


187-pencil Boris Köpf and Andrey Rybalchenko: Approximation and Randomization for Quantitative Information-Flow Analysis. In IEEE Computer Security Foundations Symposium (CSF’10). 2010, pp. 3–14.


187-pencil François Dupressoir, Andrew D. Gordon, Jan Jürjens and David A. Naumann: Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols. In Journal of Computer Security (JCS), to appear.


187-pencil Ben Livshits, Aditya Nori, Sriram Rajamani and Anindya Banerjee: Merlin: Specification Inference for Explicit Information Flow Problems. In ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI’09). 2009, pp. 75–86.