Recherche - CEA - Commissariat à l’énergie atomique et aux énergies alternatives Accéder directement au contenu

Filtrer vos résultats

158 résultats
Page :
triés par
Image document

On the stability, correctness and plausibility of visual explanation methods based on feature importance

 Romain Xu-Darme , Jenny Benois-Pineau , Romain Giot , Georges Quénot , Zakaria Chihani , et al.
2023
Pré-publication, Document de travail cea-04256974v1
Image document

CaFE : un model-checker collaboratif

 Steven de Oliveira , Virgile Prévosto , Saddek Bensalem
Approches Formelles pour l'Assistance au Développement du logiciel - AFADL, Jun 2017, Montpellier, France
Communication dans un congrès cea-01835522v1
Image document

Interface compliance of inline assembly: automatically check, patch and refine

 Frederic Recoules , Sébastien Bardin , Richard Bonichon , Matthieu Lemerre , Laurent Mounier , et al.
2021 IEEE/ACM - 43rd International Conference on Software Engineering, May 2021, Madrid, Spain. pp.1236-1247, ⟨10.1109/ICSE43902.2021.00113⟩
Communication dans un congrès cea-04228171v1
Image document

Contextualised Out-of-Distribution Detection using Pattern Identification

 Romain Xu-Darme , Julien Girard-Satabin , Darryl Hond , Gabriele Incorvaia , Zakaria Chihani
Computer Safety, Reliability, and Security. SAFECOMP 2023 Workshops, Sep 2023, Toulouse, France
Communication dans un congrès cea-04254022v1

Specifying and Verifying Concurrent C Programs with TLA+

 Amira Methni , Matthieu Lemerre , Belgacem Ben Hedia , Serge Haddad , Kamel Barkaoui
Formal Techniques for Safety-Critical Systems, 476, Springer, pp.206-222, 2015, Communications in Computer and Information Science
Chapitre d'ouvrage hal-01242954v1

Formal Methods for Quantum Algorithms

 Christophe Chareton , Sébastien Bardin , Dongho Lee , Benoît Valiron , Renaud Vilmart , et al.
Handbook of Formal Analysis and Verification in Cryptography, 1, CRC Press, pp.319-422, 2023, ⟨10.1201/9781003090052-7⟩
Chapitre d'ouvrage hal-04311441v1
Image document

Automated Constructivization of Proofs

 Frédéric Gilbert
FoSSaCS 2017, Apr 2017, Uppsala, Sweden. ⟨10.1007/978-3-662-54458-7_28⟩
Communication dans un congrès hal-01516788v1
Image document

Logic against Ghosts: Comparison of Two Proof Approaches for a List Module

 Allan Blanchard , Nikolai Kosmatov , Frédéric Loulergue
SAC 2019 - The 34th ACM/SIGAPP Symposium On Applied Computing, Apr 2019, Limassol, Cyprus. ⟨10.1145/3297280.3297495⟩
Communication dans un congrès hal-02100515v1
Image document

Towards Formal Verification of Contiki: Analysis of the AES–CCM* Modules with Frama-C

 Alexandre Peyrard , Nikolai Kosmatov , Simon Duquennoy , Shahid Raza
RED-IOT 2018 - Workshop on Recent advances in secure management of data and resources in the IoT, Feb 2018, Madrid, Spain
Communication dans un congrès hal-01670119v1

Structural Testing with PathCrawler: Tutorial Synopsis

 Nicky Williams , Nikolai Kosmatov
2012 12th International Conference on Quality Software, Xi'an, Shaanxi, China, August 27-29, 2012, 2012, Xi'an, China. pp.289--292, ⟨10.1109/QSIC.2012.24⟩
Communication dans un congrès hal-01810295v1
Image document

Runtime assertion checking and static verification: Collaborative partners

 Fonenantsoa Maurica , David R. Cok , Julien Signoles
Lecture Notes in Computer Science, 2018, 11245 (Part 2), pp.75-91. ⟨10.1007/978-3-030-03421-4_6⟩
Article dans une revue cea-04477117v1
Image document

Domestiquer la variété des critères de test avec le langage HTOL et l'outil LTest

 Michaël Marcozzi , Sébastien Bardin , Nikolai Kosmatov , Virgile Prévosto , Mickaël Delahaye
Approches Formelles pour l'Assistance au Développement de Logiciels - AFADL, Jun 2017, Montpellier, France
Communication dans un congrès cea-01835544v1
Image document

CDCL-inspired Word-level Learning for Bit-vector Constraint Solving

 Zakaria Chihani , François Bobot , Sébastien Bardin
2017
Pré-publication, Document de travail hal-01531336v1
Image document

Combining Static Analysis and Test Generation for {C} Program Debugging

 Omar Chebaro , Nikolai Kosmatov , Alain Giorgetti , Jacques Julliand
TAP'10, 4th Int. Conf. on Tests and Proofs, 2010, Spain. pp.94--100
Communication dans un congrès hal-00563308v1
Image document

Online runtime verification competitions: How to possibly deal with their issues (Position paper)

 Julien Signoles
RV-CuBES 2017 - International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools, Sep 2017, Manchester, United Kingdom. ⟨10.29007/44MK⟩
Communication dans un congrès cea-04469431v1
Image document

A Relational Shape Abstract Domain

 Hugo Illous , Matthieu Lemerre , Xavier Rival
NFM 2017 - 9th NASA Formal Methods Symposium, Apr 2017, Moffett Field, United States. pp.212-229, ⟨10.1007/978-3-319-57288-8_15⟩
Communication dans un congrès hal-01648681v1
Image document

Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system

 Ali Assaf , Guillaume Burel , Raphal Cauderlier , David Delahaye , Gilles Dowek , et al.
TYPES: Types for Proofs and Programs, May 2016, Novi SAd, Serbia
Communication dans un congrès hal-01441751v1
Image document

Binsec/Rel: Symbolic binary analyzer for security with applications to constant-Time and secret-erasure

 Lesly-Ann Daniel , Sébastien Bardin , Tamara Rezk
ACM Transactions on Privacy and Security, 2023, 26 (2), pp.11:1-42. ⟨10.1145/3563037⟩
Article dans une revue cea-04228169v1
Image document

ProSpeCT: Provably Secure Speculation for the Constant-Time Policy (Extended version)

 Lesly-Ann Daniel , Marton Bognar , Job Noorman , Sébastien Bardin , Tamara Rezk , et al.
32nd USENIX Security Symposium, USENIX Security 2023, Aug 2023, Anaheim (CA), United States. ⟨10.48550/arXiv.2302.12108⟩
Communication dans un congrès hal-04479531v1
Image document

Moniteur hybride de flux d'information pour un langage supportant des pointeurs

 Mounir Assaf , Julien Signoles , Frédéric Tronel , Eric Totel
[Rapport de recherche] RR-8326, INRIA. 2013, pp.25
Rapport hal-00841048v1
Image document

A tight integration of symbolic execution and fuzzing

 Yaëlle Vinçont , Sébastien Bardin , Michaël Marcozzi
Lecture Notes in Computer Science, 2021, FPS 2021 - The 14th International Symposium on Foundations & Practice of Security, 13291, ⟨10.1007/978-3-031-08147-7_20⟩
Article dans une revue cea-04232795v1
Image document

Real Behavior of Floating Point Numbers

 Bruno Marre , François Bobot , Zakaria Chihani
The SMT Workshop, SMT 2017, 15th International Workshop on Satisfiability Modulo Theories, Jul 2017, Heidelberg, Germany
Communication dans un congrès cea-01795760v1
Image document

Sharpening Constraint Programming approaches for Bit-Vector Theory

 Zakaria Chihani , Bruno Marre , François Bobot , Sébastien Bardin
CPAIOR 2017. International Conference on AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, Jun 2017, Padova, Italy
Communication dans un congrès cea-01795779v1

Tutorial on Automated Structural Testing with PathCrawler - (Extended Abstract)

 Nikolai Kosmatov , Nicky Williams
Tests and Proofs - 6th International Conference, TAP 2012, Prague, Czech Republic, May 31 - June 1, 2012. Proceedings, 2012, Prague, Czech Republic. pp.176, ⟨10.1007/978-3-642-30473-6_16⟩
Communication dans un congrès hal-01810294v1

Generation of All-Paths Unit Test with Function Calls

 Patricia Mouy , Bruno Marre , Nicky Williams , Pascale Le Gall
First International Conference on Software Testing, Verification, and Validation, ICST 2008, Lillehammer, Norway, April 9-11, 2008, 2008, Lillehammer, Norway. pp.32--41, ⟨10.1109/ICST.2008.35⟩
Communication dans un congrès hal-01810199v1
Image document

How testing helps to diagnose proof failures

 Guiillaume Petiot , Nikolaï Kosmatov , Bernard Botella , Alain Giorgetti , Jacques Julliand
Formal Aspects of Computing, 2018, 30 (6), pp.629 - 657. ⟨10.1007/s00165-018-0456-4⟩
Article dans une revue hal-01948799v1
Image document

Hybrid Information Flow Analysis for Real-World C Code

 Gergö Barany , Julien Signoles
TAP 2017 - 11th International Conference on Tests & Proofs, Jul 2017, Marburg, Germany. pp.23-40, ⟨10.1007/978-3-319-61467-0_2⟩
Communication dans un congrès hal-01658653v1
Image document

How Test Generation Helps Software Specification and Deductive Verification in Frama-C

 Guillaume Petiot , Nikolai Kosmatov , Alain Giorgetti , Jacques Julliand
Tests and Proofs, Jul 2014, York, United Kingdom. pp.204 - 211, ⟨10.1007/978-3-319-09099-3_16⟩
Communication dans un congrès hal-01108553v1
Image document

Gagnez sur tous les tableaux

 Richard Genestier , Alain Giorgetti , Guillaume Petiot
Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France
Communication dans un congrès hal-01099135v2
Image document

Relational properties for specification and verification of C programs in Frama-C

 Lionel Blatter
Other. Université Paris Saclay (COmUE), 2019. English. ⟨NNT : 2019SACLC065⟩
Thèse tel-02401884v1
Page :