| 2026 | FM | SeaCoral: A Collaborative Test Generation Toolset for Industrial Orchestration of Testing Tools. | Nicolas Berthier, Steven de Oliveira, Nikolai Kosmatov, Delphine Longuet |
| 2026 | FM | Formal Verification for Security Certification: From a First Success to Sustainable Industrial Usage. | Adel Djoudi, Nikolai Kosmatov |
| 2025 | FASE | Prove your Colorings: Formal Verification of Cache Coloring of Bao Hypervisor. | Axel Ferrol, Laurent Corbin, Nikolai Kosmatov |
| 2025 | IFM | Formal Verification of PKCS#1 Signature Parser Using Frama-C. | Martin Hna, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles |
| 2024 | FASE | Combining Deductive Verification with Shape Analysis. | To Bernier, Yani Ziani, Nikolai Kosmatov, Frdric Loulergue |
| 2024 | ISoLA | High-Level Program Properties in Frama-C: Definition, Verification and Deduction. | Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall |
| 2024 | TACAS | Automate where Automation Fails: Proof Strategies for Frama-C/WP. | Loc Correnson, Allan Blanchard, Adel Djoudi, Nikolai Kosmatov |
| 2024 | TAP | No Smoke Without Fire: Detecting Specification Inconsistencies with Frama-C/WP. | Allan Blanchard, Loc Correnson, Adel Djoudi, Nikolai Kosmatov |
| 2024 | TAP | Runtime Verification for High-Level Security Properties: Case Study on the TPM Software Stack. | Yani Ziani, Nikolai Kosmatov, Frdric Loulergue, Daniel Gracia Prez |
| 2023 | ESORICS | Execution at RISC: Stealth JOP Attacks on RISC-V Applications. | Loc Buckwell, Olivier Gilles, Daniel Gracia Prez, Nikolai Kosmatov |
| 2023 | IFM | Towards Formal Verification of a TPM Software Stack. | Yani Ziani, Nikolai Kosmatov, Frdric Loulergue, Daniel Gracia Prez, To Bernier |
| 2023 | SAC | An Efficient Black-Box Support of Advanced Coverage Criteria for Klee. | Nicolas Berthier, Steven de Oliveira, Nikolai Kosmatov, Delphine Longuet, Romain Soulat |
| 2022 | IFM | Certified Verification of Relational Properties. | Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall |
| 2022 | ISoLA | An Efficient VCGen-Based Modular Verification of Relational Properties. | Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall |
| 2022 | SAC | Verifying redundant-check based countermeasures: a case study. | Thibault Martin, Nikolai Kosmatov, Virgile Prevosto |
| 2021 | FM | Formal Verification of a JavaCard Virtual Machine with Frama-C. | Adel Djoudi, Martin Hna, Nikolai Kosmatov |
| 2021 | ICSE | Methodology for Specification and Verification of High-Level Requirements with MetAcsl. | Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall |
| 2021 | VMCAI | Runtime Abstract Interpretation for Numerical Accuracy and Robustness. | Franck Vdrine, Maxime Jacquemin, Nikolai Kosmatov, Julien Signoles |
| 2020 | IFM | Detection of Polluting Test Objectives for Dataflow Criteria. | Thibault Martin, Nikolai Kosmatov, Virgile Prevosto, Matthieu Lemerre |
| 2020 | ISoLA | Formal Verification of an Industrial Distributed Algorithm: An Experience Report. | Nikolai Kosmatov, Delphine Longuet, Romain Soulat |
| 2020 | RV | Efficient Runtime Assertion Checking for Properties over Mathematical Numbers. | Nikolai Kosmatov, Fonenantsoa Maurica, Julien Signoles |
| 2020 | TAP | Verified Runtime Assertion Checking for Memory Properties. | Dara Ly, Nikolai Kosmatov, Frdric Loulergue, Julien Signoles |
| 2019 | FASE | A Data Flow Model with Frequency Arithmetic. | Paul Dubrulle, Christophe Gaston, Nikolai Kosmatov, Arnault Lapitre, Stphane Louise |
| 2019 | IFM | Dynamic Reconfigurations in Frequency Constrained Data Flow. | Paul Dubrulle, Christophe Gaston, Nikolai Kosmatov, Arnault Lapitre |
| 2019 | SAC | Logic against ghosts: comparison of two proof approaches for a list module. | Allan Blanchard, Nikolai Kosmatov, Frdric Loulergue |
| 2019 | TACAS | MetAcsl: Specification and Verification of High-Level Properties. | Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall |
| 2019 | TAP | Tame Your Annotations with MetAcsl: Specifying, Testing and Proving High-Level Properties. | Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall |
| 2018 | EWSN | Towards Formal Verification of Contiki: Analysis of the AES-CCM* Modules with Frama-C. | Alexandre Peyrard, Nikolai Kosmatov, Simon Duquennoy, Shahid Raza |
| 2018 | FASE | Fast Computation of Arbitrary Control Dependencies. | Jean-Christophe Lchenet, Nikolai Kosmatov, Pascale Le Gall |
| 2018 | ICSE | Time to clean your test objectives. | Michal Marcozzi, Sbastien Bardin, Nikolai Kosmatov, Mike Papadakis, Virgile Prevosto, Loc Correnson |
| 2018 | ISoLA | Test Case Generation with PathCrawler/LTest: How to Automate an Industrial Testing Process. | Sbastien Bardin, Nikolai Kosmatov, Bruno Marre, David Mentr, Nicky Williams |
| 2018 | TAP | Static and Dynamic Verification of Relational Properties on Self-composed C Code. | Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto, Guillaume Petiot |
| 2018 | TAP | Ghosts for Lists: From Axiomatic to Executable Specifications. | Frdric Loulergue, Allan Blanchard, Nikolai Kosmatov |
| 2018 | TAP | Detection of Security Vulnerabilities in C Code Using Runtime Verification: An Experience Report. | Kostyantyn Vorobyov, Nikolai Kosmatov, Julien Signoles |
| 2017 | ICST | Taming Coverage Criteria Heterogeneity with LTest. | Michal Marcozzi, Sbastien Bardin, Mickal Delahaye, Nikolai Kosmatov, Virgile Prevosto |
| 2017 | ICST | Generic and Effective Specification of Structural Test Objectives. | Michal Marcozzi, Mickal Delahaye, Sbastien Bardin, Nikolai Kosmatov, Virgile Prevosto |
| 2017 | RV | E-ACSL, a Runtime Verification Tool for Safety and Security of C Programs (tool paper). | Julien Signoles, Nikolai Kosmatov, Kostyantyn Vorobyov |
| 2017 | RV | Runtime Detection of Temporal Memory Errors. | Kostyantyn Vorobyov, Nikolai Kosmatov, Julien Signoles, Arvid Jakobsson |
| 2017 | TACAS | RPP: Automatic Proof of Relational Properties by Self-composition. | Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto |
| 2016 | CRiSIS | Formal Verification of a Memory Allocation Module of Contiki with Frama-C: A Case Study. | Frdric Mangano, Simon Duquennoy, Nikolai Kosmatov |
| 2016 | FASE | Cut Branches Before Looking for Bugs: Sound Verification on Relaxed Slices. | Jean-Christophe Lchenet, Nikolai Kosmatov, Pascale Le Gall |
| 2016 | ISoLA | Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014. | Nikolai Kosmatov, Claude March, Yannick Moy, Julien Signoles |
| 2016 | ISSTA | A CHR-Based Solver for Weak Memory Behaviors. | Allan Blanchard, Nikolai Kosmatov, Frdric Loulergue |
| 2016 | RV | Frama-C, A Collaborative Framework for C Code Verification: Tutorial Synopsis. | Nikolai Kosmatov, Julien Signoles |
| 2016 | SCAM | Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs. | Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frdric Loulergue |
| 2016 | TAP | Your Proof Fails? Testing Helps to Find the Reason. | Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti, Jacques Julliand |
| 2015 | FMICS | A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C. | Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frdric Loulergue |
| 2015 | ICST | Sound and Quasi-Complete Detection of Infeasible Test Requirements. | Sbastien Bardin, Mickal Delahaye, Robin David, Nikolai Kosmatov, Mike Papadakis, Yves Le Traon, Jean-Yves Marion |
| 2015 | SAC | Fast as a shadow, expressive as a tree: hybrid memory monitoring for C. | Arvid Jakobsson, Nikolai Kosmatov, Julien Signoles |
| 2014 | ICST | Efficient Leveraging of Symbolic Execution to Advanced Coverage Criteria. | Sbastien Bardin, Nikolai Kosmatov, Franois Cheynier |
| 2014 | SCAM | Instrumentation of Annotated C Programs for Test Generation. | Guillaume Petiot, Bernard Botella, Jacques Julliand, Nikolai Kosmatov, Julien Signoles |
| 2014 | TAP | An All-in-One Toolkit for Automated White-Box Testing. | Sbastien Bardin, Omar Chebaro, Mickal Delahaye, Nikolai Kosmatov |
| 2014 | TAP | A Case Study on Verification of a Cloud Hypervisor by Proof and Structural Testing. | Nikolai Kosmatov, Matthieu Lemerre, Cline Alec |
| 2014 | TAP | Runtime Assertion Checking and Its Combinations with Static and Dynamic Analyses - Tutorial Synopsis. | Nikolai Kosmatov, Julien Signoles |
| 2014 | TAP | How Test Generation Helps Software Specification and Deductive Verification in Frama-C. | Guillaume Petiot, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand |
| 2013 | ICST | A Late Treatment of C Precondition in Dynamic Symbolic Execution. | Mickal Delahaye, Nikolai Kosmatov |
| 2013 | SAC | Common specification language for static and dynamic analysis of C programs. | Mickal Delahaye, Nikolai Kosmatov, Julien Signoles |
| 2013 | RV | A Late Treatment of C Precondition in Dynamic Symbolic Execution Testing Tools. | Mickal Delahaye, Nikolai Kosmatov |
| 2013 | RV | An Optimized Memory Monitoring for Runtime Assertion Checking of C Programs. | Nikolai Kosmatov, Guillaume Petiot, Julien Signoles |
| 2013 | RV | A Lesson on Runtime Assertion Checking with Frama-C. | Nikolai Kosmatov, Julien Signoles |
| 2013 | TAP | A Lesson on Proof of Programs with Frama-C. Invited Tutorial Paper. | Nikolai Kosmatov, Virgile Prevosto, Julien Signoles |
| 2012 | SAC | Program slicing enhances a verification technique combining static and dynamic analysis. | Omar Chebaro, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand |
| 2012 | SEFM | Frama-C - A Software Analysis Perspective. | Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, Boris Yakobowski |
| 2012 | TAP | Tutorial on Automated Structural Testing with PathCrawler - (Extended Abstract). | Nikolai Kosmatov, Nicky Williams |
| 2012 | TAP | A Lesson on Structural Testing with PathCrawler-online.com. | Nikolai Kosmatov, Nicky Williams, Bernard Botella, Muriel Roger, Omar Chebaro |
| 2011 | ICST | Online Test Generation with PathCrawler: Tool Demo. | Nikolai Kosmatov, Bernard Botella, Muriel Roger, Nicky Williams |
| 2011 | TAP | The SANTE Tool: Value Analysis, Program Slicing and Test Generation for C Program Debugging. | Omar Chebaro, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand |
| 2010 | TAP | Combining Static Analysis and Test Generation for C Program Debugging. | Omar Chebaro, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand |
| 2009 | ICSE | Automating Structural Testing of C Programs: Experience with PathCrawler. | Bernard Botella, Mickal Delahaye, Stphane Hong Tuan Ha, Nikolai Kosmatov, Patricia Mouy, Muriel Roger, Nicky Williams |
| 2008 | ISSRE | All-Paths TestGenerationfor Programs with Internal Aliases. | Nikolai Kosmatov |
| 2006 | SAC | A constraint solver for sequences and its applications. | Nikolai Kosmatov |
| 2004 | ISSRE | Boundary Coverage Criteria for Test Generation from Formal Models. | Nikolai Kosmatov, Bruno Legeard, Fabien Peureux, Mark Utting |