Séminaires Verimag

Si vous souhaitez être informé par courriel des annonces de séminaires, contactez Sylvain Boulmé.

Pour planifier un séminaire, les membres du laboratoire sont invités à remplir le formulaire en ligne. Les autres peuvent contacter Sylvain Boulmé.

 /  ICAL

Séminaires à venir

• 28 novembre 2024 - 14h00: Room 206 (2nd floor, badged access)
  par Grégoire BUSSONE de ENS, équipe Parkas (Inria-ENS) : Réduire les copies et l'utilisation mémoire dans les langages synchrones
  
• 2 décembre 2024 - 14h00: Amphitéatre MJK
  par Thomas Vigouroux de Verimag : Analyses quantitatives pour les attaquants adaptatifs (Thesis)
  
• 12 décembre 2024 - 14h00: Room 206 (2nd floor, badged access)
  par Lucas Bueri de Verimag : tba (Thesis)
  
• 12 décembre 2024 - 14h00: GIPSA-Lab , Salle JM Chassery, 11 rue des Maths
  par Bob AUBOUIN-PAIRAULT de Université Grenoble Alpes, VERIMAG, GIPSA-Lab : tba (Thesis)
  

Séminaires passés

• 20 novembre 2024 - par Chao Huang de University of Southampton, UK : Safe Reinforcement Learning with Verification in the Loss
• 14 novembre 2024 - par Lisa Maile de TU Braunschweig (Germany) : Real-Time Communication with Dynamic Network Traffic using Time-Sensitive Networking
• 7 novembre 2024 - par Aurèle Barrière de EPFL : Formal Verification Beyond Traditional Compilation
• 27 juin 2024 - par Nicolas Chappe de ENS-Lyon, LIP, CASH : Executable semantics based on Choice Trees for a concurrent subset of LLVM IR
• 19 juin 2024 - par Jean-François MONIN de Verimag, Polytech Grenoble. : Recent advances on the Braga method
• 18 juin 2024 - par Matthieu Sozeau de Inria (Galinette), Université de Nantes : Verified Extraction from Coq to OCaml
• 17 juin 2024 - par Sylvain BOULME de Verimag, Grenoble-INP Ensimag : Toward a FFI (Foreign Function Interface) for embedding untrusted imperative OCaml into Coq-verified computations.
• 17 juin 2024 - par Basile GROS de Verimag, UGA : Small Inversions in Coq
• 30 mai 2024 - par Mohamed Maghenem de CNRS, GIPSA-lab, Grenoble : A Hybrid-Systems Framework for Distributed Gradient-Based Estimation
• 16 mai 2024 - par Gaiyun Liu de GREAH : Modeling, analysis, and supervisory control of networked discrete event systems
• 2 mai 2024 - par Matthieu Moy de Univ. Lyon 1 - LIP (CASH) : How to Build a Broken System?
• 18 avril 2024 - par Akram Idani de LIG (Vasco), Ensimag : Formal Model-Driven Engineering
• 15 avril 2024 - par Subhajit Roy de Indian Institute of Technology Kanpur : Satisfiability modulo fuzzing: a synergistic combination of SMT solving and fuzzing
• 11 avril 2024 - par Andrei Paskevich de Univ. Paris-Saclay (LMF) - Inria Saclay (Toccata) : Coma: an intermediate verification language with explicit abstraction barriers
• 4 avril 2024 - par Sébastien Michelland de LCIS (UGA) : Abstract Interpreters: a Monadic Approach to Modular Verification
• 14 mars 2024 - par Adel NOUREDDINE de University of Pau, laboratoire LIUPPA : Observing energy consumption: from hardware to software source code
• 13 mars 2024 - par Inigo Incer de CalTech and UC Berkley : Towards Provably Safe and Secure Systems with Contract-Based Design
• 7 mars 2024 - par Sylvain Boulmé de Verimag, Grenoble-INP Ensimag : Développement logiciel formellement vérifié: pourquoi et comment ?
• 22 février 2024 - par Paolo Ballarini de CentraleSupélec - MCIS : Hybrid-Automata Specification Language: from expressive stochastic model checking to parametric stochastic model checking
• 12 février 2024 - par Aina Rasoldier de Inria : Comment évaluer le potentiel d'une solution numérique face à l'urgence écologique ? Application aux plateformes de covoiturage régulier à l'échelle locale (Thesis)
• 8 février 2024 - par Sophie Morel de CNRS - ENS-Lyon : Formalisation d'un objet geometrique dans l'assistant de preuve Lean: le cas des grassmanniennes.
• 14 décembre 2023 - par Alessandro De Palma de INRIA : From Neural Network Verification to Efficient Robust Training
• 12 décembre 2023 - par Leo Gourdin de VERIMAG : Validation Formelle de Transformations Intra-Procédurales par Simulation Symbolique Défensive (Thesis)
• 30 novembre 2023 - par Yutaka Nagashima de Huawei Technologies R&D (UK) : AI-Enhanced Theorem Proving: Tactical Approaches for Induction Problems
• 17 novembre 2023 - par Thomas Mari de VERIMAG (MOHYTOS), INRIA (SPADES) : Explications causales pour les systèmes temps réel réactifs (Thesis)
• 9 novembre 2023 - par Gidon Ernst de Ludwig-Maximilians-University of Munich : Automating software verification with respect to strong specifications
• 19 octobre 2023 - par Michael Foster de University of Sheffield : Active Inference of Extended Finite State Machines Without Reset
• 12 octobre 2023 - par Nicola Gigante de Free University of Bozen-Bolzano, Italy : Temporal Logics Modulo Theories for Infinite-State Verification
• 12 juillet 2023 - par Dejan Nickovic de AIT, Vienna : Attribute Repair for Threat Prevention
• 7 juillet 2023 - par Akshay Mambakam de VERIMAG, Université Grenoble Alpes : Parametric timed formalisms for specification and monitoring (PhD defense) (Thesis)
• 6 juillet 2023 - par Nicola Paoletti de King's College London : Causal Temporal Reasoning for Markov Decision Processes
• 30 juin 2023 - par Sayan Mitra de University of Illinois Urbana-Champaign : Assuring Safety of Learning-Enabled Systems with Perception Contracts.
• 9 juin 2023 - par Jean-Luc Scharbarg de IRIT : Trends in real-time embedded networks: towards TSN
• 9 juin 2023 - par claire maiza de GrenobleINP/ Ensimag, Verimag : Analyses matérielles et logicielles pour obtenir une analyse temporelle précise et efficace (HDR)
• 8 juin 2023 - par Basile Pesin de Inria PARKAS - ENS-Ulm : Verifying a compiler for a synchronous dataflow language with state machines in Coq
• 25 mai 2023 - par Henri-Pierre Charles de CEA, Grenoble : Spécialisation de code binaire au run-time : pour gagner du temps et de l'énergie, il faut rouler à l'HybroGen
• 4 mai 2023 - par Joseph Sifakis de VERIMAG : Artificial Intelligence and autonomous systems
• 28 avril 2023 - par Thomas Jensen de INRIA : An information flow logic based on partial equivalence relations
• 28 avril 2023 - par Etienne Boespflug de Vérimag : Outils pour l’analyse de code et de contre-mesures pour l'injection de fautes multiples (Thesis)
• 9 mars 2023 - par Clementine Gritti de University of Canterbury -- New Zealand : Internet of Things: From modern cryptography to post-quantum cryptography
• 6 mars 2023 - par Frederic Fort de IRT Saint Exupery : Programing adaptive real-time systems
• 2 mars 2023 - par Arthur Perais de TIMA : Exploring Instruction Fusion Opportunities in General Purpose Processors
• 23 février 2023 - par Léo Robert de LIMOS (Université Clermont Auvergne) : How fast do you heal? A taxonomy for post-compromise security in secure-channel establishment.
• 23 février 2023 - par Imen Sayar de IRIT-SM@RT : Collaborative development of safe and secure cyber-physical systems
• 20 février 2023 - par anais durand de univ. clermont auvergne : Exploration of 3D environments by swarms of luminous autonomous robots.
• 6 février 2023 - par Bruno FERRES de LIP (equipe CASH) : Using Model Checking for Electrical Rule Checking of Integrated Circuits at Transistor Level
• 2 février 2023 - par Charlie Jacomme de Team Prosecco of Inria Paris : A comprehensive, formal and automated analysis of the EDHOC protocol.
• 26 janvier 2023 - par Son Ho de Team Prosecco of Inria Paris : Aeneas: Rust Verification by Functional Translation
• 16 décembre 2022 - par Vincent Morice de STMicroelectronics : Modèle haut niveau de microcontrôleurs basé sur les dépendances pour le développement de logiciel embarqué (Thesis)
• 13 décembre 2022 - par Ezio Bertocci de TU Wien : Automatic Invariant Generations for Probabilistic Loops
• 8 décembre 2022 - par Kohei SUENAGA de Kyoto University : Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption
• 24 novembre 2022 - par Xavier Denis de LRI : Deductive Verification of Higher-Order Rust Programs
• 24 novembre 2022 - par Jean-François Monin de VERIMAG : Programmation récursive en Coq et intensionalité : oh le beau cas !
• 17 novembre 2022 - par Arnaud Sangnier de IRIF : Parameterized verification of Networks with selective broadcast
• 10 novembre 2022 - par Stephan Plassart de LCA2 EPFL : Equivalent Versions of Total Flow Analysis
• 27 octobre 2022 - par Hugo Gimbert de CNRS (LaBRI) : Les algorithmes de ParcourSup
• 29 septembre 2022 - par Merigoux Denis de INRIA Prosecco : Rules, Computation and Politics: Scrutinizing Unnoticed Programming Choices in French Housing Benefits
• 9 septembre 2022 - par Lucas Bueri de Verimag : On an Invariance Problem for Parameterized Concurrent Systems
• 12 juillet 2022 - par Dejan Nickovic de AIT Vienna : Information-flow Interfaces
• 7 juillet 2022 - par Franz Meyer de Universidad ORT Uruguay : Towards Efficient Active Learning of PDFA
• 21 juin 2022 - par Joel Goossens de ULB, Brussels : Real-Time Computing, Multiprocessor scheduling problems
• 16 juin 2022 - par Joel Goossens de ULB, Brussels : Periodicity of real-time priority driven schedulers with preemption delay on uniprocessor
• 14 juin 2022 - par Joel Goossens de ULB, Brussels : Real-Time Computing, foundation
• 3 juin 2022 - par CAPITAL Workshop de sCalable And PrecIse Timing AnaLysis for multicore : Workshop CAPITAL 2022 : sCalable And PrecIse Timing AnaLysis for multicore platforms
• 31 mai 2022 - par Matheus Schuh de Verimag / Kalray : Safe Implementation of Hard Real-Time Applications on Many-Core Platforms (Thesis)
• 5 mai 2022 - par Nathalie Bertrand de INRIA Rennes : Reconfigurable Parameterized Broadcast Networks: Minimal Size and Execution Length for Coverability
• 7 avril 2022 - par Benedikt Bollig de LSV, ENS Saclay : Identifiers in Registers - Describing Network Algorithms with Logic
• 24 mars 2022 - par David Monniaux de VERIMAG : The trusted computing base of the CompCert verified compiler
• 10 mars 2022 - par Paolo Torrini de Inria Sardes : A CompCert Backend with Symbolic Encryption
• 3 mars 2022 - par Xiaowei Huang de University of Liverpool : Machine Learning Safety
• 13 janvier 2022 - par Benjamin BLANC de Prover Tech : Formal Methods in Practice: Model Checking in the Railway Industry
• 13 décembre 2021 - par Joseph Sifakis de VERIMAG : Specification and Validation of Autonomous Driving Systems: A Multilevel Semantic Framework
• 7 décembre 2021 - par Alessio Mansutti de University of Oxford : Efficient complementation of semilinear sets and the VC dimension of Presburger arithmetic
• 3 décembre 2021 - par Miriam Garci­a de Institute of Science and Technology (IST) of Austr : Design, Verification and Synthesis of Hybrid Systems.
• 2 décembre 2021 - par Leo Exibard de Reykjavik University : Reactive Synthesis over Infinite Data Domains with Machines with Registers
• 29 novembre 2021 - par Nicolas Basset de VERIMAG : Uniform Sampling for Networks of Automata
• 23 novembre 2021 - par PIERRE-LEO BEGAY de Orange Labs & Verimag : Conception, développement et certification dans Coq/MathComp d'optimisations Datalog pour la vérification réseau (Thesis)
• 4 octobre 2021 - par Hadi DAYEKH de VERIMAG, UGA : Learning Automata over Large Alphabets as an Alternative to Recurrent Neural Networks
• 27 septembre 2021 - par Sylvain Boulmé de Verimag : Formally Verified Defensive Programming (efficient Coq-verified computations from untrusted ML oracles) (HDR)
• 20 septembre 2021 - par Lucas Bueri de VERIMAG : Décidabilité de la rationalité des VAS
• 30 août 2021 - par Yannick Zakowski de LIP : Sémantique de Vellvm
• 13 juillet 2021 - par Cyril Six de Kalray & Verimag : Compilation optimisante et formellement prouvée pour un processeur VLIW (Thesis)
• 17 juin 2021 - par Pierre Courtieu de CNAM-CEDRIC : [FormalProofs] Gestion d'un environment de preuve moche
• 10 juin 2021 - par Jean-François Monin de Verimag : [FormalProofs] Petites inversion et récursion débridée en Coq, la méthode de Braga
• 23 avril 2021 - par Schoitsch Erwin de AIT Austrian Institute of Technology : Ethical aspects and recommendations for trustworthy highly automated/autonomous systems
• 1er avril 2021 - par Lionel Rieg de VERIMAG / IIM Grenoble INP : [FormalProofs] A formally-verified compiler from Esterel to circuits
• 11 mars 2021 - par David Monniaux de Verimag : [SharedResources] CompCert for Risc-V on FPGA
• 26 février 2021 - par Emma AHRENS de Verimag, Mohytos : Local Reasoning for Reconfigurable Distributed Systems
• 25 février 2021 - par Cyril SIX de Kalray / Verimag : Certified Superblock Scheduling for the CompCert Compiler
• 11 février 2021 - par Franck POMMEREAU de University of Évry : Formal Modelling and Symbolic Analysis of Ecosystems
• 28 janvier 2021 - par Etienne André de Université de Lorraine : Symbolic Monitoring against Specifications Parametric in Time and Data
• 21 janvier 2021 - par Etienne Andre de Université de Lorraine : Symbolic Monitoring against Specifications Parametric in Time and Data
• 14 janvier 2021 - par Olivier RIDOUX de IRISA, Université de Rennes I : Limite de Landauer et calcul réversible : une introduction
• 18 décembre 2020 - par Guo Xiaojie de INRIA/VERIMAG : Certified Tools for Schedulability Analyses (Thesis)
• 17 décembre 2020 - par Stéphane Devismes de UGA/VERIMAG : Versatility and Efficiency in Self-Stabilizing Distributed Systems (HDR)
• 11 décembre 2020 - par Marius Bozga de VERIMAG : Compositional Generation of Invariants for Timed Systems
• 3 décembre 2020 - par Jacques Combaz de CNRS / VERIMAG / ETiCS : Introduction aux effets rebond [lien visio: https://veri-bbb.imag.fr/b/jac-lxa-inn-hnq]
• 20 novembre 2020 - par Radu Iosif de VERIMAG/CNRS : Structural Invariants for the Verification of Systems with (Recursively Defined) Parameterized Architectures
• 19 novembre 2020 - par Aina Rasoldier de INRIA / Spades - VERIMAG / ETiCS : Les méthodologies d'évaluation des impacts environnementaux des technologies de l'information et de la communication (TIC) à l'échelle mondiale
• 17 novembre 2020 - par Schuh Matheus de Kalray/Verimag : A study of predictable execution models implementation for industrial data-flow applicationson a multi-core platform with shared banked memory
• 6 novembre 2020 - par Akshay Mambakam de VERIMAG : Learning Specifications for Labelled Patterns
• 22 octobre 2020 - par Cyril Six de Kalray - Verimag : Certified and Efficient Instruction Scheduling. Application to Interlocked VLIW Processors.
• 30 juin 2020 - par Sébastien Michelland de ENS de Lyon : Une Procédure de Décision pour les Relations d'Équivalence
• 12 mars 2020 - par Mathias RAMPARISON de University of Luxemburg : Updatable Parametric Timed Automata: Decidability, Algorithms, and Application to Security
• 9 mars 2020 - par Rémy Boutonnet de VERIMAG : Modular Analysis of Numerical Properties by Abstract Interpretation (Thesis)
• 21 février 2020 - par Michael Marcozzi de Imperial College (London) : Compiler Fuzzing: How Much Does It Matter?
• 13 février 2020 - par Jonathan Salwan de Quarkslab : L'exécution symbolique pour l'aide à la rétro-ingénierie dans un cadre industriel (Thesis)
• 12 février 2020 - par Sébastien Bardin de CEA-LIST : From Safety to Security: The Case of Binary-level Code Analysis
• 6 février 2020 - par Jules Chouquet de IRIF : Lower bounds for probabilistic k-set agreement through combinatorial topology
• 3 février 2020 - par Matthieu Jan and Asavoae Mihail de CEA : Towards Automatic Extraction of Timing models from HDL designs (Mihail Asavoae) - Tracking timing anomalies (Matthieu Jan)
• 27 janvier 2020 - par Xiao XU de VERIMAG : Thesis Defence - Xiao XU - Generalisation of Alternating Automata over Infinite Alphabets (Thesis)
• 27 janvier 2020 - par Margus Veanes de Microsoft Research Lab : Symbolic Regexes & Matching
• 19 décembre 2019 - par Yannick Zakowski de University of Pennsylvania : From representing recursive and impure programs in Coq to a modular formal semantics of LLVM IR
• 19 décembre 2019 - par Hang Yu de VERIMAG : Towards an Efficient Parallel Parametric Linear Programming Solver (Thesis)
• 25 novembre 2019 - par Moshe Vardi de Rice University : Technology is Driving the Future, But Who Is Steering?
• 21 novembre 2019 - par Sophie Tourret de Max-Planck-Institut für Informatik, Saarbrücken : Stronger Higher-order Automation
• 10 octobre 2019 - par Jan Reineke de Universität des Saarlandes : Spectector: Principled detection of speculative information flows
• 8 octobre 2019 - par Valentin TOUZEAU de Verimag : Static Analysis of Least Recently Used Caches: Complexity, Optimal Analysis, and Applications to Worst-Case Execution Time and Security (Thesis)
• 26 septembre 2019 - par Pierre-Jean Meyer de University of California, Berkeley : Reachability analysis and decompositions for abstraction-based control synthesis
• 20 septembre 2019 - par -- Oded Maler Memorial Day de Organized by VERIMAG : Oded Maler Memorial Day
• 19 septembre 2019 - par Martin Franzle de Carl von Ossietzky Universitat Oldenburg, Germany : What’s to Come is Still Unsure: Automatically Synthesizing and Verifying Controllers Resilient to Delayed Interaction
• 11 juillet 2019 - par Eric Gascard de SCOP, Polytech Grenoble : Quantitative Analysis of Dynamic Fault Trees by means of Monte Carlo Simulations: Event-Driven Simulation Approach
• 9 juillet 2019 - par Lionel Rieg de VERIMAG : Integrating Formal Schedulability Analysis into a Verifed OS Kernel
• 4 juillet 2019 - par Radu IOSIF de VERIMAG : Alternating Automata Modulo First Order Theories
• 2 juillet 2019 - par Indranil Saha de IIT Kanpur, India : Developing Autonomous Multi-Robot Systems for Complex Missions
• 28 juin 2019 - par Braham Lotfi Mediouni de Verimag (RSD) : Modeling and Analysis of Stochastic Real-Time Systems (Thesis)
• 26 juin 2019 - par Rany Kahil de Verimag, Université Grenoble Alpes : Schedulability in Mixed- criticality Systems (Thesis)
• 25 juin 2019 - par Hernan Ponce de Leon de Fortiss, Munich, Germany : BMC with Weak Memory Models
• 14 juin 2019 - par Benoit Barbot de LACL, Universite Paris Est, Creteil : Cosmos a quantitative verification tool for large stochastic systems
• 13 juin 2019 - par Simon IOSTI de Verimag : Using neural networks to improve performances of correct-by-construction controllers
• 9 mai 2019 - par Saddek Bensalem de Verimag : Engineering Trustworthy Learning-Enabled Autonomous Systems
• 2 mai 2019 - par Michael PERIN de Verimag / UGA : Découvrir AMC en 45 Questions a Choix Multiples
• 29 avril 2019 - par Invited Speakers de Onera, Kalray, INRIA, Verimag ... : Journée thématique Verimag : Many-core Kalray MPPA, implementation and verification
• 5 avril 2019 - par Radu IOSIF de VERIMAG : On the Expressive Completeness and Complexity of Prenex Separation Logic
• 4 avril 2019 - par Radu IOSIF de VERIMAG : Checking Deadlock-Freedom of Parametric Component-Based Systems
• 1er avril 2019 - par Edward A. Lee de UC Berkeley : Living Digital Beings
• 28 mars 2019 - par Olivier VIDAL de ISTerre, Universite Grenoble-Alpes : Matières premières et énergie à l’échelle mondiale dans le contexte de la transition énergétique
• 20 mars 2019 - par Rim El Ballouli de Universite Grenoble Alpes : Modeling Self-configuration in Architecture-based Self-adaptive systems (Thesis)
• 8 mars 2019 - par Mathias Bourgoin de Nomadic Labs : An overview of the Tezos blockchain
• 22 février 2019 - par Moustapha Lo de Verimag : Implementing a Real-time Avionic application on a Manycore Processor (Thesis)
• 18 février 2019 - par Guillaume Baudart de IBM T. J. Watson Research Center, Yorktown Heights : Probabilistic Reactive Programming
• 14 février 2019 - par Nikos Gorogiannis de Facebook : Concurrency bug detection at scale with Infer
• 7 février 2019 - par Jacques COMBAZ de CNRS, Verimag : L'assemblage des composants en BIP
• 25 janvier 2019 - par Tom Yamaguchi de TOYOTA : Application of Abstract Interpretation to the Automotive Electronic Control System
• 24 janvier 2019 - par Maiza Claire de VERIMAG : WCET and interference analysis for multicore systems
• 22 janvier 2019 - par Georg Struth de University of Sheffield : Verifying Hybrid Systems with Modal Kleene Algebra
• 21 janvier 2019 - par Sergio Yovine de Universidad ORT Uruguay : Formal specification and implementation of an automated pattern-based parallel-code generation framework
• 18 janvier 2019 - par Chi-Hong Cheng de Fortiss : When neural networks meet dependability
• 17 janvier 2019 - par Paolo Torrini de Verimag / PACSS : Reifying and translating a monadic fragment of Gallina
• 8 janvier 2019 - par Michal Valko de SequeL, Inria Lille - Nord Europe : The power of graphs in speeding up online learning and decision making
• 7 janvier 2019 - par Michal Valko de SequeL, Inria Lille - Nord Europe : A simple parameter-free and adaptive approach to optimization under a minimal local smoothness assumption
• 19 décembre 2018 - par Khalil Ghorbal de INRIA : Simulating and Verifying Cyber-Physical Systems: Current Challenges and Novel Research Directions
• 17 décembre 2018 - par NIKOLAOS KEKATOS de Verimag Laboratory, University of Grenoble Alpes : Vérification formelle des systèmes cyber-physiques dans le processus industriel de la conception basée sur modèle (Thesis)
• 11 décembre 2018 - par Bibek Kabi de LIX : Combining Zonotope Abstraction and Constraint Programming for Synthesizing Inductive Invariants
• 6 décembre 2018 - par Joseph Sifakis de Verimag : On the Nature of Autonomy: A Rigorous Architectural Characterization
• 29 novembre 2018 - par Sylvain Boulmé de Verimag : Importation d'oracles ML impératifs dans du code Coq vérifié
• 22 novembre 2018 - par analyse et verif. legeres Une journee de reflexion de 5 exposes 10h - 16h30 : Techniques d'analyse et de verification legeres
• 16 novembre 2018 - par Amaury Graillat de VERIMAG/KALRAY : Parallel Code Generation of Synchronous Programs for a Many-core Architecture (Thesis)
• 31 octobre 2018 - par Mahieddine DELLABANI de Verimag : Formal Methods for Distributed Real-Time Systems (Thesis)
• 23 octobre 2018 - par Thusitha Asela Bandara de Verimag : Un protocole de charge adaptatif pour les batteries Lithium-lon
• 11 octobre 2018 - par Florent Chevrou de IRIT : Formalisation of Asynchronous Interactions
• 4 octobre 2018 - par Erwan Jahier de verimag : [Technical Seminar] A gentle introduction to Gitlab-CI and docker
• 20 septembre 2018 - par Cyril Six de Kalray & Verimag : Compilateur CompCert certifié pour processeur VLIW Kalray
• 13 septembre 2018 - par Franz Mayr de Universidad ORT Uruguay : Regular inference on artificial neural networks
• 25 juin 2018 - par Stefano Berardi de University of Torino : Martin-Lof's Inductive Definitions Are Not Equivalent to Cyclic Proofs
• 22 juin 2018 - par Pallab Dasgupta de IIT Kharagpur : Verification challenges in the Power Management fabric of Integrated Circuits
• 31 mai 2018 - par Cristina Serban de VERIMAG, Université Grenoble Alpes : Raisonnement automatisé pour la Logique de Séparation avec des définitions inductives (Thesis)
• 17 mai 2018 - par Michael PERIN de VERIMAG / Université Grenoble-Alpes : Automatic Grading: take a CEGAR and let the machine do your work
• 16 mai 2018 - par Arvind Adimoolam de VERIMAG : A Calculus of Complex Zonotopes for Computing Invariants of Affine Hybrid Systems (Thesis)
• 15 mai 2018 - par Luc Jaulin de Lab-STICC, ENSTA-Bretagne : Computing inner and outer approximations of forward reach sets of a nonlinear dynamical system
• 7 mai 2018 - par Alexandre Rocca de Verimag : Méthodes formelles pour la modélisation et la validation de modèles biologiques (Thesis)
• 17 avril 2018 - par Jim Kapinski de TEMA Toyota, USA : Verification of Learning-Enabled, Cyber-Physical Systems
• 12 avril 2018 - par Maria Méndez Real de ATER IETR Nantes - équipe SYSCOM : Cache-based attacks and spatial isolation countermeasure on multi and many-core architectures
• 22 mars 2018 - par Guilhem Jaber de ENS Lyon/LIP Plume : Model-checking contextual equivalence of higher-order programs with references (candidat poste MCF)
• 22 mars 2018 - par Anastasia Volkova de LIP, ENS de Lyon : Towards reliable implementation of digital filters. How digital signal processing and computer arithmetic meet (candidate poste MCF)
• 19 mars 2018 - par Benjamin Farinier de CEA_LIST-SaClay : Model Generation for Quantified Formulas: A Taint-Based Approach
• 15 mars 2018 - par Ayoub Nouri de VERIMAG : ASTROLABE: A Rigorous Approach for System-Level Performance Modeling and Analysis (candidat poste MCF)
• 15 mars 2018 - par Lionel Rieg de Yale University : Extending a verified OS kernel for real-time
• 8 mars 2018 - par Ivan Gazeau de LORIA, Nancy : Automated verification of privacy-type properties for security protocols (MCF Candidate)
• 15 février 2018 - par Gheorghe Stefanescu de University of Bucharest : Adaptive systems made by self-assembling heterogeneous components within regular 2D patterns
• 5 février 2018 - par Maxime Puys de Verimag : Sécurité des systèmes industriels : filtrage applicatif et recherche de scénarios d’attaques (Thesis)
• 18 janvier 2018 - par David Monniaux de CNRS / VERIMAG : SPECTRE + MELTDOWN
• 15 janvier 2018 - par Dogan Ulus de Verimag / UGA : Filtrage par Motif Temporisé: Théorie et Applications (Thesis)
• 21 décembre 2017 - par Mirco Giacobbe de IST Austria : Counterexample-guided Refinement of Template Polyhedra
• 11 décembre 2017 - par Denis Becker de Verimag / STMicroelectronics : Simulation SystemC/TLM Parallèle de Composants Matériels Décrits pour la Synthèse de Haut Niveau (Thesis)
• 11 décembre 2017 - par Alexandre Maréchal de Verimag : New Algorithmics for Polyhedral Calculus via Parametric Linear Programming (Thesis)
• 7 décembre 2017 - par De Oliviera Steven de CEA-List/Verimag : Synthesizing Invariants by Solving Solvable Loops
• 1er décembre 2017 - par Reineke Jan de Saarland University : On the Smoothness of Paging Algorithms
• 1er décembre 2017 - par Hamza RIHANI de Univ. Grenoble Alpes / Verimag : Analyse temporelle des systèmes temps-réels sur architectures pluri-cœurs avec application à un processeur industriel (Thesis)
• 23 novembre 2017 - par Joseph Sifakis de VERIMAG : How Much Hard is System Design?
• 20 octobre 2017 - par Franck De Goer de LIG/VASCO et VERIMAG/PACSS : Rétro-ingénierie de programmes binaires en une exécution - une analyse dynamique légère basée au niveau des fonctions (Thesis)
• 19 octobre 2017 - par de : COQ en STOCK
• 10 octobre 2017 - par Irini Eleftheria Mens de Verimag, Université Grenoble Alpes : Learning Regular Languages over Large Alphabets (Thesis)
• 10 octobre 2017 - par Frits Vaandrager de Radboud University, Netherlands : Learning Mealy Machines with Timers
• 28 septembre 2017 - par Adrien Guatto de Inria : A Functional Language with Time Warps
• 14 septembre 2017 - par Joël Goossens de Université libre de Bruxelles : Feasibility & Simulation Intervals of Schedules for Recurrent Real-Time Tasks
• 1er septembre 2017 - par Anaïs Durand de Verimag : Algorithmes distribués efficaces adaptés à un contexte incertain (Thesis)
• 31 août 2017 - par : Workshop ESTATE/VERIMAG Distributed Algorithms
• 12 juillet 2017 - par Manuel Barragan de TIMA : Feature selection and design for machine learning-based test of analog, mixed-signal and RF circuits
• 26 juin 2017 - par Hosein Nazarpour de Verimag : Surveillance de systèmes à composants multi-threads et distribués (Thesis)
• 8 juin 2017 - par Assalé ADJE de Université de Perpignan : Itérations sur les politiques pour la vérification de systèmes dynamiques en temps discret.
• 6 juin 2017 - par Laurent Lemke de UGA : Modèles partagés et infrastructure ouverte pour l’internet des objets de la ville intelligente (Thesis)
• 10 mai 2017 - par Yuliia Romenska de Univ. Grenoble Alpes : Composants abstraits pour la vérification fonctionnelle des systèmes sur puce (Thesis)
• 20 avril 2017 - par Vincent Penelle de Universite de Varsovie : On the context-freeness problem for vector addition systems. (candidat MCF)
• 19 avril 2017 - par Liliana Andrade de Verimag : High Level Modeling and Simulation of Heterogeneous Systems: A focus on the SystemC-AMS Synchronization Problem
• 11 avril 2017 - par Iulia Dragomir de Verimag : Compositional Design and Analysis of Embedded Systems
• 30 mars 2017 - par Helmut Seidl de Technische Universitaet Muenchen : Enforcing Termination of Interprocedural Analysis
• 30 mars 2017 - par Dirk Beyer de Ludwig-Maximilians-Universitaet Muenchen : Correctness Witnesses: Exchanging Verification Results between Verifiers
• 29 mars 2017 - par Josselin FEIST de VERIMAG / PACSS : Finding the Needle in the Heap: Combining Binary Analysis Techniques to Trigger Use-After-Free (Thesis)
• 29 mars 2017 - par Egor Karpenkov de VERIMAG : Finding Inductive Invariants using SMT Solving and Convex Optimization (Thesis)
• 28 mars 2017 - par Nikolaj Bjorner de Microsoft Research : Network Verification for Microsoft Azure
• 23 mars 2017 - par Romaric Ludinard de ENSAI : Bitcoin, la blockchain et le problème de la double dépense : état des lieux et analyse de propositions d'améliorations
• 23 mars 2017 - par Hugues Evrard de Imperial College, London : Automated generation of a distributed implementation from a formal model of concurrent processes interacting via multiway rendezvous.
• 16 mars 2017 - par Manuel Selva de Inria : Exécution efficace sur machine multi-cœur
• 9 mars 2017 - par Arthur Milchior de Université Paris Diderot IRIF : Deterministic Automaton and logically definable sets of numbers.
• 9 mars 2017 - par Lionel Rieg de Yale university, Flint group : Formal Proofs of Safety in Coq: Mobile Robot Networks and Lustre Compilation
• 2 mars 2017 - par Loïc Correnson de CEA - Equipe LIST : « De Frama-C à Lustre »
• 2 mars 2017 - par Nicolas Basset de Université Libre de Bruxelles : Uniform Sampling for Timed Automata with Application to Language Inclusion Measurement
• 2 mars 2017 - par Paulin Fournier de LABRI, Bordeaux : Verification of infinite probabilistic systems
• 16 février 2017 - par Mastrolilli Monaldo de IDSIA Lugano : High Degree Sum of Squares Proofs/Hierarchy for 0/1 Problems
• 16 février 2017 - par Naor Seffi de Technion Haifa : Multi-label Classification with Pairwise Relations
• 16 février 2017 - par Abhinav Srivastav de Verimag : Trade-offs in Resource Allocation Problems (Thesis)
• 9 février 2017 - par de : Second Year PhD Students Seminars - week 2/2
• 2 février 2017 - par de : Second Year PhD Students Seminars - week 1/2
• 5 décembre 2016 - par Paul FEAUTRIER de LIP, Ecole Normale Supérieure de Lyon : New Architectures, New Compilation Problems
• 17 novembre 2016 - par Robin David de CEA LIST : Formal Approaches for Automatic Deobfuscation and Reverse-engineering of Protected Codes
• 7 novembre 2016 - par Najah BEN SAID de Verimag, Grenoble Alpes University : Sécurité de Flux d'Information dans les Modèles à Base de Composant: De la Vérification à l'Implementation (Thesis)
• 4 novembre 2016 - par Souha Ben Rayana de Verimag, Grenoble Alpes University : Vérification compositionnelle des systèmes temps-réels à base de compsants et applications. (Thesis)
• 2 novembre 2016 - par Nikos Gorogiannis de University of Middlesex : Biabduction (and Related Problems) in Array Separation Logic
• 28 octobre 2016 - par J. Esparza, A. Bouajjani, and D. Nickovic de TU Munich, IRIF, Austrian IT : Verification: Theory and Practice
• 28 octobre 2016 - par Thomas FERRERE de Verimag : Assertion and Measurements for Mixed-Signal Simulation (Thesis)
• 27 octobre 2016 - par Joseph Sifakis de VERIMAG : Modeling architectures and their properties in BIP
• 13 octobre 2016 - par Ismail Oukid de SAP : Storage Class Memory (aka NVRAM): Challenges and Opportunities
• 12 octobre 2016 - par Louis Dureuil de Vérimag-CEA : Analyse de code et processus d’évaluation des composants sécurisés contre l’injection de faute (Thesis)
• 6 octobre 2016 - par Cristina SERBAN de VERIMAG : A Decision Procedure for Separation Logic in SMT
• 29 septembre 2016 - par Andreas Podelski de University of Freiburg : Thread Modularity on the Next Level
• 29 septembre 2016 - par Joel Ouaknine de Max Planck Institute and Oxford University : Decision Problems for Linear Dynamical Systems
• 29 septembre 2016 - par Parosh Abdulla de Uppsala University : Automatic Verification of Linearization Policies
• 29 septembre 2016 - par Radu Iosif de VERIMAG : Automata and Logics for Program Verification (HDR)
• 5 juillet 2016 - par Rahul Mangaram de University of Pennsylvania : Challenges with Medical Cyber-Physical Systems
• 5 juillet 2016 - par Jyo Deshmukh de TEMA Toyota, Los Angeles : Recent progress on formal methods for CPS
• 30 juin 2016 - par Sergiy Bogomolov de IST Austria : Scalable Static Hybridization Methods for Analysis of Nonlinear Systems
• 22 juin 2016 - par Heiko FALK de Hamburg University of Technology (TUHH) : WCET-Aware Compilation and Optimization for Real-Time Systems
• 16 juin 2016 - par Jan Lanik de VERIMAG : Power reduction in sequential circuits (Thesis)
• 26 mai 2016 - par Frehse Goran de VERIMAG : Scalable Verification of Hybrid Systems (HDR)
• 12 mai 2016 - par Bruno Grenet de LIRMM, Université de Montpellier : Factorisation de polynômes lacunaires
• 28 avril 2016 - par Camille Coti de Université Paris XIII / LIPN : Parallel, distributed behavioral cartography of parametric timed automata
• 24 mars 2016 - par Amaury Pouly de Oxford University, Dept. of Computer Science : Solvability of Matrix-Exponential Equations
• 9 mars 2016 - par Dario Socci de Verimag : Scheduling of Certifiable Mixed-Criticality Systems (Thesis)
• 9 mars 2016 - par Luca Santinelli de ONERA (French Aerospace Lab) : Mixed-Criticalities and Probabilities
• 9 mars 2016 - par Sanjoy Baruah de University of North Carolina at Chapel Hill. : Mixed-criticality Scheduling on Multiprocessors
• 9 mars 2016 - par Alan Burns de University of York : Mixed Criticality - A Personal View
• 2 mars 2016 - par Alexey Bakhirkin de University of Leicester : Towards finding non-terminating behaviours in programs
• 1er mars 2016 - par Arnaud Sangnier de LIAFA PARIS 7 : On the Complexity of Verifying Regular Properties on Flat Counter Systems
• 4 février 2016 - par de Verimag : PhD Seminars
• 29 janvier 2016 - par Mathilde Duclos de Université Grenoble-Alpes : Méthodes pour la vérification des protocoles cryptographiques dans le modèle calculatoire (Thesis)
• 28 janvier 2016 - par de Verimag : PhD Seminars
• 7 janvier 2016 - par de Verimag : Phd Seminars
• 10 décembre 2015 - par Alexios Lekidis de Verimag/DCS : Design flow for the rigorous development of networked embedded systems (Thesis)
• 10 décembre 2015 - par PEKTAŞ Abdurrahman de TUBITAK : Behavior based malware classification using online machine learning (Thesis)
• 16 octobre 2015 - par Enea Zaffanella de Università degli Studi di Parma : A Few Notes on the Implementation of Convex Polyhedra Using the Double Description Framework
• 15 octobre 2015 - par Alexis Fouilhe de Verimag : Revisiting the abstract domain of polyhedra: constraints-only representation and formal proof (Thesis)
• 15 octobre 2015 - par Andy King de University of Kent : The Ying and the Yang of Binary Reversing
• 14 octobre 2015 - par Chantal Keller de Université Paris Sud : F*: Higher-Order Effectful Program Verification
• 18 septembre 2015 - par Ali Kassem de Verimag : Vérification automatique de protocoles d'examen, de monnaie, de réputation, et de routage (Thesis)
• 10 septembre 2015 - par Julien Signoles Nikolai Kosmatov de CEA6LIST : Combinations of Static and Dynamic Analyses in Frama-C: An Overview
• 3 septembre 2015 - par Amaury Pouly de LIX (Polytechnique) : On the complexity of some continuous space reachability problems
• 2 juillet 2015 - par Christos H. Papadimitriou de UC Berkeley : Life under the Lens
• 25 juin 2015 - par Pablo Buiras de Chalmers University of Technology (Sweden) : Mixing Static and Dynamic Typing for Information-Flow Control in Haskell
• 11 juin 2015 - par Chris Myers de University of Utah : LEMA: A Tool for the Formal Verification of Digitally-Intensive Analog/Mixed-Signal Circuits
• 9 juin 2015 - par Ahlem TRIKI de Verimag : Distributed Implementations of Timed Component-based Systems (Thesis)
• 28 mai 2015 - par Andrew Reynolds de EPFL Lausanne : Using CVC4 for Proofs by Induction in SMT
• 8 avril 2015 - par Ayoub Nouri de Verimag : Rigorous System-level Modeling and Performance Evaluation for Embedded System Design (Thesis)
• 3 avril 2015 - par Damien Pous de ENS de Lyon : Algorithms for language equivalence of finite automata
• 19 février 2015 - par Seminaires doctorants 3 de Verimag : Verimag PhD seminars 3
• 12 février 2015 - par Seminaires doctorants 2 de Verimag : Verimag PhD seminars 2
• 5 février 2015 - par Seminaires doctorants 1 de Verimag : Verimag PhD seminars 1
• 29 janvier 2015 - par Jim Kapinski de TEMA Toyota Technical Center in Los Angeles : Applying V&V technologies to automotive engine control: challenges and directions
• 15 janvier 2015 - par Alexandre Marechal de Verimag PhD student : A new Linearization Technique for Multivariate Polynomials Using Convex Polyhedra Based on Handelman-Krivine's Theorem
• 10 décembre 2014 - par Cristina Serban de VERIMAG : An Introduction to Separation Logic
• 21 novembre 2014 - par Chih-Hong Cheng de ABB Germany : G4LTL-ST - Automatic Generation of PLC programs
• 13 novembre 2014 - par Victor Magron de Imperial College : New applications of moment-SOS hierarchies
• 7 novembre 2014 - par Jean-Baptiste Jeannin de Carnegie Mellon University : Differential Temporal Dynamic Logic for Hybrid Systems and Airplane Collision Avoidance
• 15 octobre 2014 - par Andreas Podelski de University of Freiburg : Proof Spaces for Unbounded Parallelism
• 14 octobre 2014 - par Andreas Podelski de University of Freiburg : Static Analysis Modulo Theory
• 13 octobre 2014 - par Julien Henry de Université de Grenoble : Analyse statique de programmes par interprétation abstraite et procédures de décision (Thesis)
• 13 octobre 2014 - par Pranav TENDULKAR de Verimag : Allocation et Ordonnancement sur des processeurs multi-coeur avec des solveurs SMT (Thesis)
• 9 octobre 2014 - par Kim Quyên Lý de LIAMA, VERIMAG : Verification automatique de certificats de terminaison (Thesis)
• 3 octobre 2014 - par Raphaël Jamet de Verimag : Protocoles et Modèles pour la Sécurité des Réseaux Ad Hoc Sans-Fil (Thesis)
• 12 septembre 2014 - par Jean-Marc Vincent de LIG : A Spatiotemporal Data Aggregation Technique for the Macroscopic Analysis of Large-scale Systems
• 28 mai 2014 - par Dejan Nickovic de Austrian Institute of Technology : Require, Test and Trace It
• 28 avril 2014 - par Christian VON ESSEN de Verimag/UJF : Vérification et synthèse quantitative (Thesis)
• 14 avril 2014 - par Kees Goossens de TUE : CompSOC: A Mixed-Criticality Platform, Formalism, and Design Flow
• 3 avril 2014 - par Florian Brandner de ENSTA-ParisTech : Refinement of Worst-Case Execution Time Bounds by Graph Pruning
• 3 avril 2014 - par Jan Reineke de Universität des Saarlandes : PRET DRAM controller: bank privatization for predictability and temporal isolation
• 13 mars 2014 - par Matthieu Moy de Verimag : High-level Models for Embedded Systems (HDR)
• 27 février 2014 - par Eugene Asarin de LIAFA : Toward a Timed Theory of Channel Coding
• 14 février 2014 - par Franck Cassez de NICTA, Sydney, Australie : A compositional approach to inter-procedural analysis
• 7 février 2014 - par Victor Magron de LAAS : Formal Certificates for Nonlinear Inequalities
• 6 février 2014 - par Najah Ben Said de Verimag : Information Flow Security in Component-Based Systems.
• 6 février 2014 - par Ali Kassem de Verimag : Formal Security Analysis for Routing Protocols and E-exams
• 30 janvier 2014 - par Abhinav Srivastav de Verimag : Multi-objective scheduling for multi-core systems
• 23 janvier 2014 - par Alexios Lekidis de Verimag : Model-based design in sensor network systems
• 23 janvier 2014 - par Souha Ben Rayana de Verimag : Compositional Verification of Component- Based Real-time Systems and Applications
• 23 janvier 2014 - par Alexis Fouilhe de Verimag : Verifying numerical static analysis results with a proof assistant
• 16 janvier 2014 - par Ozgun Pinarer de Verimag : Estimation of energy consumption of embedded system network
• 16 janvier 2014 - par Irini-Eleftheria Mens de Verimag : Learning Regular Languages over Large Alphabets
• 16 janvier 2014 - par Jan Lanik de Verimag : Switching reduction in sequential circuits
• 7 janvier 2014 - par Corneliu Popeea de Technische Universitaet Muenchen : Automated verification of multi-threaded programs
• 12 décembre 2013 - par Yvan Rivierre de VERIMAG : Algorithmes auto-stabilisants pour la construction de structures couvrantes réparties (Thesis)
• 9 décembre 2013 - par Giuseppe Lipari de LSV et Scuola Superiore Sant'Anna, Pisa : Hierarchical scheduling and component-based analysis of real-time systems
• 25 novembre 2013 - par Jannik Dreier de VERIMAG : Vérification formelle des protocoles de vote et de vente aux enchères: De l'anonymat à l'équité et la vérifiabilité (Thesis)
• 25 novembre 2013 - par Mahfuza Farooque de École polytechnique : A Bisimulation between DPLL(T) and a Proof-Search Strategy for the Focused Sequent Calculus
• 31 octobre 2013 - par Mirko Fiacchini de GIPSA-lab, Grenoble : Set-theory and invariance for complex systems
• 26 septembre 2013 - par Garnacho Manuel de IRIT : A Mechanized Semantic Framework for Real-Time Systems
• 16 septembre 2013 - par Jean Quilbeuf de Verimag : Implantations distribuées de modèles à base de composants communicants par interactions multiparties avec priorités : application au langage BIP. (Thesis)
• 18 juillet 2013 - par Gaël Thomas de Paris VI / LIP6 : A Study of the Scalability of Stop-the-world Garbage Collectors on Multicores
• 11 juillet 2013 - par Sriram Sankaranarayanan de University of Colorado at Boulder : Invariance and Termination for Probabilistic Programs using Martingales.
• 10 juillet 2013 - par Xiaomu Shi de VERIMAG UJF : Certification d'un simulateur de jeu d'instructions (Thesis)
• 27 juin 2013 - par Klaus Draeger de University of Oxford : Synchronization Invariants
• 19 juin 2013 - par Jessy Clédière de CEA-Grenoble LETI DSIS STCS CESTI : Treize années au Centre d'Evaluation de la Sécurité des Technologies de l'Information du CEA-Grenoble (CESTI-Léti) (HDR)
• 11 juin 2013 - par Christian von Essen de Verimag : Of Markov Decision Processes and Airborne Collisions
• 30 mai 2013 - par Chantal Keller de Laboratoire d'informatique de l'X : A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• 23 mai 2013 - par Adam Halasz de West Virginia University : Challenges and possible strategies in the modeling of signal initiation by membrane bound receptors
• 6 mai 2013 - par Emmanuel Sifakis de Verimag/UJF : Programmation efficace et sécurisé d'applications à mémoire partagée (Thesis)
• 26 avril 2013 - par Zhoulai Fu de IMDEA Madrid : Picking up your targets --- aggressive strong update beyond common sense
• 25 avril 2013 - par Deshmukh Jyotirmoy de Toyota : Mining Temporal Requirements of an Industrial-Scale Control System
• 12 avril 2013 - par Florent Garnier de VERIMAG : Verifying C-Programs memory faults freedom by mean of Abstract Interpretation and a-posteriori model verification
• 9 avril 2013 - par Paraskevas Bourgos de Verimag / UJF : Flot de conception rigoureux pour la programmation de plates-formes manycore (Thesis)
• 22 mars 2013 - par Karem Sakalla de University of Michigan Ann Arbor : Saucy3: Fast Symmetry Discovery in Graphs
• 19 mars 2013 - par Sanjit Seshia de University of California, Berkeley : Integrating Induction and Deduction for Verification and Synthesis
• 18 mars 2013 - par Wang Yi de Uppsala University : Scheduling and Analysis of Cyclic Mode-Switches
• 18 mars 2013 - par Rolf Ernst de TU Braunschweig : Mixed critical system design and analysis
• 18 mars 2013 - par Wang Yi de Uppsala University : Scheduling and Analysis of Cyclic Mode-Switches
• 6 mars 2013 - par Marc Pouzet de UPMC / ENS : Zélus: A Synchronous Language with ODEs
• 21 février 2013 - par Valentin Perrelle de UJF / Verimag : Analyse Statique de Programmes Manipulant des Tableaux (Thesis)
• 31 janvier 2013 - par Ahlem Triki de Verimag : Seminaire doctorant
• 31 janvier 2013 - par Dario Socci de Verimag : Seminaire doctorant
• 24 janvier 2013 - par Raphael Jamet de Verimag : Seminaire doctorant
• 24 janvier 2013 - par Julien Henry de Verimag : Seminaire doctorant
• 24 janvier 2013 - par Ayoub Nouri de Verimag : Seminaire doctorant
• 16 janvier 2013 - par Prabhakar Pavithra de IMDEA, Spain : Approximation based Verification of Hybrid Systems
• 7 décembre 2012 - par Romain Testylier de UJF : Reachability analysis of nonlinear dynamical systems (Thesis)
• 6 décembre 2012 - par Irina Asavoae de University Alexandru Ioan Cuza, Iasi, Romania : Bounded Model Checking of Recursive Programs with Pointers in K Abstract
• 6 décembre 2012 - par Mihail Asavoae de University Alexandru Ioan Cuza, Iasi, Romania : Semantics-Based WCET Analysis
• 9 novembre 2012 - par Damien Massé de Université de Bretagne Occidentale (Brest) : Inférences de propriétés de terminaison par itération de stratégies
• 6 novembre 2012 - par Pascal Lafourcade de Verimag : Sécurité assisté par ordinateur pour les primitives cryptographiques, les protocoles de vote électroniques et les réseaux de capteurs sans fil (HDR)
• 29 octobre 2012 - par Jean-François KEMPF de VERIMAG : Exploration de l'espace de design assistée par ordinateur pour les systèmes multi-coeurs (Thesis)
• 24 octobre 2012 - par Selma Saidi de VERIMAG : Optimizing DMA Data Transfers for Embedded Multi-Cores (Thesis)
• 16 octobre 2012 - par Guillaume Brat de NASA Ames : An overview of formal methods for Aeronautics at NASA
• 2 octobre 2012 - par Artur Pietrek de VERIMAG : TIREX: a textual target-level intermediate representation for virtual execution environment, compiler information exchange and program analysis (Thesis)
• 14 septembre 2012 - par Rance Delong de SRI International : MILS and DMILS project
• 13 septembre 2012 - par Corneliu Popeea de Technical University of Munich : Synthesizing Software Verifiers from Proof Rules
• 12 juillet 2012 - par Roberto Bruttomesso de ATRENTA : Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms
• 5 juillet 2012 - par Pascal Cuoq de CEA : Collaboration d'analyses dans Frama-C
• 26 juin 2012 - par Gerardo Schneider de Chalmers | University of Gothenburg : Towards a Framework for Conflict Analysis of Normative Texts Written in Controlled Natural Language
• 26 juin 2012 - par Eduardo Mazza de Verimag : A Formal Framework for Specifying and Analyzing Liabilities Using Log as Digital Evidence (Thesis)
• 21 juin 2012 - par Jean-Christophe Filliâtre de CNRS / LRI : Combining Interactive and Automated Theorem Proving in Why3
• 7 juin 2012 - par Gilles Muller de LIP6 : Remote Core Locking: Migrating Critical-Section Execution to Improve the Performance of Multithreaded Applications
• 5 juin 2012 - par Tesnim Abdellatif de Verimag : Rigorous Implementation of Real-time Systems (Thesis)
• 1er juin 2012 - par Ian Mitchell de VERIMAG : Scalable approximation of the viability kernel and safe control synthesis for LTI systems using maximal reachability
• 31 mai 2012 - par Pavol Cerny de IST Austria : Quantitative Abstraction Refinement
• 29 mai 2012 - par Rajarshi RAY de Verimag : Reachability Analysis of Hybrid Systems Using Support Functions (Thesis)
• 25 mai 2012 - par Johannes Reich de SPA : A System Perspective on Processes and Their Interactions.
• 11 mai 2012 - par Xavier Urbain de ENSIIE : Démonstration automatique : techniques, outils et certification.
• 9 mai 2012 - par Pierre Ganty de IMDEA (Madrid) : A Perfect Model for Bounded Verification
• 5 avril 2012 - par Laura Kovacs de Technical University of Vienna : Playing in the Grey Area of Proofs
• 22 mars 2012 - par Oded Maler de VERIMAG : Performance Evaluation of Schedulers in a Probabilistic Setting
• 12 mars 2012 - par Nicolas Berthier de Université de Grenoble : Programmation synchrone de pilotes de périphériques pour un contrôle global de ressources dans les systèmes embarqués (Thesis)
• 8 mars 2012 - par Goran Frehse de Verimag : Safety Analysis of Hybrid Systems with SpaceEx
• 5 mars 2012 - par Sriram Rajamani de Microsoft Research : Program Analysis and Machine Learning: A Win-Win Deal
• 1er mars 2012 - par Jerôme Leroux de LABRI : Vector Addition System Reachability Problem
• 23 février 2012 - par Franck Petit de LIP6 : Strength of Stabilization vs. Amount of Resources
• 10 février 2012 - par Laurent George de INRIA Rocquencourt / AOSTE Team INRIA : Robustesse temporelle dans les systèmes embarqués mono et multiprocesseur
• 9 février 2012 - par Jan Olaf Blech de Fortiss : Proof Assistant Based Certification for Modeling Languages and its Application to PLC Development
• 26 janvier 2012 - par Tom Henzinger de IST-Austria : Quantitative Reactive Modeling
• 19 janvier 2012 - par Christian von Essen de Verimag : Synthesizing Efficient Controllers
• 12 janvier 2012 - par Marion DAUBIGNARD de VERIMAG : Formalisation de preuves de sécurité concrète (Thesis)
• 18 novembre 2011 - par Giovanni Funchal de Verimag/STMicroelectronics : Contributions à la Modélisation Transactionnelle des Systèmes-sur-Puce (Thesis)
• 14 novembre 2011 - par Philippe Suter de EPFL : Sets with Cardinality Constraints in Satisfiability Modulo Theories
• 4 octobre 2011 - par Julien Legriel de VERIMAG : Optimisation multi-critère et application aux systèmes multi-processeurs embarqués (Thesis)
• 15 septembre 2011 - par Balaji Raman de DCS, Verimag : On Buffering with Stochastic Guarantees in Resource-Constrained Media Players
• 21 juillet 2011 - par Pierre Ganty de IMDEA : Pattern-based Verification for Multithreaded Programs
• 30 juin 2011 - par Nathalie Bertrand de IRISA : Determinizing timed automata.
• 28 juin 2011 - par Francesco Logozzo de Microsoft Research : Practical program verification for the working programmer with CodeContracts and Abstract Interpretation
• 21 juin 2011 - par VASSILIKI SFYRLA de VERIMAG/UJF : Modélisation des Systèmes Synchrones en BIP (Thesis)
• 26 mai 2011 - par Jannik Dreier de VERIMAG : Privacy Properties for Voting Protocols: The completed picture
• 19 mai 2011 - par Viktor Kuncak de EPFL : Towards Implicit Programming
• 18 mai 2011 - par Jinyun XUE de Institute of Software, Chinese Academy of Science, : PAR Method and PAR Platform for Developing Reliable Software and Its New Development
• 16 mars 2011 - par Fabio Somenzi de University of Colorado in Boulder : Clause Manipulation for Faster Satisfiability
• 3 mars 2011 - par Hubert Garavel de INRIA : CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processe
• 3 février 2011 - par IMENE BEN HAFAIEDH de VERIMAG-UJF : Component-based Systems: from Design to Implementation (Thesis)
• 21 janvier 2011 - par Sophie Quinton de Verimag / UJF : Design, verification and implementation of systems of components (Thesis)
• 20 décembre 2010 - par John Plaice de University of New South Wales : La programmation Cartésienne (Habilitation à Diriger des Recherches) (HDR)
• 18 novembre 2010 - par Antoine GERBAUD de Synchrone/Asynchrone : Le modèle du marcheur pour les réseaux d'interactions
• 5 novembre 2010 - par Moshe Vardi de Rice University : From Philosophical to Industrial Logics
• 28 octobre 2010 - par Mohamad Jaber de VERIMAG : Centralized and Distributed Implementations of Correct-by-construction Component-based Systems by using Source-to-source Transformations in BIP (Thesis)
• 22 septembre 2010 - par Mathias Péron de UJF / VERIMAG : Contributions à l’analyse statique de programmes manipulant des tableaux (Thesis)
• 15 septembre 2010 - par Tayeb BOUHADIBA de Verimag : 42, Une Approche à Composants pour le prototypage Virtuel des Systèmes Embarqués Hétérogènes (Thesis)
• 27 août 2010 - par Manuel Garnacho de VERIMAG - DCS : Automatisation de la certification formelle de systèmes critiques par instrumentation d\'interpréteurs abstraits (Thesis)
• 26 août 2010 - par Sébastien Bourdeauducq de Sharism at Work : Milkymist : un System-on-Chip libre et orienté video temps réel
• 8 juillet 2010 - par Sophie Quinton de Verimag : Achieving distributed control through model checking
• 1er juillet 2010 - par Jocelyne Troccaz de CNRS/TIMC : TBA
• 18 juin 2010 - par Arshia Cont de IRCAM : Antescofo : A performance-synchronous language for computer music
• 17 juin 2010 - par Karel Heurtefeux de Synchrone : Localisation qualitative appliquée au routage et à l'accès au canal dans les réseaux de capteurs
• 27 mai 2010 - par Thanh Hung NGUYEN de Verimag : Vérification Constructive des Systèmes à base de Composants (Thesis)
• 10 mai 2010 - par Christophe JOUBERT de Technical University of Valencia, Spain : Datalog-based Program Analysis with BES and RWL
• 10 mai 2010 - par Arnaud Sangnier de DISI, Università di Genova : Weak Time Petri Nets Strike back!
• 10 mai 2010 - par Nadia El Mrabet de GREYC algo team - Université de Caen : Arithmétique des couplages, performance et résistance aux attaques par canaux cachés
• 10 mai 2010 - par Regis Gascon de Inria Sophia-Antipolis :
• 7 mai 2010 - par Kevin Marquet de Verimag : Vérification automatique de modèles de systèmes sur puce
• 7 mai 2010 - par Alexandre DONZE de verimag : Conception et analyse basée sur les modèles de systèmes hybrides: techniques par simulations, applications et perspectives
• 22 avril 2010 - par Nikolay Kosmatov de CEA - LISI : Le traitement des alias internes dans l'outil de génération de tests PathCrawler
• 7 avril 2010 - par Mohamed Yassin CHKOURI de VERIMAG : Modélisation des systèmes temps-réel embarqués en utilisant AADL pour la génération automatique d’applications formellement vérifiées (Thesis)
• 1er avril 2010 - par Claire Maiza de Compiler Design Lab, Saarland University : Static analysis of interferences in the cache memory in preemptive real-time systems
• 19 mars 2010 - par Nicolas Blanc de ETH Zurich : Static Analysis for SystemC with Scoot: From Verification to Simulation
• 9 mars 2010 - par Thomas GAWLITZA de verimag : Combining Strategy Iteration with Semidefinite Programming for Abstract Interpretation
• 5 mars 2010 - par Marc Poulhiès de VERIMAG - DCS : Conception et Implantation de Système Fondé sur les Composants. Vers une Unification des Paradigmes Génie Logiciel et Système. (Thesis)
• 4 mars 2010 - par Ondrej Sery de Charles University Prague : Code analysis with Blast
• 16 février 2010 - par Bahareh Badban de University of Konstanz : Automated Invariant Generation for the Verification of Real-Time Systems
• 4 février 2010 - par Marius Bozga de Verimag : Component-Based Construction of Real-Time Systems (HDR)
• 29 janvier 2010 - par Dang Thao de VERIMAG : Methods and tools for Computer Aided Design of Embedded Systems (HDR)
• 14 janvier 2010 - par Arnaud Sangnier de Universite de Turin : Reversal-bounded counter machines revisited
• 19 novembre 2009 - par Matthias Althoff de Technische Universität München : Reachability Analysis of Nonlinear and Hybrid Systems with Zonotopes
• 19 novembre 2009 - par Bruce Krogh de Dept. of Electrical and Computer Engineering, Carn : Research Directions in Cyber-Physical Systems
• 12 novembre 2009 - par Florent Garnier de Vermimagg- Team DCS : A classification of randomized fair strategies for studying termination of term rewriting
• 9 novembre 2009 - par Yliès Falcone de Vérimag : Etude et mise en oeuvre de méthodes de validation à l'exécution (Thesis)
• 29 octobre 2009 - par Stephane Demri de ENS CACHAN : Les problèmes de couverture et finitude pour les systèmes d'addition de vecteurs arborescents.
• 28 octobre 2009 - par Colas Le Guernic de VERIMAG : Calcul d'Atteignabilité des Systèmes Hybrides à Partie Continue Linéaire (Thesis)
• 21 octobre 2009 - par Aldric Degorre de Vérimag : Langages formels: quelques aspects quantitatifs (Thesis)
• 24 septembre 2009 - par Bageshri KARKARE de Verimag : Efficiency, Precision, Simplicity, and Generality in Interprocedural Data Flow Analysis.
• 15 septembre 2009 - par Dino Distefano de Queen Mary University, London : Compositional Shape Analysis by means of Bi-Abduction
• 25 juin 2009 - par Zvonimir Rakamaric de University of British Columbia : Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers
• 25 juin 2009 - par Scott Cotton de Verimag : Sur Quelques Problèmes de la Satisfiabilité (Thesis)
• 19 juin 2009 - par David Monniaux de CNRS / VERIMAG : Analyse statique : de la théorie à la pratique (HDR)
• 14 mai 2009 - par Florian Kammueller de Technische Universitat Berlin : ASPfun: un calcul pour des objets distribués
• 7 mai 2009 - par Villard Jules de LSV, Cachan : Proving Copyless Message Passing
• 16 avril 2009 - par Christophe Guillon de STMicroelectronics : Les représentations SSA et Psi-SSA
• 9 avril 2009 - par Alexandre Donzé de VERIMAG : Calcul numérique d'ensembles atteignables pour les systèmes hybrides et applications
• 2 avril 2009 - par Domagoj Babic de Fujitsu Labs America : Scalable and Precise Extended Static Checking
• 5 mars 2009 - par Thomas Gawlitza de Technische Universität München : Precise Relational Invariants Through Strategy Iteration

Archives