| 2025 | MEMOCODE | Time Aware Compilation Verified: A Category-Theoretic Approach in Rocq. | Benjamin Lion, David Nowak |
| 2022 | ECOOP | Defining Corecursive Functions in Coq Using Approximations. | Vlad Rusu, David Nowak |
| 2022 | RTAS | A Formal Correctness Proof for an EDF Scheduler Implementation. | Florian Vanhems, Vlad Rusu, David Nowak, Gilles Grimaud |
| 2019 | MPC | A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning. | Reynald Affeldt, David Nowak, Takafumi Saikawa |
| 2018 | CPP | Formal proof of polynomial-time complexity with quasi-interpretations. | Hugo Fre, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, David Nowak |
| 2017 | SYNASC | A Certified Procedure for RL Verification. | Andrei Arusoaie, David Nowak, Vlad Rusu, Dorel Lucanu |
| 2016 | TASE | Formal Proof of Dynamic Memory Isolation Based on MMU. | Narjes Jomaa, David Nowak, Gilles Grimaud, Samuel Hym |
| 2011 | ITP | A Formalization of Polytime Functions. | Sylvain Heraud, David Nowak |
| 2010 | ProvSec | A Calculus for Game-Based Security Proofs. | David Nowak, Yu Zhang |
| 2008 | ICISC | On Formal Verification of Arithmetic-Based Cryptographic Primitives. | David Nowak |
| 2007 | ICICS | A Framework for Game-Based Security Proofs. | David Nowak |
| 2005 | ATVA | Reasoning About Transfinite Sequences. | Stphane Demri, David Nowak |
| 2005 | TIME | On the Freeze Quantifier in Constraint LTL: Decidability and Complexity. | Stphane Demri, Ranko Lazic, David Nowak |
| 2004 | CSL | Complete Lax Logical Relations for Cryptographic Lambda-Calculi. | Jean Goubault-Larrecq, Slawomir Lasota, David Nowak, Yu Zhang |
| 2003 | CSL | Logical Relations for Dynamic Name Creation. | Yu Zhang, David Nowak |
| 2003 | ICFEM | Formal Proof of a Polychronous Protocol for Loosely Time-Triggered Architectures. | Mickal Kerboeuf, David Nowak, Jean-Pierre Talpin |
| 2002 | CSL | Logical Relations for Monadic Types. | Jean Goubault-Larrecq, Slawomir Lasota, David Nowak |
| 2000 | CONCUR | A Unifying Approach to Data-Independence. | Ranko Lazic, David Nowak |
| 1999 | CONCUR | Synchronous Structures. | David Nowak, Jean-Pierre Talpin, Paul Le Guernic |
| 1997 | EuroPar | An ML-Like Module System for the Synchronous Language SIGNAL. | David Nowak, Jean-Pierre Talpin, Thierry Gautier, Paul Le Guernic |