Anciens exposés
- 21.05.2013 - Julien Signoles (CEA LIST) - Common Specification
Language for Static and Dynamic Analysis of C Programs
- 16.04.2013 - Jean-Yves Marion (LORIA) - On detection
methods and analysis of malware
- 15.03.2013 - John Murray (SRI) - SYSTEMS, GAMES, AND IDENTITY:
New Research Ideas at SRI
- 12.03.2013 - Natarajan Shankar (SRI) - Inference systems and
Architectures
- 26.02.2013 - Guillaume Melquiond (INRIA) - Formal proof of
numerical properties and automation
- 19.02.2013 - Maria Christakis (ETHZ) - Collaborative
Verification and Testing with Explicit Assumptions
- 18.02.2013 - Etienne Lozes (ENS Cachan) - Preuves de programmes à
échanges de messages non copiants dans Heap-Hop
- 13.02.2013 - Benoit Vaugon (ENSTA) - Une théorie relativiste
originale à base de géométrie différentielle
- 28.01.2013 - Loic Correnson (CEA LIST) - Modèles mémoire
pour le C
- 08.01.2013 - Loic Correnson (CEA LIST) - Preprocessing pour
SMT-solveurs
- 18.12.2012 - Jose Pablo Escobedo (CEA LIST) - Off-line test
case generation for timed symbolic model-based conformance
testing
- 14.12.2012 - William Edmonson (North Carolina State University)
& Natasha Neogi (National Institute of Aerospace) - Highly
Confident Reduced Life-Cycle Design Process for Small Satellite
Systems: Methodology and Theory
- 14.12.2012 - Helmut Seidl (Technische Universität München) - How
to
combine widening and narrowing for non-monotonic systems of
equations
- 20.11.2012 - Sébastien Bardin (CEA LIST) - A combined approach
for solving constraints over Finite Domains and Arrays
- 23.10.2012 - François Bobot (LRI) - Réécritures gardées dans le
prouveur SMT CVC4
- 25.09.2012 - Henning Kerstan (Université de Duisbourg / INKO /
TCS)
- Coalgebraic Trace Semantics for Probabilistic Transition Systems
Based on Measure Theory
- 25.09.2012 - Mathieu Lemerre (CEA LIST) - La sécurité système
dans Anaxagoros
- 19.06.2012 - Mounir Assaf (CEA LIST/ LSL) - Analyse de sécurité
de programmes avec pointeurs
- 22.05.2012 - Maria Christofi (Gemalto) - Vérification formelle
d'implémentations cryptographiques
- 10.05.2012 - Mohamed Iguernelala (Paris Sud, LRI) - New
Simplex-Based Procedure For Deciding Quantifier-Free Linear Integer
Arithmetic
- 03.05.2012 - Sylvain Conchon et Alain Mesbout (Paris-Sud, LRI) -
Cubicle: A Parallel SMT-based Model Checker for Parameterized Systems
- 24.04.2012 - Jean-Jacques Lévy (MSR INRIA) - Création de Redexs
et Normalisation Forte dans les calculs typés
- 28.02.2012 - Xavier Rival (INRIA) - Domaines
abstraits pour l'analyse statique de programmes
manipulant des structures de données complexes
- 14.02.2012 - Virgile Prevosto (CEA LIST) - Functional
dependencies of C functions via weakest preconditions
- 24.01.2012 - Jacques Julliand (Uni. Franche-Comté / LIFC) -
Contributions à la génération automatique de tests à partir de critères
de sélection dynamique par abstraction de modèles
- 22.11.2011 - Jörg Brauer (RWTH Aachen University) - Automatic
abstraction for binary code
- 08.11.2011 - Bart Jacobs (Katholieke Universiteit Leuven) -
VeriFast: a Powerful, Sound, Predictable, Fast Verifier for C and Java
- 18.10.2011 - Florent Kirchner (CEA LIST / LSL) - Spécifier et
valider des politiques de copie d'objet
- 22.08.2011 - Mounir Assaf (Supélec) - Utilisation de méthodes
hybrides pour la détection d’intrusion paramétrée par la politique de
sécuritéreposant sur le suivi des flux d’information
- 01.07.2011 - Francois Dupressoir (Microsoft R&D)
- Verification of Security Properties for Real Size C Programs
- 21.06.2011 - Sébastien Bardin (CEA LIST) - Refinement-based CFG
Reconstruction from Unstructured Programs
- 24.05.2011 - Julien Signoles (CEA LIST) - Une bibliothèque de
typage dynamique en OCaml
- 10.05.2011 - Johannes Kinder (EPFL) - Static analysis of x86
Executable Codes
- 26.04.2011 - Benoit Robillard (ENSIIE) - Vérification formelle et
optimisation de l'allocation de registres par coloration de graphes
- 29.03.2011 - Patrice Godefroid (Microsoft R&D) - White-box
Fuzzing for Security Testing
- 15.03.2011 - Simao Mello De Sousa (Uni. Of Beira Interior) -
Certifying Execution Time
- 08.03.2011 - Alexandre Chapoutot (ENSTA) - Interval Slopes an
Abstract Domain for Floating-Point Variables
- 08.02.2011 - Paolo Herms (CEA LIST) - Certification d'un
générateur d'obligations de preuve
- 18.01.2011 - Micaela Mayero et
Franck Butelle (LIPN) - Formal proof of SCHUR conjugate function
- 15.12.2010 - Yassamine Seladji (CEA LIST)
- Accélération du calcul du
point-fixe en interprétation abstraite en utilisant la convergence des
suites numériques
- 15.12.2010 - Hoan Vu (ENSI Bourges) - Gestion de la confiance
dans un réseau ouvert
- 14.12.2010 - Xavier Allamigeon
(INRIA Saclay) - Tropical polyhedra, and application to
abstract interpretation
- 30.11.2010 - Florent Kirchner (INRIA) - Systèmes de preuve
conjugués
- 23.11.2010 - Damien Doligez (INRIA), Stefan Merz (INRIA) - TLAPS
-- The TLA Proof System
- 26.10.2010 - Johan Oudinet, Sylvain Peyronnet (LRI)
- Coverage-biased random exploration of large models and
application to testing
- 19.10.2010 - Stefan Schwoon
(LSV) - Verification of Java programs using Moped.
- 28.09.2010 - Burkhart Wolff (LRI) - On Theorem Prover-based Testing
- 22.06.2010 - Loïc Correnson (CEA LIST/LSL) - Preuves et Modèles
Mémoires dans Frama-C
- 08.06.2010 - Loïc Correnson (CEA LIST/LSL) -Analyse multi-thread dans Frama-C
- 02.06.2010 - Loïc Correnson (CEA LIST/LSL) - Preuves et Modèles
Mémoires dans Frama-C
- 01.06.2010 - Christophe Junke (CEA LIST / LSL)
- Handling state Machine specifications with GATeL
- 27.04.2010 - Dumitru Ceara (Verimag) - Taint
Dependency Sequences: a characterization of insecure execution paths
based on input-sensitive cause sequences
- 20.04.2010 - Sébastien Bardin (CEA LIST / LSL) - An
Alternative to SAT-based Approaches for Bit-Vectors
- 13.04.2010 - Yann Thierry-Mieg (Paris 6 / LIP6)
- Hierarchical Set Decision Diagrams: Une structure de données
efficace pour le model-checking
- 06.04.2010 - Nicky Williams (CEA LIST / LSL) - Abstract
Path Testing with PathCrawler
- 30.03.2010 - Virgile Prevosto (CEA LIST / LSL) -
Accessibilité d'un état avec Frama-C et PathCrawler
- 02.03.2010 - Omar Chebaro (CEA LIST / LSL) - Combining
Static Analysis and Test Generation for C Program Debugging
- 16.02.2010 - Jean Fortin (Paris 12 / LACL) - BSP-Why : un
langage intermédiaire pour la vérification formelle de programmes
parallèles BSP
- 26.01.2010 - Peter Habermehl (Paris 7) - Automatic Verification
of Integer Array Programs.
- 21.01.2010 - Jules Villard (ENS Cachan) - Proving Copyless
Message Passing.
- 08.12.2009 - Yannick Moy
(AdaCore) - Hi-Lite: High Integrity Lint Integrated with Testing
and Execution.
- 01.12.2009 - Mickael Delahaye (CEA LSL) - Généralisation de
chemins infaisables à partir d'explication
- 17.11.2009 - Richard Lassaigne
(Equipe de Logique mathématique, Paris 7) - Vérification probabiliste
et Approximation
- 10.11.2009 - Alain Frisch (Lexifi) - OCaml chez Lexifi
- 20.10.2009 - Etienne André
(LSV) - Synthèse de contraintes pour la généralisation
d'un comportement de référence dans les automates
temporisés paramétrés
- 06.10.2009 - Ali Ayad (CEA LSL)
- Étude du comportement des nombres flottants dans les programmes
C
- 09.06.2009 - Jonathan-Christofer
Demay (Supelec Rennes) - Instrumentation des programmes C
pour la detection d'intrusion
- 12.05.2009 - Florence charreteur
(IRISA) - Raisonnement à contraintes pour le test de
bytecode Java
- 28.04.2009 - Benjmain
Blanc (CEA LSL) - Everything about Gatel
- 21.04.2009 - Pierre Weis (INRIA Rocquencourt) - Moca:
un compilateur de types relationnels
- 14.04.2009 - Emmanuel
Haucourt (CEA Measi) - Pourquoi et comment une machine
manipule-t-elle certaines catégories
- 07.04.2009 - Nicky Williams (CEA LSL) - Test Generation
Strategies to Measure Worst-Case Execution Time
- 17.03.2009 - Sébastien
Bardin (CEA LSL) - Pruning the Search Space in Path-Based Test
Generation
- 03.03.2009 - Tayssir
Touili (LIAFA) - SPADE: verification of multithreaded
dynamic and recursive programs
- 10.02.2009 - Damien
Doligez (INRIA Rocquencourt) - Pointeurs faibles et
hash-consing dans OCaml
- 20.01.2009 - Sylvie
Putot (CEA Measi) - Sur et sous approximation pour
l'analyse statique de programmes numériques dans FLUCTUAT
- 13.01.2009 - Virgile
Prevosto (CEA LSL) - ACSL, un langage de spécification
pour le C
- 16.12.2008 - Julien
Signoles (CEA LSL) - Analyse des applications sécuritaires
avec Frama-C
- 12.12.2008 - Florent
Bouchy (LSV) - Reachability in Timed Counter Systems
- 09.12.2008 - Richard Bonichon
(CEA LSL) - Tableaux
et déduction modulo
- 28.10.2008 -
Nikolaï Kosmatov (CEA LSL) - Le traitement des alias internes
dans un algorithme de génération de tests à la PathCrawler