default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDNikolai Kosmatov
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
[j14]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): 4:1-4:46 (2024)- [c79]Téo Bernier, Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue:
Combining Deductive Verification with Shape Analysis. FASE 2024: 280-289 - [c78]Loïc Correnson, Allan Blanchard, Adel Djoudi, Nikolai Kosmatov:
Automate where Automation Fails: Proof Strategies for Frama-C/WP. TACAS (1) 2024: 331-339 - [c77]Allan Blanchard, Loïc Correnson, Adel Djoudi, Nikolai Kosmatov:
No Smoke Without Fire: Detecting Specification Inconsistencies with Frama-C/WP. TAP 2024: 65-83 - [c76]Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue, Daniel Gracia Pérez:
Runtime Verification for High-Level Security Properties: Case Study on the TPM Software Stack. TAP 2024: 87-106 - [i14]Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall:
An Efficient VCGen-based Modular Verification of Relational Properties. CoRR abs/2401.08385 (2024) - 2023
- [j13]Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall:
Efficient computation of arbitrary control dependencies. Theor. Comput. Sci. 969: 114029 (2023) - [c75]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: 377-391 - [c74]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: 93-112 - [c73]Nicolas Berthier, Steven de Oliveira, Nikolai Kosmatov, Delphine Longuet, Romain Soulat:
An Efficient Black-Box Support of Advanced Coverage Criteria for Klee. SAC 2023: 1706-1715 - [i13]Loïc Buckwell, Olivier Gilles, Daniel Gracia Pérez, Nikolai Kosmatov:
Execution at RISC: Stealth JOP Attacks on RISC-V Applications. CoRR abs/2307.12648 (2023) - [i12]Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue, Daniel Gracia Pérez, Téo Bernier:
Towards Formal Verification of a TPM Software Stack. CoRR abs/2307.16821 (2023) - 2022
- [j12]Christophe Gaston, Nikolai Kosmatov, Pascale Le Gall:
Editorial. Softw. Qual. J. 30(1): 1-2 (2022) - [c72]Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall:
Certified Verification of Relational Properties. IFM 2022: 86-105 - [c71]Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall:
An Efficient VCGen-Based Modular Verification of Relational Properties. ISoLA (1) 2022: 498-516 - [c70]Thibault Martin, Nikolai Kosmatov, Virgile Prevosto:
Verifying redundant-check based countermeasures: a case study. SAC 2022: 1849-1852 - [i11]Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall:
Certified Verification of Relational Properties. CoRR abs/2202.10349 (2022) - [i10]Nicolas Berthier, Steven de Oliveira, Nikolai Kosmatov, Delphine Longuet, Romain Soulat:
An Efficient Black-Box Support of Advanced Coverage Criteria for Klee. CoRR abs/2211.14592 (2022) - [i9]Olivier Gilles, Franck Viguier, Nikolai Kosmatov, Daniel Gracia Pérez:
Control-Flow Integrity at RISC: Attacking RISC-V by Jump-Oriented Programming. CoRR abs/2211.16212 (2022) - 2021
- [j11]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): 56-68 (2021) - [j10]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: 102641 (2021) - [j9]Paul Dubrulle, Nikolai Kosmatov, Christophe Gaston, Arnault Lapitre:
PolyGraph: a data flow model with frequency arithmetic. Int. J. Softw. Tools Technol. Transf. 23(3): 489-517 (2021) - [j8]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): 519 (2021) - [c69]Adel Djoudi, Martin Hána, Nikolai Kosmatov:
Formal Verification of a JavaCard Virtual Machine with Frama-C. FM 2021: 427-444 - [c68]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: 54-67 - [c67]Franck Védrine, Maxime Jacquemin, Nikolai Kosmatov, Julien Signoles:
Runtime Abstract Interpretation for Numerical Accuracy and Robustness. VMCAI 2021: 243-266 - 2020
- [c66]Thibault Martin, Nikolai Kosmatov, Virgile Prevosto, Matthieu Lemerre:
Detection of Polluting Test Objectives for Dataflow Criteria. IFM 2020: 337-345 - [c65]Nikolai Kosmatov, Delphine Longuet, Romain Soulat:
Formal Verification of an Industrial Distributed Algorithm: An Experience Report. ISoLA (1) 2020: 525-542 - [c64]Nikolai Kosmatov, Fonenantsoa Maurica, Julien Signoles:
Efficient Runtime Assertion Checking for Properties over Mathematical Numbers. RV 2020: 310-322 - [c63]Dara Ly, Nikolai Kosmatov, Frédéric Loulergue, Julien Signoles:
Verified Runtime Assertion Checking for Memory Properties. TAP@STAF 2020: 100-121
2010 – 2019
- 2019
- [j7]Jasmin Blanchette, Francis Bordeleau, Alfonso Pierantonio, Nikolai Kosmatov, Gabriele Taentzer, Manuel Wimmer:
Introduction to the STAF 2015 special section. Softw. Syst. Model. 18(1): 191-193 (2019) - [c62]Paul Dubrulle, Christophe Gaston, Nikolai Kosmatov, Arnault Lapitre, Stéphane Louise:
A Data Flow Model with Frequency Arithmetic. FASE 2019: 369-385 - [c61]Paul Dubrulle, Christophe Gaston, Nikolai Kosmatov, Arnault Lapitre:
Dynamic Reconfigurations in Frequency Constrained Data Flow. IFM 2019: 175-193 - [c60]Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov:
Towards Full Proof Automation in Frama-C Using Auto-active Verification. NFM 2019: 88-105 - [c59]Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue:
Logic against ghosts: comparison of two proof approaches for a list module. SAC 2019: 2186-2195 - [c58]Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall:
MetAcsl: Specification and Verification of High-Level Properties. TACAS (1) 2019: 358-364 - [c57]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: 167-185 - [e2]Christophe Gaston, Nikolai Kosmatov, Pascale Le Gall:
Testing Software and Systems - 31st IFIP WG 6.1 International Conference, ICTSS 2019, Paris, France, October 15-17, 2019, Proceedings. Lecture Notes in Computer Science 11812, Springer 2019, ISBN 978-3-030-31279-4 [contents] - [i8]Maxime Jacquemin, Fonenantsoa Maurica, Nikolai Kosmatov, Julien Signoles, Franck Védrine:
Abstract Compilation for Verification of Numerical Accuracy Properties. CoRR abs/1911.10930 (2019) - 2018
- [j6]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: 121-142 (2018) - [j5]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): 107-131 (2018) - [j4]Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti, Jacques Julliand:
How testing helps to diagnose proof failures. Formal Aspects Comput. 30(6): 629-657 (2018) - [c56]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: 264-269 - [c55]Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall:
Fast Computation of Arbitrary Control Dependencies. FASE 2018: 207-224 - [c54]Michaël Marcozzi, Sébastien Bardin, Nikolai Kosmatov, Mike Papadakis, Virgile Prevosto, Loïc Correnson:
Time to clean your test objectives. ICSE 2018: 456-467 - [c53]Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue:
A Lesson on Verification of IoT Software with Frama-C. HPCS 2018: 21-30 - [c52]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: 104-120 - [c51]Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue:
Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C. NFM 2018: 37-53 - [c50]Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue:
Tutorial: Secure Your Things: Secure Development of IoT Software with Frama-C. SecDev 2018: 126-127 - [c49]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: 44-62 - [c48]Kostyantyn Vorobyov, Nikolai Kosmatov, Julien Signoles:
Detection of Security Vulnerabilities in C Code Using Runtime Verification: An Experience Report. TAP@STAF 2018: 139-156 - [c47]Frédéric Loulergue, Allan Blanchard, Nikolai Kosmatov:
Ghosts for Lists: From Axiomatic to Executable Specifications. TAP@STAF 2018: 177-184 - [i7]Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto:
Self-composition to Prove Relational Properties in Annotated C Program. CoRR abs/1801.06876 (2018) - [i6]Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall:
MetAcsl: Specification and Verification of High-Level Properties. CoRR abs/1811.10509 (2018) - 2017
- [c46]Michaël Marcozzi, Mickaël Delahaye, Sébastien Bardin, Nikolai Kosmatov, Virgile Prevosto:
Generic and Effective Specification of Structural Test Objectives. ICST 2017: 436-441 - [c45]Michaël Marcozzi, Sébastien Bardin, Mickaël Delahaye, Nikolai Kosmatov, Virgile Prevosto:
Taming Coverage Criteria Heterogeneity with LTest. ICST 2017: 500-507 - [c44]Kostyantyn Vorobyov, Julien Signoles, Nikolai Kosmatov:
Shadow state encoding for efficient monitoring of block-level properties. ISMM 2017: 47-58 - [c43]Julien Signoles, Nikolai Kosmatov, Kostyantyn Vorobyov:
E-ACSL, a Runtime Verification Tool for Safety and Security of C Programs (tool paper). RV-CuBES 2017: 164-173 - [c42]Kostyantyn Vorobyov, Nikolai Kosmatov, Julien Signoles, Arvid Jakobsson:
Runtime Detection of Temporal Memory Errors. RV 2017: 294-311 - [c41]Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto:
RPP: Automatic Proof of Relational Properties by Self-composition. TACAS (1) 2017: 391-397 - [c40]Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov:
From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation. VPT@ETAPS 2017: 109-123 - [i5]Michaël Marcozzi, Sébastien Bardin, Nikolai Kosmatov, Mike Papadakis, Virgile Prevosto, Loïc Correnson:
Freeing Testers from Polluting Test Objectives. CoRR abs/1708.08765 (2017) - 2016
- [j3]Arvid Jakobsson, Nikolai Kosmatov, Julien Signoles:
Fast as a shadow, expressive as a tree: Optimized memory monitoring for C. Sci. Comput. Program. 132: 226-246 (2016) - [c39]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: 114-120 - [c38]Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall:
Cut Branches Before Looking for Bugs: Sound Verification on Relaxed Slices. FASE 2016: 179-196 - [c37]Nikolai Kosmatov, Claude Marché, Yannick Moy, Julien Signoles:
Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014. ISoLA (1) 2016: 461-478 - [c36]Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue:
A CHR-Based Solver for Weak Memory Behaviors. CSTVA@ISSTA 2016: 15-22 - [c35]Nikolai Kosmatov, Julien Signoles:
Frama-C, A Collaborative Framework for C Code Verification: Tutorial Synopsis. RV 2016: 92-115 - [c34]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: 67-72 - [c33]Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti, Jacques Julliand:
Your Proof Fails? Testing Helps to Find the Reason. TAP@STAF 2016: 130-150 - [i4]Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto:
Deductive Verification with Relational Properties. CoRR abs/1606.00678 (2016) - [i3]Sébastien Bardin, Mickaël Delahaye, Nikolai Kosmatov, Michaël Marcozzi, Virgile Prevosto:
Generic and Effective Specification of Structural Test Objectives. CoRR abs/1609.01204 (2016) - 2015
- [j2]Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, Boris Yakobowski:
Frama-C: A software analysis perspective. Formal Aspects Comput. 27(3): 573-609 (2015) - [c32]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: 15-30 - [c31]Balázs Kiss, Nikolai Kosmatov, Dillon Pariente, Armand Puccetti:
Combining Static and Dynamic Analyses for Vulnerability Detection: Illustration on Heartbleed. Haifa Verification Conference 2015: 39-50 - [c30]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: 1-10 - [c29]Arvid Jakobsson, Nikolai Kosmatov, Julien Signoles:
Fast as a shadow, expressive as a tree: hybrid memory monitoring for C. SAC 2015: 1765-1772 - [e1]Jasmin Christian Blanchette, Nikolai Kosmatov:
Tests and Proofs - 9th International Conference, TAP@STAF 2015, L'Aquila, Italy, July 22-24, 2015. Proceedings. Lecture Notes in Computer Science 9154, Springer 2015, ISBN 978-3-319-21214-2 [contents] - [i2]Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti, Jacques Julliand:
Your Proof Fails? Testing Helps to Find the Reason. CoRR abs/1508.01691 (2015) - 2014
- [j1]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): 107-143 (2014) - [c28]Sébastien Bardin, Nikolai Kosmatov, François Cheynier:
Efficient Leveraging of Symbolic Execution to Advanced Coverage Criteria. ICST 2014: 173-182 - [c27]Guillaume Petiot, Bernard Botella, Jacques Julliand, Nikolai Kosmatov, Julien Signoles:
Instrumentation of Annotated C Programs for Test Generation. SCAM 2014: 105-114 - [c26]Sébastien Bardin, Omar Chebaro, Mickaël Delahaye, Nikolai Kosmatov:
An All-in-One Toolkit for Automated White-Box Testing. TAP@STAF 2014: 53-60 - [c25]Nikolai Kosmatov, Matthieu Lemerre, Céline Alec:
A Case Study on Verification of a Cloud Hypervisor by Proof and Structural Testing. TAP@STAF 2014: 158-164 - [c24]Nikolai Kosmatov, Julien Signoles:
Runtime Assertion Checking and Its Combinations with Static and Dynamic Analyses - Tutorial Synopsis. TAP@STAF 2014: 165-168 - [c23]Guillaume Petiot, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand:
How Test Generation Helps Software Specification and Deductive Verification in Frama-C. TAP@STAF 2014: 204-211 - 2013
- [c22]Mickaël Delahaye, Nikolai Kosmatov:
A Late Treatment of C Precondition in Dynamic Symbolic Execution. ICST Workshops 2013: 230-231 - [c21]Nikolai Kosmatov, Guillaume Petiot, Julien Signoles:
An Optimized Memory Monitoring for Runtime Assertion Checking of C Programs. RV 2013: 167-182 - [c20]Mickaël Delahaye, Nikolai Kosmatov:
A Late Treatment of C Precondition in Dynamic Symbolic Execution Testing Tools. RV 2013: 328-333 - [c19]Nikolai Kosmatov, Julien Signoles:
A Lesson on Runtime Assertion Checking with Frama-C. RV 2013: 386-399 - [c18]Mickaël Delahaye, Nikolai Kosmatov, Julien Signoles:
Common specification language for static and dynamic analysis of C programs. SAC 2013: 1230-1235 - [c17]Nikolai Kosmatov, Nicky Williams, Bernard Botella, Muriel Roger:
Structural Unit Testing as a Service with PathCrawler-online.com. SOSE 2013: 435-440 - [c16]Nikolai Kosmatov, Virgile Prevosto, Julien Signoles:
A Lesson on Proof of Programs with Frama-C. Invited Tutorial Paper. TAP@STAF 2013: 168-177 - [i1]Sébastien Bardin, Nikolai Kosmatov, François Cheynier:
Efficient Leverage of Symbolic ATG Tools to Advanced Coverage Criteria. CoRR abs/1308.4045 (2013) - 2012
- [c15]Frédéric Loulergue, Frédéric Gava, Nikolai Kosmatov, Matthieu Lemerre:
Towards verified cloud computing environments. HPCS 2012: 91-97 - [c14]Nicky Williams, Nikolai Kosmatov:
Structural Testing with PathCrawler: Tutorial Synopsis. QSIC 2012: 289-292 - [c13]Omar Chebaro, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand:
Program slicing enhances a verification technique combining static and dynamic analysis. SAC 2012: 1284-1291 - [c12]Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, Boris Yakobowski:
Frama-C - A Software Analysis Perspective. SEFM 2012: 233-247 - [c11]Nikolai Kosmatov, Nicky Williams, Bernard Botella, Muriel Roger, Omar Chebaro:
A Lesson on Structural Testing with PathCrawler-online.com. TAP@TOOLS 2012: 169-175 - [c10]Nikolai Kosmatov, Nicky Williams:
Tutorial on Automated Structural Testing with PathCrawler - (Extended Abstract). TAP@TOOLS 2012: 176 - 2011
- [c9]Nikolai Kosmatov, Bernard Botella, Muriel Roger, Nicky Williams:
Online Test Generation with PathCrawler: Tool Demo. ICST Workshops 2011: 316-317 - [c8]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: 78-83 - 2010
- [c7]Omar Chebaro, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand:
Combining Static Analysis and Test Generation for C Program Debugging. TAP@TOOLS 2010: 94-100
2000 – 2009
- 2009
- [c6]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: 70-78 - 2008
- [c5]Nikolai Kosmatov:
All-Paths TestGenerationfor Programs with Internal Aliases. ISSRE 2008: 147-156 - 2006
- [c4]Nikolai Kosmatov:
A constraint solver for sequences and its applications. SAC 2006: 404-408 - 2005
- [c3]Nikolai Kosmatov:
Constraint Solving for Sequences in Software Validation and Verification. INAP 2005: 25-37 - [c2]Jean-François Couchot, Alain Giorgetti, Nikolai Kosmatov:
A uniform deductive approach for parameterized protocol safety. ASE 2005: 364-367 - 2004
- [c1]Nikolai Kosmatov, Bruno Legeard, Fabien Peureux, Mark Utting:
Boundary Coverage Criteria for Test Generation from Formal Models. ISSRE 2004: 139-150
Coauthor Index