Alexey Gotsman and Sebastian Burckhardt. Consistency models with global operation sequencing and their composition. DISC’17: International Symposium on Distributed Computing, 2017.
Artem Khyzha, Mike Dodds, Alexey Gotsman, and Matthew Parkinson. Proving linearizability using partial orders. ESOP’17: European Symposium on Programming, 2017.
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.
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.
Artem Khyzha, Alexey Gotsman, and Matthew Parkinson. A generic logic for proving linearizability. FM’16: International Symposium on Formal Methods, 2016.
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.
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.
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.
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.
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
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.
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.
Sebastian 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.
Gilles 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
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.
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
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.
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.
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.
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.
Mark 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.
Sebastian Burckhardt, Alexey Gotsman, and Hongseok Yang Understanding eventual consistency, Microsoft Research Technical Report MSR-TR-2013-39
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.
Alexey 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.
Sebastian 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.
Alexey 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.
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.
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.
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.
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.