Nikolai Kosmatov

ORCID

Publication Activity (10 Years)

Years Active: 2004-2024
Publications (10 Years): 69

Top Venues

Publications

Dara Ly, Nikolai Kosmatov, Frédéric Loulergue, Julien Signoles
Sound Runtime Assertion Checking for Memory Properties via Program Transformation. Formal Aspects Comput. 36 (1) (2024)
Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall
An Efficient VCGen-based Modular Verification of Relational Properties. CoRR (2024)
Loïc Correnson, Allan Blanchard, Adel Djoudi, Nikolai Kosmatov
Automate where Automation Fails: Proof Strategies for Frama-C/WP. TACAS (1) (2024)
Téo Bernier, Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue
Combining Deductive Verification with Shape Analysis. FASE (2024)
Nicolas Berthier, Steven de Oliveira, Nikolai Kosmatov, Delphine Longuet, Romain Soulat
An Efficient Black-Box Support of Advanced Coverage Criteria for Klee. SAC (2023)
Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall
Efficient computation of arbitrary control dependencies. Theor. Comput. Sci. 969 (2023)
Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue, Daniel Gracia Pérez, Téo Bernier
Towards Formal Verification of a TPM Software Stack. iFM (2023)
Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue, Daniel Gracia Pérez, Téo Bernier
Towards Formal Verification of a TPM Software Stack. CoRR (2023)
Loïc Buckwell, Olivier Gilles, Daniel Gracia Pérez, Nikolai Kosmatov
Execution at RISC: Stealth JOP Attacks on RISC-V Applications. CoRR (2023)
Loïc Buckwell, Olivier Gilles, Daniel Gracia Pérez, Nikolai Kosmatov
Execution at RISC: Stealth JOP Attacks on RISC-V Applications. ESORICS Workshops (2) (2023)
Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall
Certified Verification of Relational Properties. IFM (2022)
Olivier Gilles, Franck Viguier, Nikolai Kosmatov, Daniel Gracia Pérez
Control-Flow Integrity at RISC: Attacking RISC-V by Jump-Oriented Programming. CoRR (2022)
Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall
An Efficient VCGen-Based Modular Verification of Relational Properties. ISoLA (1) (2022)
Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall
Certified Verification of Relational Properties. CoRR (2022)
Nicolas Berthier, Steven de Oliveira, Nikolai Kosmatov, Delphine Longuet, Romain Soulat
An Efficient Black-Box Support of Advanced Coverage Criteria for Klee. CoRR (2022)
Thibault Martin, Nikolai Kosmatov, Virgile Prevosto
Verifying redundant-check based countermeasures: a case study. SAC (2022)
Christophe Gaston, Nikolai Kosmatov, Pascale Le Gall
Editorial. Softw. Qual. J. 30 (1) (2022)
Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall
Methodology for Specification and Verification of High-Level Requirements with MetAcsl. FormaliSE@ICSE (2021)
Patrick Baudin, François Bobot, David Bühler, Loïc Correnson, Florent Kirchner, Nikolai Kosmatov, André Maroneze, Valentin Perrelle, Virgile Prevosto, Julien Signoles, Nicky Williams
The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. Commun. ACM 64 (8) (2021)
Franck Védrine, Maxime Jacquemin, Nikolai Kosmatov, Julien Signoles
Runtime Abstract Interpretation for Numerical Accuracy and Robustness. VMCAI (2021)
Adel Djoudi, Martin Hána, Nikolai Kosmatov
Formal Verification of a JavaCard Virtual Machine with Frama-C. FM (2021)
Sébastien Bardin, Nikolai Kosmatov, Michaël Marcozzi, Mickaël Delahaye
Specify and measure, cover and reveal: A unified framework for automated test generation. Sci. Comput. Program. 207 (2021)
Paul Dubrulle, Nikolai Kosmatov, Christophe Gaston, Arnault Lapitre
Correction to: PolyGraph: a data flow model with frequency arithmetic. Int. J. Softw. Tools Technol. Transf. 23 (3) (2021)
Paul Dubrulle, Nikolai Kosmatov, Christophe Gaston, Arnault Lapitre
PolyGraph: a data flow model with frequency arithmetic. Int. J. Softw. Tools Technol. Transf. 23 (3) (2021)
Thibault Martin, Nikolai Kosmatov, Virgile Prevosto, Matthieu Lemerre
Detection of Polluting Test Objectives for Dataflow Criteria. IFM (2020)
Dara Ly, Nikolai Kosmatov, Frédéric Loulergue, Julien Signoles
Verified Runtime Assertion Checking for Memory Properties. TAP@STAF (2020)
Nikolai Kosmatov, Fonenantsoa Maurica, Julien Signoles
Efficient Runtime Assertion Checking for Properties over Mathematical Numbers. RV (2020)
Nikolai Kosmatov, Delphine Longuet, Romain Soulat
Formal Verification of an Industrial Distributed Algorithm: An Experience Report. ISoLA (1) (2020)
Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov
Towards Full Proof Automation in Frama-C Using Auto-active Verification. NFM (2019)
Maxime Jacquemin, Fonenantsoa Maurica, Nikolai Kosmatov, Julien Signoles, Franck Védrine
Abstract Compilation for Verification of Numerical Accuracy Properties. CoRR (2019)
Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall
Tame Your Annotations with MetAcsl: Specifying, Testing and Proving High-Level Properties. TAP@FM (2019)
Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall
MetAcsl: Specification and Verification of High-Level Properties. TACAS (1) (2019)
Paul Dubrulle, Christophe Gaston, Nikolai Kosmatov, Arnault Lapitre
Dynamic Reconfigurations in Frequency Constrained Data Flow. IFM (2019)
Paul Dubrulle, Christophe Gaston, Nikolai Kosmatov, Arnault Lapitre, Stéphane Louise
A Data Flow Model with Frequency Arithmetic. FASE (2019)
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
Logic against ghosts: comparison of two proof approaches for a list module. SAC (2019)
Jasmin Blanchette, Francis Bordeleau, Alfonso Pierantonio, Nikolai Kosmatov, Gabriele Taentzer, Manuel Wimmer
Introduction to the STAF 2015 special section. Softw. Syst. Model. 18 (1) (2019)
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C. NFM (2018)
Alexandre Peyrard, Nikolai Kosmatov, Simon Duquennoy, Inria Lille, Shahid Raza
Towards Formal Verification of Contiki: Analysis of the AES-CCM* Modules with Frama-C. EWSN (2018)
Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto
Self-composition to Prove Relational Properties in Annotated C Program. CoRR (2018)
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
MMFilter : A CHR-Based Solver for Generation of Executions under Weak Memory Models. Comput. Lang. Syst. Struct. 53 (2018)
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
Tutorial: Secure Your Things: Secure Development of IoT Software with Frama-C. SecDev (2018)
Michaël Marcozzi, Sébastien Bardin, Nikolai Kosmatov, Mike Papadakis, Virgile Prevosto, Loïc Correnson
Time to clean your test objectives. ICSE (2018)
Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall
MetAcsl: Specification and Verification of High-Level Properties. CoRR (2018)
Sébastien Bardin, Nikolai Kosmatov, Bruno Marre, David Mentré, Nicky Williams
Test Case Generation with PathCrawler/LTest: How to Automate an Industrial Testing Process. ISoLA (4) (2018)
Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti, Jacques Julliand
How testing helps to diagnose proof failures. Formal Aspects Comput. 30 (6) (2018)
Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto, Guillaume Petiot
Static and Dynamic Verification of Relational Properties on Self-composed C Code. TAP@STAF (2018)
Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall
Cut branches before looking for bugs: certifiably sound verification on relaxed slices. Formal Aspects Comput. 30 (1) (2018)
Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall
Fast Computation of Arbitrary Control Dependencies. FASE (2018)
Frédéric Loulergue, Allan Blanchard, Nikolai Kosmatov
Ghosts for Lists: From Axiomatic to Executable Specifications. TAP@STAF (2018)
Kostyantyn Vorobyov, Nikolai Kosmatov, Julien Signoles
Detection of Security Vulnerabilities in C Code Using Runtime Verification: An Experience Report. TAP@STAF (2018)
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
A Lesson on Verification of IoT Software with Frama-C. HPCS (2018)
Michaël Marcozzi, Sébastien Bardin, Nikolai Kosmatov, Mike Papadakis, Virgile Prevosto, Loïc Correnson
Freeing Testers from Polluting Test Objectives. CoRR (2017)
Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov
From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation. VPT@ETAPS (2017)
Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto
RPP: Automatic Proof of Relational Properties by Self-composition. TACAS (1) (2017)
Kostyantyn Vorobyov, Nikolai Kosmatov, Julien Signoles, Arvid Jakobsson
Runtime Detection of Temporal Memory Errors. RV (2017)
Michaël Marcozzi, Sébastien Bardin, Mickaël Delahaye, Nikolai Kosmatov, Virgile Prevosto
Taming Coverage Criteria Heterogeneity with LTest. ICST (2017)
Julien Signoles, Nikolai Kosmatov, Kostyantyn Vorobyov
E-ACSL, a Runtime Verification Tool for Safety and Security of C Programs (tool paper). RV-CuBES (2017)
Michaël Marcozzi, Mickaël Delahaye, Sébastien Bardin, Nikolai Kosmatov, Virgile Prevosto
Generic and Effective Specification of Structural Test Objectives. ICST (2017)
Kostyantyn Vorobyov, Julien Signoles, Nikolai Kosmatov
Shadow state encoding for efficient monitoring of block-level properties. ISMM (2017)
Sébastien Bardin, Mickaël Delahaye, Nikolai Kosmatov, Michaël Marcozzi, Virgile Prevosto
Generic and Effective Specification of Structural Test Objectives. CoRR (2016)
Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall
Cut Branches Before Looking for Bugs: Sound Verification on Relaxed Slices. FASE (2016)
Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto
Deductive Verification with Relational Properties. CoRR (2016)
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
A CHR-Based Solver for Weak Memory Behaviors. CSTVA@ISSTA (2016)
Frédéric Mangano, Simon Duquennoy, Nikolai Kosmatov
Formal Verification of a Memory Allocation Module of Contiki with Frama-C: A Case Study. CRiSIS (2016)
Nikolai Kosmatov, Claude Marché, Yannick Moy, Julien Signoles
Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014. ISoLA (1) (2016)
Arvid Jakobsson, Nikolai Kosmatov, Julien Signoles
Fast as a shadow, expressive as a tree: Optimized memory monitoring for C. Sci. Comput. Program. 132 (2016)
Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti, Jacques Julliand
Your Proof Fails? Testing Helps to Find the Reason. TAP@STAF (2016)
Nikolai Kosmatov, Julien Signoles
Frama-C, A Collaborative Framework for C Code Verification: Tutorial Synopsis. RV (2016)
Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frédéric Loulergue
Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs. SCAM (2016)
Arvid Jakobsson, Nikolai Kosmatov, Julien Signoles
Fast as a shadow, expressive as a tree: hybrid memory monitoring for C. SAC (2015)
Sébastien Bardin, Mickaël Delahaye, Robin David, Nikolai Kosmatov, Mike Papadakis, Yves Le Traon, Jean-Yves Marion
Sound and Quasi-Complete Detection of Infeasible Test Requirements. ICST (2015)
Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, Boris Yakobowski
Frama-C: A software analysis perspective. Formal Aspects Comput. 27 (3) (2015)
Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti, Jacques Julliand
Your Proof Fails? Testing Helps to Find the Reason. CoRR (2015)
Balázs Kiss, Nikolai Kosmatov, Dillon Pariente, Armand Puccetti
Combining Static and Dynamic Analyses for Vulnerability Detection: Illustration on Heartbleed. Haifa Verification Conference (2015)
Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frédéric Loulergue
A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C. FMICS (2015)
Sébastien Bardin, Omar Chebaro, Mickaël Delahaye, Nikolai Kosmatov
An All-in-One Toolkit for Automated White-Box Testing. TAP@STAF (2014)
Omar Chebaro, Pascal Cuoq, Nikolai Kosmatov, Bruno Marre, Anne Pacalet, Nicky Williams, Boris Yakobowski
Behind the scenes in SANTE: a combination of static and dynamic analyses. Autom. Softw. Eng. 21 (1) (2014)
Nikolai Kosmatov, Matthieu Lemerre, Céline Alec
A Case Study on Verification of a Cloud Hypervisor by Proof and Structural Testing. TAP@STAF (2014)
Guillaume Petiot, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand
How Test Generation Helps Software Specification and Deductive Verification in Frama-C. TAP@STAF (2014)
Nikolai Kosmatov, Julien Signoles
Runtime Assertion Checking and Its Combinations with Static and Dynamic Analyses - Tutorial Synopsis. TAP@STAF (2014)
Guillaume Petiot, Bernard Botella, Jacques Julliand, Nikolai Kosmatov, Julien Signoles
Instrumentation of Annotated C Programs for Test Generation. SCAM (2014)
Sébastien Bardin, Nikolai Kosmatov, François Cheynier
Efficient Leveraging of Symbolic Execution to Advanced Coverage Criteria. ICST (2014)
Mickaël Delahaye, Nikolai Kosmatov
A Late Treatment of C Precondition in Dynamic Symbolic Execution. ICST Workshops (2013)
Nikolai Kosmatov, Guillaume Petiot, Julien Signoles
An Optimized Memory Monitoring for Runtime Assertion Checking of C Programs. RV (2013)
Sébastien Bardin, Nikolai Kosmatov, François Cheynier
Efficient Leverage of Symbolic ATG Tools to Advanced Coverage Criteria. CoRR (2013)
Nikolai Kosmatov, Nicky Williams, Bernard Botella, Muriel Roger
Structural Unit Testing as a Service with PathCrawler-online.com. SOSE (2013)
Mickaël Delahaye, Nikolai Kosmatov
A Late Treatment of C Precondition in Dynamic Symbolic Execution Testing Tools. RV (2013)
Mickaël Delahaye, Nikolai Kosmatov, Julien Signoles
Common specification language for static and dynamic analysis of C programs. SAC (2013)
Nikolai Kosmatov, Julien Signoles
A Lesson on Runtime Assertion Checking with Frama-C. RV (2013)
Nikolai Kosmatov, Virgile Prevosto, Julien Signoles
A Lesson on Proof of Programs with Frama-C. Invited Tutorial Paper. TAP@STAF (2013)
Omar Chebaro, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand
Program slicing enhances a verification technique combining static and dynamic analysis. SAC (2012)
Nikolai Kosmatov, Nicky Williams, Bernard Botella, Muriel Roger, Omar Chebaro
A Lesson on Structural Testing with PathCrawler-online.com. TAP@TOOLS (2012)
Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, Boris Yakobowski
Frama-C - A Software Analysis Perspective. SEFM (2012)
Nicky Williams, Nikolai Kosmatov
Structural Testing with PathCrawler: Tutorial Synopsis. QSIC (2012)
Nikolai Kosmatov, Nicky Williams
Tutorial on Automated Structural Testing with PathCrawler - (Extended Abstract). TAP@TOOLS (2012)
Frédéric Loulergue, Frédéric Gava, Nikolai Kosmatov, Matthieu Lemerre
Towards verified cloud computing environments. HPCS (2012)
Omar Chebaro, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand
The SANTE Tool: Value Analysis, Program Slicing and Test Generation for C Program Debugging. TAP@TOOLS (2011)
Nikolai Kosmatov, Bernard Botella, Muriel Roger, Nicky Williams
Online Test Generation with PathCrawler: Tool Demo. ICST Workshops (2011)
Omar Chebaro, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand
Combining Static Analysis and Test Generation for C Program Debugging. TAP@TOOLS (2010)
Bernard Botella, Mickaël Delahaye, Stéphane Hong Tuan Ha, Nikolai Kosmatov, Patricia Mouy, Muriel Roger, Nicky Williams
Automating Structural Testing of C Programs: Experience with PathCrawler. AST (2009)

Nikolai Kosmatov.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Nikolai Kosmatov