| 2015 | EuroCrypt | Mind the Gap: Modular Machine-Checked Proofs of One-Round Key Exchange Protocols. | Gilles Barthe, Juan Manuel Crespo, Yassine Lakhnech, Benedikt Schmidt |
| 2013 | CCS | Fully automated analysis of padding-based encryption in the computational model. | Gilles Barthe, Juan Manuel Crespo, Benjamin Grgoire, Csar Kunz, Yassine Lakhnech, Benedikt Schmidt, Santiago Zanella-Bguelin |
| 2013 | ESORICS | Automated Security Proofs for Almost-Universal Hash for MAC Verification. | Martin Gagn, Pascal Lafourcade, Yassine Lakhnech |
| 2013 | FOSSACS | On Unique Decomposition of Processes in the Applied π-Calculus. | Jannik Dreier, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech |
| 2013 | ProvSec | CIL Security Proof for a Password-Based Key Exchange. | Cristian Ene, Clmentine Gritti, Yassine Lakhnech |
| 2012 | CPP | Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs. | Gilles Barthe, Benjamin Grgoire, Csar Kunz, Yassine Lakhnech, Santiago Zanella-Bguelin |
| 2012 | ESORICS | Defining Privacy for Weighted Votes, Single and Multi-voter Coercion. | Jannik Dreier, Pascal Lafourcade, Yassine Lakhnech |
| 2011 | CPP | Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience. | Pierre Corbineau, Mathilde Duclos, Yassine Lakhnech |
| 2010 | CCS | Computational indistinguishability logic. | Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech |
| 2010 | LPAR | On the Equality of Probabilistic Terms. | Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech, Vincent Laporte |
| 2009 | ESORICS | Formal Indistinguishability Extended to the Random Oracle Model. | Cristian Ene, Yassine Lakhnech, Van Chan Ngo |
| 2008 | CCS | Towards automated proofs for asymmetric encryption schemes in the random oracle model. | Judical Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech |
| 2007 | CRYPTO | A Generalization of DDH with Applications to Protocol Analysis and Computational Soundness. | Emmanuel Bresson, Yassine Lakhnech, Laurent Mazar, Bogdan Warinschi |
| 2006 | ICALP | Flat Parametric Counter Automata. | Marius Bozga, Radu Iosif, Yassine Lakhnech |
| 2005 | ESOP | Completing the Picture: Soundness of Formal Encryption in the Presence of Active Adversaries. | Romain Janvier, Yassine Lakhnech, Laurent Mazar |
| 2004 | CONCUR | A Symbolic Decision Procedure for Cryptographic Protocols with Time Stamps (Extended Abstract). | Liana Bozga, Cristian Ene, Yassine Lakhnech |
| 2004 | FOSSACS | On the Existence of an Effective and Complete Inference System for Cryptographic Protocols. | Liana Bozga, Cristian Ene, Yassine Lakhnech |
| 2004 | SAS | On Logics of Aliasing. | Marius Bozga, Radu Iosif, Yassine Lakhnech |
| 2003 | CAV | HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols. | Liana Bozga, Yassine Lakhnech, Michal Prin |
| 2003 | PEPM | Storeless semantics and alias logic. | Marius Bozga, Radu Iosif, Yassine Lakhnech |
| 2003 | TACAS | Pattern-Based Abstraction for Verifying Secrecy in Protocols. | Liana Bozga, Yassine Lakhnech, Michal Prin |
| 2002 | VMCAI | Parameterized Verification of a Cache Coherence Protocol: Safety and Liveness. | Kai Baukus, Yassine Lakhnech, Karsten Stahl |
| 2001 | CAV | Iterating Transducers. | Dennis Dams, Yassine Lakhnech, Martin Steffen |
| 2001 | SAS | Analyzing Fair Parametric Extended Automata. | Ahmed Bouajjani, Aurore Collomb-Annichini, Yassine Lakhnech, Mihaela Sighireanu |
| 2001 | TACAS | Incremental Verification by Abstraction. | Yassine Lakhnech, Saddek Bensalem, Sergey Berezin, Sam Owre |
| 2000 | SAS | A Transformational Approach for Generating Non-linear Invariants. | Saddek Bensalem, Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Yassine Lakhnech |
| 2000 | TACAS | Abstracting WS1S Systems to Verify Parameterized Networks. | Kai Baukus, Saddek Bensalem, Yassine Lakhnech, Karsten Stahl |
| 1999 | CAV | Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis. | Parosh Aziz Abdulla, Aurore Annichini, Saddek Bensalem, Ahmed Bouajjani, Peter Habermehl, Yassine Lakhnech |
| 1998 | CAV | Computing Abstractions of Infinite State Systems Compositionally and Automatically. | Saddek Bensalem, Yassine Lakhnech, Sam Owre |
| 1998 | CAV | InVeST: A Tool for the Verification of Invariants. | Saddek Bensalem, Yassine Lakhnech, Sam Owre |
| 1996 | CAV | Powerful Techniques for the Automatic Generation of Invariants. | Saddek Bensalem, Yassine Lakhnech, Hassen Sadi |
| 1996 | FM | Modular Completeness: Integrating the Reuse of Specified Software in Top-down Program Development. | Job Zwiers, Ulrich Hannemann, Yassine Lakhnech, Willem P. de Roever, Frank A. Stomp |
| 1995 | CAV | From Duration Calculus To Linear Hybrid Automata. | Ahmed Bouajjani, Yassine Lakhnech, Riadh Robbana |
| 1995 | CONCUR | Temporal Logic + Timed Automata: Expressiveness and Decidability. | Ahmed Bouajjani, Yassine Lakhnech |
| 1992 | CC | Provably Correct Compiler Development and Implementation. | Bettina Buth, Karl-Heinz Buth, Martin Frnzle, Burghard von Karger, Yassine Lakhnech, Hans Langmaack, Markus Mller-Olm |