Back to the main page

Patents:
    2021:

  1. Nikolai Kosmatov, Virgile Prevosto and Thibault Martin.
    Method and system for verification of redundant-check countermeasures.
    Patent application. Submitted on August 20, 2021 to European Patent Office. [pdf]

    2. 2018:

  2. Paul Dubrulle, Stéphane Louise, Christophe Gaston, Mathieu Jan, Nikolai Kosmatov, and Arnault Lapitre.
    Outil et procédé de conception et de validation d'un système flots de données par un modèle formel. (Tool and method for design and validation of a data flow system by a formal model).
    Patent application. In French. Submitted on August 31, 2018 to INPI (French Patent Office). [pdf]

    3. 2016:

  3. Kostyantyn Vorobyov, Nikolai Kosmatov, and Julien Signoles.
    A computer-implemented method and a system for encoding a heap application memory state using shadow memory.
    Patent application. Submitted on September 27, 2016 to European Patent Office. Submitted on September 15, 2017 to US Patent Office. [pdf]

  4. Kostyantyn Vorobyov, Nikolai Kosmatov, and Julien Signoles.
    A computer-implemented method and a system for encoding a stack application memory state using shadow memory.
    Patent application. Submitted on December 7, 2016 to European Patent Office. Submitted on November 29, 2017 to US Patent Office. [pdf]


Publications:

In Computer Science:
    2024:

  1. Nicky Williams and Nikolai Kosmatov.
    Test Generation with PathCrawler.
    Chapter 6 in Nikolai Kosmatov, Virgile Prevosto, Julien Signoles (Eds),
    Guide to Software Verification with Frama-C. Core Components, Usages, and Applications.
    Computer Science Foundations and Applied Logic Book Series.
    pages 305-338. Springer, 2024. ISBN 978-3-031-55607-4.
    DOI 10.1007/978-3-031-55608-1_6

  2. Nikolai Kosmatov, Artjom Plaunov, Subash Shankar and Julien Signoles .
    Combining Analyses Within Frama-C.
    Chapter 9 in Nikolai Kosmatov, Virgile Prevosto, Julien Signoles (Eds),
    Guide to Software Verification with Frama-C. Core Components, Usages, and Applications.
    Computer Science Foundations and Applied Logic Book Series.
    pages 423-455. Springer, 2024. ISBN 978-3-031-55607-4.
    DOI 10.1007/978-3-031-55608-1_9

  3. Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto and Virgile Robles.
    Specification and Verification of High-Level Properties.
    Chapter 10 in Nikolai Kosmatov, Virgile Prevosto, Julien Signoles (Eds),
    Guide to Software Verification with Frama-C. Core Components, Usages, and Applications.
    Computer Science Foundations and Applied Logic Book Series.
    pages 457-486. Springer, 2024. ISBN 978-3-031-55607-4.
    DOI 10.1007/978-3-031-55608-1_10

  4. Adel Djoudi, Martin Hána and Nikolai Kosmatov.
    Proof of Security Properties: Application to JavaCard Virtual Machine.
    Chapter 16 in Nikolai Kosmatov, Virgile Prevosto, Julien Signoles (Eds),
    Guide to Software Verification with Frama-C. Core Components, Usages, and Applications.
    Computer Science Foundations and Applied Logic Book Series.
    pages 659-683. Springer, 2024. ISBN 978-3-031-55607-4.
    DOI 10.1007/978-3-031-55608-1_16

  5. Téo Biton, Olivier Gilles, Daniel Gracia Pérez, Nikolai Kosmatov and Sébastien Pillement.
    Call Rewinding: Efficient Backward Edge Protection.
    In IACR Trans. Cryptogr. Hardw. Embed. Syst., vol. 2025, No 1, pages 227-250. 2024.
    [pdf] This is the authors' final version of the work. DOI: 10.46586/tches.v2025.i1.227-250.

  6. Dara Ly, Nikolai Kosmatov, Frédéric Loulergue, and Julien Signoles.
    Sound Runtime Assertion Checking for Memory Properties via Program Transformation.
    In Formal Aspects of Computing Journal, vol. 4, issue 1, pages 4:1-4:46. 2024. ACM.
    [pdf] This is the authors' final version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in FAC 2024, DOI: 10.1145/3605951.

  7. Grégoire Boussu, Nikolai Kosmatov and Franck Védrine.
    A Case Study on Numerical Analysis of a Path Computation Algorithm.
    In Proc. of the 6th International Workshop on Formal Methods for Autonomous Systems (FMAS 2024),
    co-located with the 19th International Conference on integrated Formal Methods (iFM 2024),
    Manchester, UK, November 2024, EPTCS, vol. 411, pages 123-142.
    [pdf] This is the authors' final version of the work. DOI: 10.4204/EPTCS.411.8.

  8. Virgile Robles, Nikolai Kosmatov, Virgile Prevosto and Pascale Le Gall.
    High-Level Program Properties in Frama-C: Definition, Verification and Deduction.
    In Proc. of the 12th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2024),
    Crete, Greece, October 2024, LNCS, vol. 15221, pages 159-177. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-031-75380-0_10.

  9. Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue, and Daniel Gracia Pérez.
    Runtime Verification for High-Level Security Properties: Case Study on the TPM Software Stack.
    In Proc. of the 18th International Conference on Tests & Proofs (TAP 2024),
    co-located with the 26th International Symposium on Formal Methods (FM 2024),
    Milan, Italy, September 2024, pages 87-106. LNCS, vol. 15153. Springer.
    [pdf] [slides] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-031-72044-4_5.

  10. Allan Blanchard, Loïc Correnson, Adel Djoudi and Nikolai Kosmatov.
    No Smoke without Fire: Detecting Specification Inconsistencies with Frama-C/WP.
    In Proc. of the 18th International Conference on Tests & Proofs (TAP 2024),
    co-located with the 26th International Symposium on Formal Methods (FM 2024),
    Milan, Italy, September 2024, pages 65-83. LNCS, vol. 15153. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-031-72044-4_4.

  11. Loïc Correnson, Allan Blanchard, Adel Djoudi and Nikolai Kosmatov.
    Automate where Automation Fails: Proof Strategies for Frama-C/WP.
    In Proc. of the 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2024),
    Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2024),
    Luxembourg City, Luxembourg, Apr 2024, pages 331-339. LNCS, vol. 14570. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-031-57246-3_18.

  12. Téo Bernier, Yani Ziani, Nikolai Kosmatov and Frédéric Loulergue.
    Combining Deductive Verification with Shape Analysis.
    In Proc. of the 27th International Conference on Fundamental Approaches to Software Engineering (FASE 2024),
    Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2024),
    Luxembourg City, Luxembourg, Apr 2024, pages 280-289. LNCS, vol. 14573. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-031-57259-3_14.

    13. 2023:

  13. Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall.
    Efficient Computation of Arbitrary Control Dependencies.
    In Theor. Comput. Sci., vol. 969, 2023.
    [pdf] This is the authors' final version of the work. DOI: https://doi.org/10.1016/j.tcs.2023.114029.

  14. Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue, Daniel Gracia Pérez and Téo Bernier.
    Towards Formal Verification of a TPM Software Stack.
    In Proc. of the 18th International Conference on integrated Formal Methods (iFM 2023),
    Leiden, the Netherlands, Nov 2023, pages 93-112. LNCS, vol. 14300. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-031-47705-8_6.

  15. Loïc Buckwell, Olivier Gilles, Daniel Gracia Pérez and Nikolai Kosmatov.
    Execution at RISC: Stealth JOP Attacks on RISC-V Applications.
    In Proc. of the Workshop on Attacks and Software Protection (WASP 2023), co-located with the 28th European Symposium on Research in Computer Security (ESORICS 2023),
    The Hague, the Netherlands, Sept 2023, pages 377-391. LNCS, vol. 14399. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-031-54129-2_22.

  16. Nicolas Berthier, Steven de Oliveira, Nikolai Kosmatov, Delphine Longuet and Romain Soulat.
    An Efficient Black-Box Support of Advanced Coverage Criteria for Klee.
    In Proc. of the 38th ACM/SIGAPP Symposium On Applied Computing, Software Verification and Testing Track (SAC-SVT 2023),
    Tallinn, Estonia, March 2023, pages 1706-1715. ACM.
    [pdf] This is the authors' final version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in SAC 2023, DOI: 10.1145/3555776.3577713.

    17. 2022:

  17. Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto and Pascale Le Gall.
    An Efficient VCGen-based Modular Verification of Relational Properties.
    In Proc. of the 11th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2022),
    Rhodes, Greece, October 2022, LNCS, vol. 13701, pages 498-516. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-031-19849-6_28.

  18. Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto and Pascale Le Gall.
    Certified Verification of Relational Properties.
    In Proc. of the 17th International Conference on integrated Formal Methods (iFM 2022),
    Lugano, Switzerland, June 2022, pages 86-105. LNCS, vol. 13274. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-031-07727-2_6.

  19. Adel Djoudi, Martin Hána, Nikolai Kosmatov, Milan Kříženecký, Franck Ohayon, Patricia Mouy, Arnaud Fontaine and David Féliot.
    A Bottom-Up Formal Verification Approach for Common Criteria Certification: Application to JavaCard Virtual Machine.
    Best paper award (category "Processes, Methods and Tools"). [award]
    In Proc. of the 11th European Congress on Embedded Real-Time Systems (ERTS 2022),
    Toulouse, Juin 1-2, 2022.
    [pdf]

  20. Thibault Martin, Nikolai Kosmatov and Virgile Prevosto.
    Verifying Redundant-Check Based Countermeasures: A Case Study.
    In Proc. of the 37th ACM/SIGAPP Symposium On Applied Computing, Software Verification and Testing Track (SAC-SVT 2022),
    Online, April 2022, pages 1849-1852. ACM. ISBN 78-1-4503-8713-2/22/04.
    [pdf] This is the authors' final version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in SAC 2022, DOI: 10.1145/3477314.3507341.

    21. 2021:

  21. Patrick Baudin, François Bobot, David Bühler, Loïc Correnson, Florent Kirchner, Nikolai Kosmatov, André Maroneze, Valentin Perrelle, Virgile Prevosto, Julien Signoles, and Nicky Williams.
    The Dogged Pursuit of Bug-Free C Programs: The Frama-C Software Analysis Platform.
    In Communications of the ACM,
    2021, vol. 64, pages 56-68. ACM. ISSN: 0001-0782.
    [pdf] This is the authors' final version of the work. The final publication is available here. DOI: 10.1145/3470569.

  22. Sébastien Bardin, Nikolai Kosmatov, Michaël Marcozzi, and Mickaël Delahaye.
    Specify and Measure, Cover and Reveal: A Unified Framework for Automated Test Generation.
    In Science of Computer Programming,
    2021, vol. 207, ISSN 0167-6423.
    [pdf] This is the authors' final version of the work. The final publication was published in Sci. Comput. Program., DOI: 10.1016/j.scico.2021.102641.

  23. Paul Dubrulle, Christophe Gaston, Nikolai Kosmatov, and Arnault Lapitre.
    Polygraph: A Data Flow Model with Frequency Arithmetic.
    In International Journal on Software Tools for Technology Transfer (STTT),
    2020, vol. 23, num. 3, pages 489-517. Springer. ISSN: 1433-2779.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/s10009-020-00586-9.

  24. Adel Djoudi, Martin Hána and Nikolai Kosmatov.
    Formal verification of a JavaCard virtual machine with Frama-C.
    In Proc. of the 24rd International Symposium on Formal Methods (FM 2021),
    Online, November 2021, pages 427-444. LNCS, vol. 13047. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-030-90870-6_23.

  25. Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, and Pascale Le Gall.
    Methodology for Specification and Verifiation of High-Level Properties with MetAcsl.
    In Proc. of the 9th IEEE/ACM International Conference on Formal Methods in Software Engineering (FormaliSE 2021),
    Online, May 2021, pages 54-67. IEEE.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/FormaliSE52586.2021.00012.

  26. Franck Védrine, Maxime Jacquemin, Nikolai Kosmatov and Julien Signoles.
    Detection of Polluting Test Objectives for Dataflow Criteria Runtime Abstract Interpretation for Numerical Accuracy and Robustness.
    In Proc. of the 22nd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2021),
    Online, January 2021, pages 243-266. LNCS, vol. 12597. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-030-67067-2_12.

    27. 2020:

  27. Thibault Martin, Nikolai Kosmatov, Virgile Prevosto and Matthieu Lemerre.
    Detection of Polluting Test Objectives for Dataflow Criteria.
    In Proc. of the 16th International Conference on integrated Formal Methods (iFM 2020)
    Lugano, Switzerland, November 2020, pages 337-345. LNCS, vol. 12546. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-030-63461-2_18.

  28. Nikolai Kosmatov, Delphine Longuet, Romain Soulat.
    Formal Verification of an Industrial Distributed Algorithm: an Experience Report.
    In Proc. of the 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2020),
    Rhodes, Greece, October 2020, LNCS, vol. 12476, pages 525-542. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-030-61362-4_30.

  29. Nikolai Kosmatov, Fonenantsoa Maurica, Julien Signoles.
    Efficient Runtime Assertion Checking of Properties over Mathematical Numbers.
    In Proc. of the 20th International Conference on Runtime Verification (RV 2020),
    Los Angeles, USA, October 2020, LNCS, vol. 12399, pages 310-322. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-030-60508-7_17.

  30. Dara Ly, Nikolai Kosmatov, Frédéric Loulergue, and Julien Signoles.
    Verified Runtime Assertion Checking for Memory Properties.
    In Proc. of the 14th International Conference on Tests & Proofs (TAP 2020),
    part of the Software Technologies: Applications and Foundations conference (STAF 2020),
    Bergen, Norway, June 2020, pages 100-121. LNCS, vol. 12165. Springer. ISBN 978-3-030-50995-8.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-030-50995-8_6.

    31. 2019:

  31. Paul Dubrulle, Christophe Gaston, Nikolai Kosmatov, and Arnault Lapitre.
    Dynamic Reconfigurations in Frequency Constrained Data Flow.
    In Proc. of the 15th International Conference on integrated Formal Methods (iFM 2019)
    Bergen, Norway, December 2019, pages 175-193. LNCS, vol. 11918. Springer. ISBN 978-3-030-34967-7.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-030-34968-4.

  32. Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, and Pascale Le Gall.
    Tame your annotations with MetAcsl: Specifying, Testing and Proving High-Level Properties.
    In Proc. of the 13th International Conference on Tests & Proofs (TAP 2019),
    part of the Third World Congress on Formal Methods (FM 2019),
    Porto, Portugal, October 2019, pages 167-185. LNCS, vol. 11823. Springer. ISBN 978-3-030-31156-8.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-030-31157-5_11

  33. Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov.
    Towards Full Proof Automation in Frama-C using Auto-Active Verification.
    In Proc. of the 11th NASA Formal Methods Symposium (NFM 2019),
    Houston, TX, USA, May 2019, LNCS, vol. 11460, pages 88-105. Springer. ISBN 978-3-030-20651-2.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-030-20652-9_6.

  34. Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue.
    Logic against Ghosts: Comparison of two Proof Approaches for a List Module.
    Best Software Development paper award. [award]
    In Proc. of the 34th ACM/SIGAPP Symposium On Applied Computing, Software Verification and Testing Track (SAC-SVT 2019),
    Limassol, Cyprus, April 2019, pages 2186-2195. ACM. ISBN 978-1-4503-5933-7.
    [pdf] This is the authors' final version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in SAC 2019, DOI: 10.1145/3297280.3297495.

  35. Paul Dubrulle, Christophe Gaston, Nikolai Kosmatov, Arnault Lapitre, and Stéphane Louise.
    A Data Flow Model with Frequency Arithmetic.
    In Proc. of the 22nd International Conference on Fundamental Approaches to Software Engineering (FASE 2019)
    part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2019),
    Prague, Czech Republic, April 2019, pages 369-385. LNCS, vol. 11424. Springer. ISBN 978-3-030-16721-9.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-030-16722-6_22.

  36. Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, and Pascale Le Gall.
    MetAcsl: Specification and Verification of High-Level Properties.
    In Proc. of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019),
    part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2019),
    Prague, Czech Republic, April 2019, pages 358-364. LNCS, vol. 11427. Springer. ISBN 978-3-030-17461-3.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-030-17462-0_22.

    37. 2018:

  37. Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue.
    MMFilter: A CHR-based solver for generation of executions under weak memory models.
    In Computer Languages, Systems and Structures, vol. 53, pages 121-142. Elsevier.
    [pdf] This is the authors' final version of the work. DOI: https://doi.org/10.1016/j.cl.2018.03.002.

  38. Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti, Jacques Julliand.
    How Testing Helps to Diagnose Proof Failures.
    In Formal Aspects of Computing Journal, vol. 30, issue 6, pages 629-657. 2018. Springer..
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/s00165-018-0456-4.

  39. Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall.
    Cut Branches Before Looking for Bugs: Certifiably Sound Verification on Relaxed Slices.
    In Formal Aspects of Computing Journal, vol. 30, issue 1, pages 107-131. 2018. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/s00165-017-0439-x

  40. Dara Ly, Nikolai Kosmatov, Julien Signoles, Frédéric Loulergue.
    Soundness of a Dataflow Analysis for Memory Monitoring.
    In Proc. of the 5th International Workshop on Languages and Tools for Ensuring Cyber-Resilience in Critical Software-Intensive Systems (HILT 2018),
    part of the ACM SIGPLAN Conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH 2018),
    Boston, USA, November 2018, ACM.
    Published in ACM SIGAda Ada Letters, vol. 38, No. 2. 2019. ACM. ISSN 1094-3641.
    [pdf] This is the authors' final version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in HILT 2018, http://doi.acm.org/10.1145/3375408.3375416.

  41. Sébastien Bardin, Nikolai Kosmatov, Bruno Marre, David Mentré, Nicky Williams.
    Test Case Generation with Pathcrawler/LTest: How to Automate an Industrial Testing Process.
    In Proc. of the 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2018),
    Limassol, Cyprus, November 2018, LNCS, vol. 11247, pages 104-120. Springer. ISBN 978-3-030-03426-9.
    [pdf] [slides] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-030-03427-6_12.

  42. Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue.
    A Lesson on Verification of IoT Software with Frama-C.
    In Proc. of the 12th International Conference on High Performance Computing & Simulation (HPCS 2018),
    Orléans, France, July 2018, pages 21-30. IEEE. ISBN 978-1-5386-7878-7.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/HPCS.2018.00018.

  43. Kostyantyn Vorobyov, Nikolai Kosmatov, Julien Signoles.
    Detection of Security Vulnerabilities in C Code using Runtime Verification: an Experience Report.
    In Proc. of the 12th International Conference on Tests & Proofs (TAP 2018),
    Toulouse, France, June 2018, pages 139-156. LNCS, vol. 10889. Springer. ISBN 978-3-319-92993-4.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-92994-1_8.

  44. Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto, Guillaume Petiot.
    Static and Dynamic Verification of Relational Properties on Self-Composed C Code.
    In Proc. of the 12th International Conference on Tests & Proofs (TAP 2018),
    Toulouse, France, June 2018, pages 44-62. LNCS, vol. 10889. Springer. ISBN 978-3-319-92993-4.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-92994-1_3.

  45. Frédéric Loulergue, Allan Blanchard, Nikolai Kosmatov.
    Ghosts for Lists: from Axiomatic to Executable Specifications.
    In Proc. of the 12th International Conference on Tests & Proofs (TAP 2018),
    Toulouse, France, June 2018, pages 177-184. LNCS, vol. 10889. Springer. ISBN 978-3-319-92993-4.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-92994-1_11.

  46. Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov.
    Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C.
    In Proc. of the 10th NASA Formal Methods Symposium (NFM 2018),
    Newport News, VA, USA, April 2018, LNCS, vol. 10811, pages 37-53. Springer. ISBN 978-3-319-77934-8.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: http://dx.doi.org/10.1007/978-3-319-77935-5_3.

  47. Michaël Marcozzi, Sébastien Bardin, Nikolai Kosmatov, Mike Papadakis, Virgile Prevosto and Loïc Correnson.
    Time to Clean your Test Objectives.
    In Proc. of the 40th International Conference on Software Engineering (ICSE 2018),
    Gothenburg, Sweden, June 2018, pages 456-467. ACM. ISBN 978-1-4503-5638-1.
    [pdf] This is the authors' final version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ICSE 2018, http://doi.acm.org/10.1145/3180155.3180191.

  48. Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall.
    Fast Computation of Arbitrary Control Dependencies.
    In Proc. of the 21st International Conference on Fundamental Approaches to Software Engineering (FASE 2018)
    part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2018),
    Thessaloniki, Greece, April 2018, pages 207-224. LNCS, vol. 10802. Springer. ISBN 978-3-319-89362-4.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: https://doi.org/10.1007/978-3-319-89363-1_12.

  49. Alexandre Peyrard, Nikolai Kosmatov, Simon Duquennoy, Shahid Raza.
    Towards Formal Verification of Contiki OS: Analysis of the AES-CCM* Modules with Frama-C.
    In Proc. of the 2nd International Workshop on Recent advances in secure management of data and resources in the IoT (RED-IoT 2018),
    part of the International Conference on Embedded Wireless Systems and Networks (EWSN 2018),
    Madrid, Spain, February 2018, pages 264-269. ACM.
    [pdf] This is the authors' final version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in RED-IOT 2018, http://dl.acm.org/citation.cfm?id=3234910.

  50. Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall.
    Why3 a dit : gardez le contrôle en toute situation.
    In 29mes Journées Francophones des Langages Applicatifs (JFLA 2018)
    Banyuls-sur-Mer, France, January 2018, 7 pages. (In French).
    [pdf]

    51. 2017:

  51. Julien Signoles, Nikolai Kosmatov and Kostyantyn Vorobyov.
    E-ACSL, a Runtime Verification Tool for Safety and Security of C Programs (tool paper).
    In Proc. of the 1st International Workshop on Competitions, Usability,
    Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES 2017),
    part of the 17th International Conference on Runtime Verification (RV 2017),
    Seattle, USA, September 2017, Kalpa Publications in Computing, vol. 3, pages 164-173, ISSN: 2515-1762.
    [pdf] This is the authors' final version of the work.

  52. Kostyantyn Vorobyov, Nikolai Kosmatov, Julien Signoles and Arvid Jakobsson.
    Runtime Detection of Temporal Memory Errors.
    In Proc. of the 17th International Conference on Runtime Verification (RV 2017),
    Seattle, USA, September 2017, LNCS, vol. 10548, pages 294-311. Springer. ISBN 978-3-319-67530-5.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-67531-2_18.

  53. Kostyantyn Vorobyov, Julien Signoles, and Nikolai Kosmatov.
    Shadow State Encoding for Efficient Monitoring of Block-level Properties.
    In Proc. of the 2017 ACM SIGPLAN International Symposium on Memory Management (ISMM 2017),
    Barcelona, Spain, June 2017, pages 47-58, ACM. ISBN 978-1-4503-5044-0.
    [pdf] This is the authors' final version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ISMM 2017, http://doi.acm.org/10.1145/3092255.3092269

  54. Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov.
    From Concurrent Programs to Sequential Simulating Programs: Correctness of a Transformation.
    In Proc. of the 5th International Workshop on Verification and Program Transformation (VPT 2017), ETAPS 2017 Workshops,
    Uppsala, Sweden, April 2017, EPTCS, vol. 253, pages 109-123.
    [pdf] This is the authors' final version of the work. DOI: 10.4204/EPTCS.253.9.

  55. Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall and Virgile Prevosto.
    RPP: Automatic Proof of Relational Properties by Self-Composition.
    In Proc. of the 23th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017),
    part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2017),
    Uppsala, Sweden, April 2017, LNCS, vol. 10205, pages 391-397. Springer. ISBN 978-3-662-54576-8.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-662-54577-5_22.

  56. Michaël Marcozzi, Mickaël Delahaye, Sébastien Bardin, Nikolai Kosmatov and Virgile Prevosto.
    Generic and Effective Specification of Structural Test Objectives.
    In Proc. of the 10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017),
    Tokyo, Japan, March 2017, pages 436-441. IEEE. ISBN 978-1-5090-6031-3.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/ICST.2017.48

  57. Michaël Marcozzi, Sébastien Bardin, Mickaël Delahaye, Nikolai Kosmatov and Virgile Prevosto.
    Taming Coverage Criteria Heterogeneity with LTest.
    In Proc. of the 10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017),
    Tokyo, Japan, March 2017, pages 500-507. IEEE. ISBN 978-1-5090-6031-3.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/ICST.2017.57

    58. 2016:

  58. Arvid Jakobsson, Nikolai Kosmatov and Julien Signoles.
    Fast as a shadow, expressive as a tree: Optimized memory monitoring for C.
    In Science of Computer Programming,
    2016, vol. 132, part 2, pages 226-246,. ISSN 0167-6423.
    [pdf] This is the authors' final version of the work. The final publication was published in Sci. Comput. Program., DOI: 10.1016/j.scico.2016.09.003

  59. Nikolai Kosmatov, Claude Marché, Yannick Moy, Julien Signoles.
    Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014.
    In Proc. of the 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2016),
    Corfu, Greece, October 2016, LNCS, vol. 9952, pages 461-478. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-47166-2_32.

  60. Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frédéric Loulergue.
    Conc2Seq : A Frama-C Plugin for Verification of Parallel Compositions of C Programs.
    In Proc. of the 16th IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2016),
    Raleigh, NC, USA, October 2016, pages 67-72. IEEE. ISBN 978-1-5090-3848-0.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/SCAM.2016.18.

  61. Nikolai Kosmatov, Julien Signoles.
    Frama-C, a Collaborative Framework for C Code Verification. Tutorial Synopsis.
    In Proc. of the 7th International Conference on Runtime Verification (RV 2016),
    Madrid, Spain, September 2016, LNCS, vol. 10012, pages 92-115. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-46982-9_7.

  62. Frédéric Mangano, Simon Duquennoy and Nikolai Kosmatov.
    A Memory Allocation Module of Contiki Formally Verified with Frama-C. A Case Study.
    In Proc. of the 11th International Conference on Risks and Security of Internet and Systems (CRiSIS 2016),
    Roscoff, France, September 2016, LNCS, vol. 10158, pages 114-120. Springer. ISBN 978-3-319-54875-3.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-54876-0_9.

  63. Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue.
    A CHR-Based Solver for Weak Memory Behaviors.
    In Proc. of the 7th International Workshop on Constraint Solvers in Testing, Verification, and Analysis (CSTVA 2016), ISSTA 2016 Workshops,
    Saarbruecken, Germany, July 2016, pages 15-22. CEUR Workshop Proceedings, vol. 1639.
    [pdf]

  64. Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti, Jacques Julliand.
    Your Proof Fails? Testing Helps to Find the Reason.
    Best paper award. [award]
    In Proc. of the 10th International Conference on Tests & Proofs (TAP 2016),
    Vienna, Austria, July 2016, pages 130-150. LNCS, vol. 9762. Springer. ISBN 978-3-319-41134-7.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-41135-4_8.

  65. Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall.
    Cut Branches Before Looking for Bugs: Sound Verification on Relaxed Slices.
    In Proc. of the 19th International Conference on Fundamental Approaches to Software Engineering (FASE 2016)
    part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2016),
    Eindhoven, The Netherlands, April 2016, pages 179-196. LNCS, vol. 9633. Springer. ISBN 978-3-662-49664-0.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-662-49665-7_11.

  66. Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall.
    Coq a dit : fromage tranché ne peut cacher ses trous.
    In 27mes Journées Francophones des Langages Applicatifs (JFLA 2016)
    Saint-Malo, France, January 2016, 3 pages. (In French).
    [pdf]

    67. 2015:

  67. Balázs Kiss, Nikolai Kosmatov, Dillon Pariente and Armand Puccetti.
    Combining Static and Dynamic Analyses for Vulnerability Detection: Illustration on Heartbleed.
    In Proc. of the 11th Haifa Verification Conference (HVC 2015),
    Haifa, Israel, November 2015, pages 39-50. LNCS, vol. 9434. Springer. ISBN 978-3-319-26286-4.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-26287-1

  68. 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.
    In Proc. of the 20th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2015),
    Oslo, Norway, June 2015, pages 15-30. LNCS, vol. 9128. Springer. ISBN 978-3-319-19457-8.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-19458-5_2

  69. Sébastien Bardin, Mickaël Delahaye, Robin David, Nikolai Kosmatov, Mike Papadakis, Yves Le Traon and Jean-Yves Marion.
    Sound and Quasi-Complete Detection of Infeasible Test Requirements.
    In Proc. of the 8th IEEE International Conference on Software Testing, Verification and Validation (ICST 2015),
    Graz, Austria, April 2015, pages 1-10. IEEE. ISBN 978-1-4799-7125-1.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/ICST.2015.7102607

  70. Arvid Jakobsson, Nikolai Kosmatov and Julien Signoles.
    Fast as a Shadow, Expressive as a Tree: Hybrid Memory Monitoring for C.
    In Proc. of the 30th ACM/SIGAPP Symposium On Applied Computing, Software Verification and Testing Track (SAC-SVT 2015),
    Salamanca, Spain, April 2015, pages 1765-1772. ACM. ISBN 978-1-4503-3196-8.
    [pdf] This is the authors' final version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in SAC 2015, DOI: 10.1145/2695664.2695815

  71. Arvid Jakobsson, Nikolai Kosmatov and Julien Signoles.
    Rester statique pour devenir plus rapide, plus précis et plus mince.
    In 26mes Journées Francophones des Langages Applicatifs (JFLA 2015)
    Val d'Ajol, France, January 2015, 15 pages. (In French)
    [pdf]

  72. Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski.
    Frama-C: A Program Analysis Perspective.
    In Formal Aspects of Computing Journal, vol. 27, issue 3, pages 573-609. 2015. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/s00165-014-0326-7

    73. 2014:

  73. Guillaume Petiot, Bernard Botella, Jacques Julliand, Nikolai Kosmatov, Julien Signoles.
    Instrumentation of Annotated C Programs for Test Generation.
    In Proc. of the 14th IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2014),
    Victoria, Canada, September 2014, pages 105-114. IEEE. ISBN 978-0-7695-5304-7.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/SCAM.2014.19

  74. Sébastien Bardin, Omar Chebaro, Mickaël Delahaye, Nikolai Kosmatov.
    An All-in-one Toolkit for Automated White-Box Testing.
    In Proc. of the 8th International Conference on Tests & Proofs (TAP 2014),
    York, UK, July 2014, pages 53-60. LNCS, vol. 8570. Springer. ISBN 978-3-319-09098-6.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-09099-3_4

  75. Nikolai Kosmatov, Matthieu Lemerre, Céline Alec.
    A Case Study on Verification of a Cloud Hypervisor by Proof and Structural Testing.
    In Proc. of the 8th International Conference on Tests & Proofs (TAP 2014),
    York, UK, July 2014, pages 158-164. LNCS, vol. 8570. Springer. ISBN 978-3-319-09098-6.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-09099-3_12

  76. Nikolai Kosmatov, Julien Signoles.
    Runtime Assertion Checking and its Combinations with Static and Dynamic Analyses. Tutorial Synopsis.
    In Proc. of the 8th International Conference on Tests & Proofs (TAP 2014),
    York, UK, July 2014, pages 165-168. LNCS, vol. 8570. Springer. ISBN 978-3-319-09098-6.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-09099-3_13

  77. Guillaume Petiot, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand.
    How Test Generation Helps Software Specification and Deductive Verification in Frama-C.
    In Proc. of the 8th International Conference on Tests & Proofs (TAP 2014),
    York, UK, July 2014, pages 204-211. LNCS, vol. 8570. Springer. ISBN 978-3-319-09098-6.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-09099-3_16

  78. Sébastien Bardin, Nikolai Kosmatov, François Cheynier.
    Efficient Leverage of Symbolic ATG Tools to Advanced Coverage Criteria.
    In Proc. of the 7th IEEE International Conference on Software Testing, Verification and Validation (ICST 2014),
    Cleveland, Ohio, USA, March-April 2014, pages 173-182. IEEE. ISBN 978-0-7695-5185-2.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/ICST.2014.30

  79. 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.
    In Automated Software Engineering Journal, vol. 21(1), pages 107-143. 2014. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/s10515-013-0127-x

    80. 2013:

  80. Nikolai Kosmatov, Guillaume Petiot, Julien Signoles.
    An Optimized Memory Monitoring for Runtime Assertion Checking of C Programs.
    In Proc. of the 4th International Conference on Runtime Verification (RV 2013),
    Rennes, France, September 2013, LNCS, vol. 8174, pages 167-182. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-642-40787-1_10

  81. Mickaël Delahaye, Nikolai Kosmatov.
    A Late Treatment of C Precondition in Dynamic Symbolic Execution Testing Tools.
    In Proc. of the 4th International Conference on Runtime Verification (RV 2013),
    Rennes, France, September 2013, LNCS, vol. 8174, pages 328-333. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-642-40787-1_20

  82. Nikolai Kosmatov, Julien Signoles.
    A Lesson on Runtime Assertion Checking with Frama-C.
    In Proc. of the 4th International Conference on Runtime Verification (RV 2013),
    Rennes, France, September 2013, LNCS, vol. 8174, pages 386-399. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-642-40787-1_29

  83. Nikolai Kosmatov, Virgile Prevosto, Julien Signoles.
    A Lesson on Proof of Programs with Frama-C. Invited Tutorial Paper.
    In Proc. of the 7th International Conference on Tests and Proofs (TAP 2013),
    Budapest, Hungary, June 2013, LNCS, vol. 7942, pages 168-177. Springer.
    [pdf] This is the authors' final version of the work. The final publication will be available at http://link.springer.com. DOI: 10.1007/978-3-642-38916-0_10

  84. Nikolai Kosmatov, Nicky Williams, Bernard Botella, Muriel Roger.
    Strucutural Unit Testing as a Service with PathCrawler-online.com.
    In Proc. of the 7th IEEE International Symposium on Service Oriented System Engineering (SOSE 2013),
    San Francisco Bay, USA, March 2013, pages 435-440. ISBN 978-0-7695-4944-6.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/SOSE.2013.78.

  85. Mickaël Delahaye, Nikolai Kosmatov.
    A Late Treatment of C Precondition in Dynamic Symbolic Execution.
    In Proc. of the 5th International Workshop on Constraints in Software Testing, Verification, and Analysis (CSTVA 2013), ICST Workshops,
    Luxembourg, March 2013, pages 230-231. IEEE. ISBN 978-1-4799-1324-4.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/ICSTW.2013.34.

  86. Mickaël Delahaye, Nikolai Kosmatov, Julien Signoles.
    Common Specification Language for Static and Dynamic Analysis of C Programs.
    In Proc. of the 28th Annual ACM Symposium On Applied Computing, Software Verification and Testing Track (SAC-SVT 2013),
    Coimbra, Portugal, March 2013, pages 1230--1235, ACM. ISBN 978-1-4503-1656-9.
    [pdf] This is the authors' final version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in SAC 2013, http://dx.doi.org/10.1145/2480362.2480593

  87. Nikolai Kosmatov.
    Concolic Test Generation and the Cloud: Deployment and Verification Perspectives.
    Chapter 11 in Software Testing in the Cloud: Perspectives on an Emerging Discipline
    pages 231-251. IGI Global, 2013. ISBN 978-1-46662-536-5.
    [pdf] This is the author's final version of the work.

    88. 2012:

  88. Matthieu Lemerre, Nikolai Kosmatov, Céline Alec.
    Verified secure kernels and hypervisors for the cloud.
    In Proc. of Computer and Electronics Security Applications Rendez-vous (C&ESAR 2012),
    Rennes, France, November 2012, pages 89--104.
    [pdf] This paper is not a formal archieval publication.

  89. Omar Chebaro, Mickaël Delahaye, Nikolai Kosmatov.
    Testing Inexecutable Conditions on Input Pointers in C Programs with SANTE.
    In Proc. of the 24th International Conference on Software & Systems Engineering and their Applications (ICSSEA 2012),
    Paris, France, October 2012.
    [pdf] This is the authors' final version of the work.

  90. Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski.
    Frama-C: A Program Analysis Perspective.
    In Proc. of the 10th International Conference on Software Engineering and Formal Methods (SEFM 2012),
    Thessaloniki, Greece, October 2012, LNCS, vol. 7504, pages 233-247. Springer. ISBN 978-3-642-33825-0.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-642-33826-7_16

  91. Nicky Williams, Nikolai Kosmatov.
    Structural Testing with PathCrawler. Tutorial Synopsis.
    In Proc. of the 12th International Conference on Quality Software (QSIC 2012),
    Xi'an, China, August 2012, pages 289-292. IEEE. ISBN 978-0-7695-4833-3.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/QSIC.2012.24

  92. Frédéric Loulergue, Frédéric Gava, Nikolai Kosmatov, Matthieu Lemerre.
    Towards Verified Cloud Computing Environments.
    In Proc. of the 2012 International Conference on High Performance Computing and Simulation (HPCS 2012),
    Madrid, Spain, July 2012, pages 91-97. IEEE. ISBN 978-1-4673-2359-8.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/HPCSim.2012.6266896

  93. Nikolai Kosmatov, Nicky Williams, Bernard Botella, Muriel Roger, Omar Chebaro.
    A lesson on structural testing with pathcrawler-online.com.
    In Proc. of the 6th International Conference on Tests and Proofs (TAP 2012),
    Prague, Czech Republic, May-June 2012, LNCS, vol. 7305, pages 169-175. Springer. ISBN 978-3-642-30472-9.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-642-30473-6_15

  94. Nikolai Kosmatov, Nicky Williams.
    Tutorial on Automated Structural Testing with PathCrawler -- Extended Abstract.
    In Proc. of the 6th International Conference on Tests and Proofs (TAP 2012),
    Prague, Czech Republic, May-June 2012, LNCS, vol. 7305, pages 176. Springer. ISBN 978-3-642-30472-9.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-642-30473-6_16

  95. Omar Chebaro, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand.
    Program Slicing Enhances a Verification Technique Combining Static and Dynamic Analysis.
    In Proc. of the 27th Annual ACM Symposium On Applied Computing, Software Verification and Testing Track (SAC-SVT 2012),
    Riva del Garda (Trento), Italy, March 2012, pages 1284--1291, ACM. ISBN 978-1-4503-0857-1.
    [pdf] This is the authors' final version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in SAC 2012, http://dx.doi.org/10.1145/2245276.2231980

    96. 2011:

  96. Nikolai Kosmatov, Bernard Botella, Muriel Roger, Nicky Williams.
    Online Test Generation with PathCrawler. Tool demo.
    Best demo award.
    In Proc. of the 3rd International Workshop on Constraints in Software Testing, Verification, and Analysis (CSTVA 2011), ICST Workshops,
    Berlin, Germany, March 2011, pages 316-317. IEEE. ISBN 978-1-4577-0019-4.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/ICSTW.2011.85.

  97. Omar Chebaro, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand.
    The SANTE Tool: Value Analysis, Program Slicing and Test Generation for C Program Debugging.
    In Proc. of the 5th International Conference on Tests and Proofs (TAP 2011),
    Zurich, Switzerland, June-July 2011, LNCS, vol. 6706, pages 78-83. Springer. ISBN 978-3-642-21767-8.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-642-21768-5_7

    98. 2010:

  98. Nikolai Kosmatov.
    Génération de tests "tous-les-chemins" : quelle complexité pour quelles contraintes?.
    In Actes des Sixièmes Journées Francophones de Programmation par Contraintes (JFPC 2010),
    Caen, France, Juin 2010, pages 187-196.
    [pdf]

  99. Omar Chebaro, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand.
    Combining Static Analysis and Test Generation for C Program Debugging.
    In Proc. of the 4th International Conference on Tests and Proofs (TAP 2010),
    Malaga, Spain, July 2010, LNCS, vol. 6143, pages 94-100. Springer. ISBN 978-3-642-13976-5.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-642-13977-2_9

  100. Nikolai Kosmatov.
    Constraint-Based Techniques for Software Testing.
    Chapter 11 in Artificial Intelligence Applications for Improved Software Engineering Development: New Prospects
    Advances in Intelligent Information Technologies Book Series
    pages 218-232. IGI Global, 2010. ISBN 978-1-60566-758-4.
    [pdf] This is the author's final version of the work.

    101. 2009:

  101. Nikolai Kosmatov.
    On Complexity of All-Paths Test Generation. From Practice to Theory.
    In Proc. of the Testing: Academic and Industrial Conference - Practice and Research Techniques (TAIC PART 2009),
    Windsor, United Kingdom, September 2009, pages 144-153. IEEE Computer Society Press. ISBN 978-0-7695-3820-4.
    [pdf] This is the author's final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/TAICPART.2009.26

  102. 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
    In Proc. of the Fourth International Workshop on the Automation of Software Test (AST 2009),
    part of the 31st International Conference on Software Engineering (ICSE 2009),
    Vancouver, Canada, May 2009, pages 70-78. IEEE Computer Society Press.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/IWAST.2009.5069043

    103. 2008:

  103. Nikolai Kosmatov.
    All-paths test generation for programs with internal aliases.
    In Proc. of the 19th IEEE Int. Symp. on Software Reliability Engineering (ISSRE 2008),
    Redmond, Seattle, USA, November 2008, pages 147-156. IEEE Computer Society Press. ISBN 978-1-4244-3417-6.
    [pdf] This is the author's final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/ISSRE.2008.25

    104. 2006:

  104. Nikolai Kosmatov.
    Constraint Solving for Sequences in Software Validation and Verification.
    In M. Umeda, A. Wolf et al., editors,
    Revised Selected Papers of the 16th International Conference on Applications of Declarative Programming and Knowledge Management (INAP 2005),
    Fukuoka, Japan, October 2005, LNCS, vol. 4369, pages 25-37. Springer, 2006. ISBN 978-3-540-69233-1. DOI: 10.1007/11963578_3.

  105. Nikolai Kosmatov.
    A Constraint Solver for Sequences and its Applications.
    In Proc. of the 21st Annual ACM Symposium on Applied Computing, Constraint Solving and Programming Track (SAC-SCP 2006),
    Dijon, France, April 2006, pages 404-408. ACM Press. ISBN: 1-59593-108-2.
    [pdf] © ACM, 2006.
    This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in SAC 2006, http://doi.acm.org/10.1145/1141277.1141369

  106. Yohan Boichut, Nikolai Kosmatov, Laurent Vigneron.
    Validation of Prouvé protocols using the automatic tool TA4SP.
    In Proc. of the Third Taiwanese-French Conference on Information Technology (TFIT 2006),
    Nancy, France, March 2006, pages 467-480.
    [pdf]

    107. 2005:

  107. Jean-François Couchot, Alain Giorgetti, Nikolai Kosmatov.
    A uniform deductive approach for parameterized protocol safety.
    In Proc. of the 20th IEEE/ACM International Conference on Automated Software Engineering (ASE 2005),
    Long Beach, California, USA, November 2005, pages 364-367. IEEE Computer Society Press. ISBN: 1-59593-993-4.
    [pdf] © ACM, 2005.
    This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ASE 2005, http://doi.acm.org/10.1145/1101908.1101971

  108. Nikolai Kosmatov.
    A Constraint Solver for Sequences.
    In Proc. of the 1st Int. Workshop on Constraint Programming Beyond Finite Integer Domains (BeyondFD 2005),
    part of the 11th International Conference on Principles and Practice of Constraint Programming (CP 2005),
    Sitges (Barcelona), Spain, October 2005, pages 49-54.
    [pdf]

    109. 2004:

  109. Nikolai Kosmatov, Bruno Legeard, Fabien Peureux, Mark Utting.
    Boundary coverage criteria for test generation from formal models.
    In Proc. of the 15th IEEE Int. Symp. on Software Reliability Engineering (ISSRE 2004),
    Saint-Malo, France, November 2004, pages 139-150. IEEE Computer Society Press. ISBN 0-7695-2215-7.
    [pdf] This is the author's final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/ISSRE.2004.12

    110. In Mathematics:
    2007:

  110. Alexander Generalov, Nikolai Kosmatov.
    Projective resolutions and Yoneda algebras for algebras of dihedral type.
    Algebras and Repr. Theory. 10 (2007), no. 3, 241-256. Springer.
    [pdf] This is the author's final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/s10468-006-9012-7

    111. 2004:

  111. Alexander Generalov, Nikolai Kosmatov.
    Projective resolutions and Yoneda algebras for algebras of dihedral type: the family D(3Q).
    J. Math. Sci. 140 (2007), 221-238. (Originally published in Fund. Appl. Math. in 2004, vol. 10, no. 4, 65-89.)
    [pdf] This is the author's final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/s10958-007-0419-4.

    112. 2003:

  112. Alexander Generalov, Nikolai Kosmatov.
    Computation of the Yoneda algebras for algebras of dihedral type.
    J. Math. Sci. 130 (2005), no. 3, 4699-4711. Springer.
    Russian version in
    Zap. Nauchn. Sem. S.-Peterburg. Otdel. Mat. Inst. Steklov. (POMI) 305 (2003), 101-120.
    [pdf] This is the author's final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/s10958-005-0364-z

    113. 2002:

  113. Nikolai Kosmatov.
    On the homological dimensions of pullbacks. II.
    Théorie des nombres, Années 1998/2001, 4 pp.,
    Publ. Math. UFR Sci. Tech. Besançon, Univ. Franche-Comté, Besançon, 2002.

    114. 2000:

  114. Nikolai Kosmatov.
    Bounds on Homological Dimensions of Pullbacks. II.
    J. Math. Sci. 116 (2003), no. 1, 3014-3015. Springer.
    Russian version in
    Zap. Nauchn. Sem. S.-Peterburg. Otdel. Mat. Inst. Steklov. (POMI) 272 (2000), 234-237.
    [pdf] This is the author's final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1023/A:1023551328399

    115. 1999:

  115. Nikolai Kosmatov.
    Bounds for the Homological Dimensions of Pullbacks.
    J. Math. Sci. 112 (2002), no. 4, 4367-4370. Springer.
    Russian version in
    Zap. Nauchn. Sem. S.-Peterburg. Otdel. Mat. Inst. Steklov.(POMI) 265 (1999), 222-228.
    [pdf] This is the author's final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1023/A:1020351104689

  116. Nikolai Kosmatov.
    An estimate for the global dimension of pullback rings. (In Russian)
    Fund. Appl. Math. 5 (1999), no. 4, 1251-1253.
    [pdf] This is the author's final version of the work.

  117. Nikolai Kosmatov.
    On the global and weak dimensions of pullbacks of non-commutative rings.
    Théorie des nombres, Années 1996/97-1997/98, 7 pp.,
    Publ. Math. UFR Sci. Tech. Besançon, Univ. Franche-Comté, Besançon, 1999.

Back to the main page