Nikolai Kosmatov

117 papers A* 2A 6B 21C 8Misc 7Journal 30Unranked 42

Year	Rank	Type	Title / Venue / Authors
2025	—	`conf`	Aspycot: A Spike and Python Co-simulation Testbench for Hardware Monitoring IPs. RAPIDO@HiPEAC Téo Biton, Sébastien Pillement, Olivier Gilles, Nikolai Kosmatov, Daniel Gracia Pérez
2025	J	`jnl`	Call Rewinding: Efficient Backward Edge Protection. IACR Trans. Cryptogr. Hardw. Embed. Syst. Téo Biton, Olivier Gilles, Daniel Gracia Pérez, Nikolai Kosmatov, Sébastien Pillement
2025	B	`conf`	Formal Verification of PKCS#1 Signature Parser Using Frama-C. iFM Martin Hána, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles
2025	B	`ed.`	Integrated Formal Methods - 19th International Conference, IFM 2024, Manchester, UK, November 13-15, 2024, Proceedings IFM Nikolai Kosmatov, Laura Kovács
2025	B	`conf`	Prove your Colorings: Formal Verification of Cache Coloring of Bao Hypervisor. FASE Axel Ferréol, Laurent Corbin, Nikolai Kosmatov
2025	J	`jnl`	Towards Formal Verification of a TPM Software Stack: Achievements and Opportunities. Formal Aspects Comput. Yani Ziani, Téo Bernier, Nikolai Kosmatov, Frédéric Loulergue, Daniel Gracia Pérez
2024	—	`conf`	A Case Study on Numerical Analysis of a Path Computation Algorithm. FMAS@iFM Grégoire Boussu, Nikolai Kosmatov, Franck Védrine
2024	J	`jnl`	An Efficient VCGen-based Modular Verification of Relational Properties. CoRR Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall
2024	—	`conf`	Automate where Automation Fails: Proof Strategies for Frama-C/WP. TACAS (1) Loïc Correnson, Allan Blanchard, Adel Djoudi, Nikolai Kosmatov
2024	B	`conf`	Combining Deductive Verification with Shape Analysis. FASE Téo Bernier, Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue
2024	—	`conf`	High-Level Program Properties in Frama-C: Definition, Verification and Deduction. ISoLA (3) Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall
2024	C	`conf`	No Smoke Without Fire: Detecting Specification Inconsistencies with Frama-C/WP. TAP Allan Blanchard, Loïc Correnson, Adel Djoudi, Nikolai Kosmatov
2024	C	`conf`	Runtime Verification for High-Level Security Properties: Case Study on the TPM Software Stack. TAP Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue, Daniel Gracia Pérez
2024	J	`jnl`	Sound Runtime Assertion Checking for Memory Properties via Program Transformation. Formal Aspects Comput. Dara Ly, Nikolai Kosmatov, Frédéric Loulergue, Julien Signoles
2023	Misc	`conf`	An Efficient Black-Box Support of Advanced Coverage Criteria for Klee. SAC Nicolas Berthier, Steven de Oliveira, Nikolai Kosmatov, Delphine Longuet, Romain Soulat
2023	J	`jnl`	Efficient computation of arbitrary control dependencies. Theor. Comput. Sci. Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall
2023	—	`conf`	Execution at RISC: Stealth JOP Attacks on RISC-V Applications. ESORICS Workshops (2) Loïc Buckwell, Olivier Gilles, Daniel Gracia Pérez, Nikolai Kosmatov
2023	J	`jnl`	Execution at RISC: Stealth JOP Attacks on RISC-V Applications. CoRR Loïc Buckwell, Olivier Gilles, Daniel Gracia Pérez, Nikolai Kosmatov
2023	B	`conf`	Towards Formal Verification of a TPM Software Stack. iFM Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue, Daniel Gracia Pérez, Téo Bernier
2023	J	`jnl`	Towards Formal Verification of a TPM Software Stack. CoRR Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue, Daniel Gracia Pérez, Téo Bernier
2022	J	`jnl`	An Efficient Black-Box Support of Advanced Coverage Criteria for Klee. CoRR Nicolas Berthier, Steven de Oliveira, Nikolai Kosmatov, Delphine Longuet, Romain Soulat
2022	—	`conf`	An Efficient VCGen-Based Modular Verification of Relational Properties. ISoLA (1) Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall
2022	B	`conf`	Certified Verification of Relational Properties. IFM Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall
2022	J	`jnl`	Certified Verification of Relational Properties. CoRR Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall
2022	J	`jnl`	Control-Flow Integrity at RISC: Attacking RISC-V by Jump-Oriented Programming. CoRR Olivier Gilles, Franck Viguier, Nikolai Kosmatov, Daniel Gracia Pérez
2022	J	`jnl`	Editorial. Softw. Qual. J. Christophe Gaston, Nikolai Kosmatov, Pascale Le Gall
2022	Misc	`conf`	Verifying redundant-check based countermeasures: a case study. SAC Thibault Martin, Nikolai Kosmatov, Virgile Prevosto
2021	J	`jnl`	Correction to: PolyGraph: a data flow model with frequency arithmetic. Int. J. Softw. Tools Technol. Transf. Paul Dubrulle, Nikolai Kosmatov, Christophe Gaston, Arnault Lapitre
2021	B	`conf`	Formal Verification of a JavaCard Virtual Machine with Frama-C. FM Adel Djoudi, Martin Hána, Nikolai Kosmatov
2021	—	`conf`	Methodology for Specification and Verification of High-Level Requirements with MetAcsl. FormaliSE@ICSE Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall
2021	J	`jnl`	PolyGraph: a data flow model with frequency arithmetic. Int. J. Softw. Tools Technol. Transf. Paul Dubrulle, Nikolai Kosmatov, Christophe Gaston, Arnault Lapitre
2021	B	`conf`	Runtime Abstract Interpretation for Numerical Accuracy and Robustness. VMCAI Franck Védrine, Maxime Jacquemin, Nikolai Kosmatov, Julien Signoles
2021	J	`jnl`	Specify and measure, cover and reveal: A unified framework for automated test generation. Sci. Comput. Program. Sébastien Bardin, Nikolai Kosmatov, Michaël Marcozzi, Mickaël Delahaye
2021	J	`jnl`	The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. Commun. ACM 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
2020	B	`conf`	Detection of Polluting Test Objectives for Dataflow Criteria. IFM Thibault Martin, Nikolai Kosmatov, Virgile Prevosto, Matthieu Lemerre
2020	B	`conf`	Efficient Runtime Assertion Checking for Properties over Mathematical Numbers. RV Nikolai Kosmatov, Fonenantsoa Maurica, Julien Signoles
2020	—	`conf`	Formal Verification of an Industrial Distributed Algorithm: An Experience Report. ISoLA (1) Nikolai Kosmatov, Delphine Longuet, Romain Soulat
2020	—	`conf`	Verified Runtime Assertion Checking for Memory Properties. TAP@STAF Dara Ly, Nikolai Kosmatov, Frédéric Loulergue, Julien Signoles
2019	B	`conf`	A Data Flow Model with Frequency Arithmetic. FASE Paul Dubrulle, Christophe Gaston, Nikolai Kosmatov, Arnault Lapitre, Stéphane Louise
2019	J	`jnl`	Abstract Compilation for Verification of Numerical Accuracy Properties. CoRR Maxime Jacquemin, Fonenantsoa Maurica, Nikolai Kosmatov, Julien Signoles, Franck Védrine
2019	B	`conf`	Dynamic Reconfigurations in Frequency Constrained Data Flow. IFM Paul Dubrulle, Christophe Gaston, Nikolai Kosmatov, Arnault Lapitre
2019	J	`jnl`	Introduction to the STAF 2015 special section. Softw. Syst. Model. Jasmin Blanchette, Francis Bordeleau, Alfonso Pierantonio, Nikolai Kosmatov, Gabriele Taentzer, Manuel Wimmer
2019	Misc	`conf`	Logic against ghosts: comparison of two proof approaches for a list module. SAC Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
2019	—	`conf`	MetAcsl: Specification and Verification of High-Level Properties. TACAS (1) Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall
2019	—	`conf`	Tame Your Annotations with MetAcsl: Specifying, Testing and Proving High-Level Properties. TAP@FM Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall
2019	C	`ed.`	Testing Software and Systems - 31st IFIP WG 6.1 International Conference, ICTSS 2019, Paris, France, October 15-17, 2019, Proceedings ICTSS Christophe Gaston, Nikolai Kosmatov, Pascale Le Gall
2019	—	`conf`	Towards Full Proof Automation in Frama-C Using Auto-active Verification. NFM Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov
2018	—	`conf`	A Lesson on Verification of IoT Software with Frama-C. HPCS Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
2018	J	`jnl`	Cut branches before looking for bugs: certifiably sound verification on relaxed slices. Formal Aspects Comput. Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall
2018	—	`conf`	Detection of Security Vulnerabilities in C Code Using Runtime Verification: An Experience Report. TAP@STAF Kostyantyn Vorobyov, Nikolai Kosmatov, Julien Signoles
2018	B	`conf`	Fast Computation of Arbitrary Control Dependencies. FASE Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall
2018	—	`conf`	Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C. NFM Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
2018	—	`conf`	Ghosts for Lists: From Axiomatic to Executable Specifications. TAP@STAF Frédéric Loulergue, Allan Blanchard, Nikolai Kosmatov
2018	J	`jnl`	How testing helps to diagnose proof failures. Formal Aspects Comput. Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti, Jacques Julliand
2018	J	`jnl`	MMFilter : A CHR-Based Solver for Generation of Executions under Weak Memory Models. Comput. Lang. Syst. Struct. Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
2018	J	`jnl`	MetAcsl: Specification and Verification of High-Level Properties. CoRR Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall
2018	J	`jnl`	Self-composition to Prove Relational Properties in Annotated C Program. CoRR Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto
2018	—	`conf`	Static and Dynamic Verification of Relational Properties on Self-composed C Code. TAP@STAF Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto, Guillaume Petiot
2018	—	`conf`	Test Case Generation with PathCrawler/LTest: How to Automate an Industrial Testing Process. ISoLA (4) Sébastien Bardin, Nikolai Kosmatov, Bruno Marre, David Mentré, Nicky Williams
2018	A*	`conf`	Time to clean your test objectives. ICSE Michaël Marcozzi, Sébastien Bardin, Nikolai Kosmatov, Mike Papadakis, Virgile Prevosto, Loïc Correnson
2018	B	`conf`	Towards Formal Verification of Contiki: Analysis of the AES-CCM* Modules with Frama-C. EWSN Alexandre Peyrard, Nikolai Kosmatov, Simon Duquennoy, Shahid Raza
2018	—	`conf`	Tutorial: Secure Your Things: Secure Development of IoT Software with Frama-C. SecDev Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
2017	—	`conf`	E-ACSL, a Runtime Verification Tool for Safety and Security of C Programs (tool paper). RV-CuBES Julien Signoles, Nikolai Kosmatov, Kostyantyn Vorobyov
2017	J	`jnl`	Freeing Testers from Polluting Test Objectives. CoRR Michaël Marcozzi, Sébastien Bardin, Nikolai Kosmatov, Mike Papadakis, Virgile Prevosto, Loïc Correnson
2017	—	`conf`	From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation. VPT@ETAPS Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov
2017	A	`conf`	Generic and Effective Specification of Structural Test Objectives. ICST Michaël Marcozzi, Mickaël Delahaye, Sébastien Bardin, Nikolai Kosmatov, Virgile Prevosto
2017	—	`conf`	RPP: Automatic Proof of Relational Properties by Self-composition. TACAS (1) Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto
2017	B	`conf`	Runtime Detection of Temporal Memory Errors. RV Kostyantyn Vorobyov, Nikolai Kosmatov, Julien Signoles, Arvid Jakobsson
2017	C	`conf`	Shadow state encoding for efficient monitoring of block-level properties. ISMM Kostyantyn Vorobyov, Julien Signoles, Nikolai Kosmatov
2017	A	`conf`	Taming Coverage Criteria Heterogeneity with LTest. ICST Michaël Marcozzi, Sébastien Bardin, Mickaël Delahaye, Nikolai Kosmatov, Virgile Prevosto
2016	—	`conf`	A CHR-Based Solver for Weak Memory Behaviors. CSTVA@ISSTA Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
2016	C	`conf`	Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs. SCAM Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frédéric Loulergue
2016	B	`conf`	Cut Branches Before Looking for Bugs: Sound Verification on Relaxed Slices. FASE Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall
2016	J	`jnl`	Deductive Verification with Relational Properties. CoRR Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto
2016	J	`jnl`	Fast as a shadow, expressive as a tree: Optimized memory monitoring for C. Sci. Comput. Program. Arvid Jakobsson, Nikolai Kosmatov, Julien Signoles
2016	C	`conf`	Formal Verification of a Memory Allocation Module of Contiki with Frama-C: A Case Study. CRiSIS Frédéric Mangano, Simon Duquennoy, Nikolai Kosmatov
2016	B	`conf`	Frama-C, A Collaborative Framework for C Code Verification: Tutorial Synopsis. RV Nikolai Kosmatov, Julien Signoles
2016	J	`jnl`	Generic and Effective Specification of Structural Test Objectives. CoRR Sébastien Bardin, Mickaël Delahaye, Nikolai Kosmatov, Michaël Marcozzi, Virgile Prevosto
2016	—	`conf`	Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014. ISoLA (1) Nikolai Kosmatov, Claude Marché, Yannick Moy, Julien Signoles
2016	—	`conf`	Your Proof Fails? Testing Helps to Find the Reason. TAP@STAF Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti, Jacques Julliand
2015	C	`conf`	A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C. FMICS Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frédéric Loulergue
2015	—	`conf`	Combining Static and Dynamic Analyses for Vulnerability Detection: Illustration on Heartbleed. Haifa Verification Conference Balázs Kiss, Nikolai Kosmatov, Dillon Pariente, Armand Puccetti
2015	Misc	`conf`	Fast as a shadow, expressive as a tree: hybrid memory monitoring for C. SAC Arvid Jakobsson, Nikolai Kosmatov, Julien Signoles
2015	J	`jnl`	Frama-C: A software analysis perspective. Formal Aspects Comput. Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, Boris Yakobowski
2015	A	`conf`	Sound and Quasi-Complete Detection of Infeasible Test Requirements. ICST Sébastien Bardin, Mickaël Delahaye, Robin David, Nikolai Kosmatov, Mike Papadakis, Yves Le Traon, Jean-Yves Marion
2015	—	`ed.`	Tests and Proofs - 9th International Conference, TAP@STAF 2015, L'Aquila, Italy, July 22-24, 2015. Proceedings TAP@STAF Jasmin Christian Blanchette, Nikolai Kosmatov
2015	J	`jnl`	Your Proof Fails? Testing Helps to Find the Reason. CoRR Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti, Jacques Julliand
2014	—	`conf`	A Case Study on Verification of a Cloud Hypervisor by Proof and Structural Testing. TAP@STAF Nikolai Kosmatov, Matthieu Lemerre, Céline Alec
2014	—	`conf`	An All-in-One Toolkit for Automated White-Box Testing. TAP@STAF Sébastien Bardin, Omar Chebaro, Mickaël Delahaye, Nikolai Kosmatov
2014	J	`jnl`	Behind the scenes in SANTE: a combination of static and dynamic analyses. Autom. Softw. Eng. Omar Chebaro, Pascal Cuoq, Nikolai Kosmatov, Bruno Marre, Anne Pacalet, Nicky Williams, Boris Yakobowski
2014	A	`conf`	Efficient Leveraging of Symbolic Execution to Advanced Coverage Criteria. ICST Sébastien Bardin, Nikolai Kosmatov, François Cheynier
2014	—	`conf`	How Test Generation Helps Software Specification and Deductive Verification in Frama-C. TAP@STAF Guillaume Petiot, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand
2014	C	`conf`	Instrumentation of Annotated C Programs for Test Generation. SCAM Guillaume Petiot, Bernard Botella, Jacques Julliand, Nikolai Kosmatov, Julien Signoles
2014	—	`conf`	Runtime Assertion Checking and Its Combinations with Static and Dynamic Analyses - Tutorial Synopsis. TAP@STAF Nikolai Kosmatov, Julien Signoles
2013	B	`conf`	A Late Treatment of C Precondition in Dynamic Symbolic Execution Testing Tools. RV Mickaël Delahaye, Nikolai Kosmatov
2013	—	`conf`	A Late Treatment of C Precondition in Dynamic Symbolic Execution. ICST Workshops Mickaël Delahaye, Nikolai Kosmatov
2013	—	`conf`	A Lesson on Proof of Programs with Frama-C. Invited Tutorial Paper. TAP@STAF Nikolai Kosmatov, Virgile Prevosto, Julien Signoles
2013	B	`conf`	A Lesson on Runtime Assertion Checking with Frama-C. RV Nikolai Kosmatov, Julien Signoles
2013	B	`conf`	An Optimized Memory Monitoring for Runtime Assertion Checking of C Programs. RV Nikolai Kosmatov, Guillaume Petiot, Julien Signoles
2013	Misc	`conf`	Common specification language for static and dynamic analysis of C programs. SAC Mickaël Delahaye, Nikolai Kosmatov, Julien Signoles
2013	J	`jnl`	Efficient Leverage of Symbolic ATG Tools to Advanced Coverage Criteria. CoRR Sébastien Bardin, Nikolai Kosmatov, François Cheynier
2013	—	`conf`	Structural Unit Testing as a Service with PathCrawler-online.com. SOSE Nikolai Kosmatov, Nicky Williams, Bernard Botella, Muriel Roger
2012	—	`conf`	A Lesson on Structural Testing with PathCrawler-online.com. TAP@TOOLS Nikolai Kosmatov, Nicky Williams, Bernard Botella, Muriel Roger, Omar Chebaro
2012	B	`conf`	Frama-C - A Software Analysis Perspective. SEFM Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, Boris Yakobowski
2012	Misc	`conf`	Program slicing enhances a verification technique combining static and dynamic analysis. SAC Omar Chebaro, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand
2012	—	`conf`	Structural Testing with PathCrawler: Tutorial Synopsis. QSIC Nicky Williams, Nikolai Kosmatov
2012	—	`conf`	Towards verified cloud computing environments. HPCS Frédéric Loulergue, Frédéric Gava, Nikolai Kosmatov, Matthieu Lemerre
2012	—	`conf`	Tutorial on Automated Structural Testing with PathCrawler - (Extended Abstract). TAP@TOOLS Nikolai Kosmatov, Nicky Williams
2011	—	`conf`	Online Test Generation with PathCrawler: Tool Demo. ICST Workshops Nikolai Kosmatov, Bernard Botella, Muriel Roger, Nicky Williams
2011	—	`conf`	The SANTE Tool: Value Analysis, Program Slicing and Test Generation for C Program Debugging. TAP@TOOLS Omar Chebaro, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand
2010	—	`conf`	Combining Static Analysis and Test Generation for C Program Debugging. TAP@TOOLS Omar Chebaro, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand
2009	—	`conf`	Automating Structural Testing of C Programs: Experience with PathCrawler. AST@ICSE Bernard Botella, Mickaël Delahaye, Stéphane Hong Tuan Ha, Nikolai Kosmatov, Patricia Mouy, Muriel Roger, Nicky Williams
2008	A	`conf`	All-Paths TestGenerationfor Programs with Internal Aliases. ISSRE Nikolai Kosmatov
2006	Misc	`conf`	A constraint solver for sequences and its applications. SAC Nikolai Kosmatov
2005	A*	`conf`	A uniform deductive approach for parameterized protocol safety. ASE Jean-François Couchot, Alain Giorgetti, Nikolai Kosmatov
2005	—	`conf`	Constraint Solving for Sequences in Software Validation and Verification. INAP Nikolai Kosmatov
2004	A	`conf`	Boundary Coverage Criteria for Test Generation from Formal Models. ISSRE Nikolai Kosmatov, Bruno Legeard, Fabien Peureux, Mark Utting