BEGIN:VCALENDAR VERSION:2.0 PRODID:-//129.88.40.24//NONSGML kigkonsult.se iCalcreator 2.20.4// CALSCALE:GREGORIAN METHOD:PUBLISH X-WR-CALNAME:Evènements Verimag X-WR-CALDESC:Liste des évènements (séminaires\, thèses\, ...) au laboratoir e Verimag. X-WR-TIMEZONE:Europe/Paris BEGIN:VEVENT UID:20260720T014631UTC-6787rkKcrR@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20260702T140000 DTEND:20260702T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Léo Colisson Palais - Towards intuitive and formal security proofs using quantum-inspired diagrammatic reasoning END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6788pjSfRw@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20260521T140000 DTEND:20260521T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Clara Bourgeais - Modification du back-end d'un compilateur pour la sécurité : étude de cas sur une contre-mesure contre les attaqs par canau x auxiliaires (Compiler Back-end Modification for Security : a SCA Counter measure Case Study) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6789ssXTEO@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20260430T140000 DTEND:20260430T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Marek BUCKI - Conception de logiciels critiques -- retour d’expérie nce du domaine médical\, et questionnement sur la pratique et l'enseigneme nt de méthodes de design des logiciels END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6789Veso6l@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20260402T140000 DTEND:20260402T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Mohamed Graiet - Approche formelle Générique de Transfert Learning (GTL) dans le continuum CEI END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6790MNUADB@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20260319T140000 DTEND:20260319T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Youssouf Oualhadj - Rational Synthesis in Resource-Constrained Mult i-Agent Systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-67918VRaGz@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20260122T140000 DTEND:20260122T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Joseph Sifakis - Bringing AI to Autonomous Systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6791FItBNx@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20260119T140000 DTEND:20260119T143000 DURATION:PT0H30M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Alban Reynaud - Formal Verification of Borrow-Checking by Local Com mutation Diagrams END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6911fSfWmN@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20251218T140000 DTEND:20251218T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Jérémie Decouchant - Defending TEE-aided Blockchain Consensus again st Rollback Attacks END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6913lXjpMJ@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20251211T140000 DTEND:20251211T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Thaïs Baudon - Compiling types and other high-level language featur es for performance or security END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6914ZxxBAd@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20251204T140000 DTEND:20251204T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Jannik LAVAL - Jumeaux Numériques : Les sciences du logiciel au cœu r de la transformation industrielle (Digital Twins: software engineering a t the heart of industrial transformation) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-69148Uz2UK@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20251201T140000 DTEND:20251201T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Sylvain BOULME - Introduction à la programmation orientée objet en Crystal END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-69153xiiDp@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20251125T140000 DTEND:20251125T150000 DURATION:PT1H0M0S LOCATION:Room 106 (1st floor\, badged access) SUMMARY:Véronique Cortier - Electronic voting: design\, attack\, and formal verification END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6916AVXBIL@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20251121T140000 DTEND:20251121T170000 DURATION:PT3H0M0S LOCATION:Amphithéâtre - Maison du doctorat Jean Kuntzmann SUMMARY:Oussama Oulkaid - Formal models of integrated circuits for transist or level electrical verification END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6916M8FWUG@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20251113T150000 DTEND:20251113T170000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Yann Herklotz - Towards scalable verification and efficient hardwar e generation using verified high-level synthesis tools END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-69176nmJMO@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20251016T143000 DTEND:20251016T163000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Nicolas Chappe - Representing and reasoning about nondeterministic programs END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6918TVAbIE@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20251009T140000 DTEND:20251009T150000 DURATION:PT1H0M0S LOCATION:BBB SUMMARY:Tiago Cogumbreiro - Verifying GPU programs with Memory Access Proto cols END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6918c75JsG@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20251003T100000 DTEND:20251003T120000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Eduardo Camponogara - Formal Analysis of Optimization-based Control lers Approximated by ReLU Neural Nets END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6919sB2z98@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20250626T140000 DTEND:20250626T150000 DURATION:PT1H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Nikolaus Huber - Mimosa: A Language Design for Modern Embedded Syst ems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6920pXcNZK@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20250613T100000 DTEND:20250613T110000 DURATION:PT1H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Selma Saidi - Connected Minds: Leveraging Collective Reasoning for Autonomous Systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6920l6c5OI@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20250612T140000 DTEND:20250612T150000 DURATION:PT1H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Maher Mallem - Parameterized complexity of scheduling problems with precedence delays END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-69218MG2Ua@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20250605T140000 DTEND:20250605T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Sébastien Michelland - Secure compilation—with the compiler\, not a gainst: first experiments on 'Tracing LLVM' END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6921tIRgoi@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20250417T140000 DTEND:20250417T150000 DURATION:PT1H0M0S LOCATION:Zoom UGA 959 9591 1882 -- Passcode: 063113 SUMMARY:Riadh ROBBANA - Le Vote Électronique Sécurisé à l’Ère de la Blockch ain : Contexte\, Défis et Solutions Innovantes END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6922K2rHzF@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20250411T150000 DTEND:20250411T190000 DURATION:PT4H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Hadi Dayekh - L'apprentissage passif et actif des systèmes dynamiqu es non linéaires commutés (Passive and Active Learning of Switched Nonline ar Dynamical Systems) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6923RNKGuu@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20250327T140000 DTEND:20250327T160000 DURATION:PT2H0M0S LOCATION:Zoom (Meeting ID: 986 9236 8072\; Passcode: 923483) SUMMARY:Youssouf Oualhadj - Robust timed synthesis END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6923rAE77x@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20250313T140000 DTEND:20250313T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Thomas Carle - MINOTAuR: a timing-predictable RiscV (CVA6) core END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6924LF234F@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20250306T140000 DTEND:20250306T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Yannick Chevalier - Logique et Cybersécurité END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6924oxbOuD@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20250123T140000 DTEND:20250123T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Niklas Kochdumper - Reachability Analysis and its Application to Ve rification and Control of Cyber-Physical Systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-69252iKjPv@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20241212T140000 DTEND:20241212T160000 DURATION:PT2H0M0S LOCATION:GIPSA-Lab \, Salle JM Chassery\, 11 rue des Maths SUMMARY:Bob AUBOUIN-PAIRAULT - Data-based anesthesia process modelling for online monitoring and prediction END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-69266f86Tl@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20241212T150000 DTEND:20241212T190000 DURATION:PT4H0M0S LOCATION:Amphi C002 - Bâtiment Ampère de l'Ensimag SUMMARY:Lucas Bueri - Logics for Reasoning about the Correctness of Reconfi gurable Distributed Systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6926mtzJbS@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20241202T140000 DTEND:20241202T160000 DURATION:PT2H0M0S LOCATION:Amphitéatre MJK SUMMARY:Thomas Vigouroux - Analyses quantitatives pour les attaquants adapt atifs (Quantitative analysis for adaptive attackers) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6927ropa4X@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20241128T140000 DTEND:20241128T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Grégoire BUSSONE - Réduire les copies et l'utilisation mémoire dans les langages synchrones (Reducing copies and memory consumption in synchr onous languages) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-69282WmfuU@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20241120T140000 DTEND:20241120T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Chao Huang - Safe Reinforcement Learning with Verification in the L oss END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6928MPht7i@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20241114T140000 DTEND:20241114T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Lisa Maile - Real-Time Communication with Dynamic Network Traffic u sing Time-Sensitive Networking END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6929na9Gf8@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20241107T140000 DTEND:20241107T150000 DURATION:PT1H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Aurèle Barrière - Formal Verification Beyond Traditional Compilatio n END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6930jdihsd@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20240627T140000 DTEND:20240627T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Nicolas Chappe - Executable semantics based on Choice Trees for a c oncurrent subset of LLVM IR END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-69309KeWf5@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20240619T093000 DTEND:20240619T113000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Jean-François MONIN - Recent advances on the Braga method END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6931pew2m9@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20240618T093000 DTEND:20240618T113000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Matthieu Sozeau - Verified Extraction from Coq to OCaml END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6932TDGZZ0@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20240617T160000 DTEND:20240617T180000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Basile GROS - Small Inversions in Coq END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-69329m2rbk@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20240617T140000 DTEND:20240617T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Sylvain BOULME - Toward a FFI (Foreign Function Interface) for embe dding untrusted imperative OCaml into Coq-verified computations. END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6933tpPVk6@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20240530T140000 DTEND:20240530T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Mohamed Maghenem - A Hybrid-Systems Framework for Distributed Gradi ent-Based Estimation END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6934PugW79@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20240516T140000 DTEND:20240516T150000 DURATION:PT1H0M0S LOCATION:BBB SUMMARY:Gaiyun Liu - Modeling\, analysis\, and supervisory control of netwo rked discrete event systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6934eviT2Z@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20240502T130000 DTEND:20240502T150000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Matthieu Moy - How to Build a Broken System? END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6935B6trFa@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20240418T140000 DTEND:20240418T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Akram Idani - Formal Model-Driven Engineering END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6936XNc7sG@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20240415T140000 DTEND:20240415T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Subhajit Roy - Satisfiability modulo fuzzing: a synergistic combina tion of SMT solving and fuzzing END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6936AcWfdM@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20240411T143000 DTEND:20240411T163000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Andrei Paskevich - Coma: an intermediate verification language with explicit abstraction barriers END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6937vmvn3D@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20240404T133000 DTEND:20240404T153000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Sébastien Michelland - Abstract Interpreters: a Monadic Approach to Modular Verification END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6938SkhN5D@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20240314T131500 DTEND:20240314T151500 DURATION:PT2H0M0S LOCATION:Room 206 (3rd floor\, badged access) SUMMARY:Adel NOUREDDINE - Observing energy consumption: from hardware to so ftware source code END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6938msUOEA@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20240313T103000 DTEND:20240313T123000 DURATION:PT2H0M0S LOCATION:Room 306 (3rd floor\, badged access) SUMMARY:Inigo Incer - Towards Provably Safe and Secure Systems with Contrac t-Based Design END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6939WZxM16@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20240307T143000 DTEND:20240307T163000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Sylvain Boulmé - Développement logiciel formellement vérifié: pourq uoi et comment ? END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6940DVJvpj@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20240222T140000 DTEND:20240222T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Paolo Ballarini - Hybrid-Automata Specification Language: from expr essive stochastic model checking to parametric stochastic model checking END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6940NWoiB8@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20240212T100000 DTEND:20240212T130000 DURATION:PT3H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Aina Rasoldier - Comment évaluer le potentiel d'une solution numéri que face à l'urgence écologique ? Application aux plateformes de covoitura ge régulier à l'échelle locale END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6941ZDAPbM@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20240208T140000 DTEND:20240208T160000 DURATION:PT2H0M0S LOCATION:Ensimag\, Amphi E SUMMARY:Sophie Morel - Formalisation d'un objet geometrique dans l'assistan t de preuve Lean: le cas des grassmanniennes. END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-69415UrZv5@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20231214T140000 DTEND:20231214T150000 DURATION:PT1H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Alessandro De Palma - From Neural Network Verification to Efficient Robust Training END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6942nA51Em@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20231212T093000 DTEND:20231212T113000 DURATION:PT2H0M0S LOCATION:Seminar Room 2\, ground floor (Building IMAG) SUMMARY:Leo Gourdin - Validation Formelle de Transformations Intra-Procédur ales par Simulation Symbolique Défensive (Formal Validation of Intra-Proce dural Transformations by Defensive Symbolic Simulation) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6943JBR36u@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20231130T140000 DTEND:20231130T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Yutaka Nagashima - AI-Enhanced Theorem Proving: Tactical Approaches for Induction Problems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-69436GUKS3@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20231117T143000 DTEND:20231117T163000 DURATION:PT2H0M0S LOCATION:Maison du doctorat Jean Kuntzmann SUMMARY:Thomas Mari - Explications causales pour les systèmes temps réel ré actifs (Causal explanations for reactive real-time systems) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6944RlxJsc@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20231109T140000 DTEND:20231109T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Gidon Ernst - Automating software verification with respect to stro ng specifications END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6944NGr7zE@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20231019T140000 DTEND:20231019T160000 DURATION:PT2H0M0S LOCATION:zoom SUMMARY:Michael Foster - Active Inference of Extended Finite State Machines Without Reset END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6945PlukUn@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20231012T140000 DTEND:20231012T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Nicola Gigante - Temporal Logics Modulo Theories for Infinite-State Verification END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6946U5Gbz2@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20230712T140000 DTEND:20230712T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Dejan Nickovic - Attribute Repair for Threat Prevention END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6946UEF8fV@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20230707T100000 DTEND:20230707T120000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Akshay Mambakam - Parametric timed formalisms for specification and monitoring (PhD defense) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-69477nD0MP@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20230706T140000 DTEND:20230706T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Nicola Paoletti - Causal Temporal Reasoning for Markov Decision Pro cesses END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-69485obIVh@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20230630T140000 DTEND:20230630T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Sayan Mitra - Assuring Safety of Learning-Enabled Systems with Perc eption Contracts. END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6948u7eI4L@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:HDR DTSTART:20230609T150000 DTEND:20230609T170000 DURATION:PT2H0M0S LOCATION:Auditorium\, ground floor (Building IMAG) SUMMARY:claire maiza - Analyses matérielles et logicielles pour obtenir une analyse temporelle précise et efficace (Hardware and software analyses fo r precise and efficient timing analysis) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-69492OUHZx@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20230609T100000 DTEND:20230609T110000 DURATION:PT1H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Jean-Luc Scharbarg - Trends in real-time embedded networks: towards TSN END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6949LUNxUl@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20230608T140000 DTEND:20230608T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Basile Pesin - Verifying a compiler for a synchronous dataflow lang uage with state machines in Coq END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-69502ku81M@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20230525T140000 DTEND:20230525T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Henri-Pierre Charles - Spécialisation de code binaire au run-time : pour gagner du temps et de l'énergie\, il faut rouler à l'HybroGen END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6951KZUIXf@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20230504T140000 DTEND:20230504T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Joseph Sifakis - Artificial Intelligence and autonomous systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-6951McK2t7@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20230428T110000 DTEND:20230428T120000 DURATION:PT1H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Thomas Jensen - An information flow logic based on partial equivale nce relations END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7106KkmvGa@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20230428T140000 DTEND:20230428T170000 DURATION:PT3H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Etienne Boespflug - Outils pour l’analyse de code et de contre-mesu res pour l'injection de fautes multiples END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7108wLKTmJ@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20230309T140000 DTEND:20230309T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Clementine Gritti - Internet of Things: From modern cryptography to post-quantum cryptography END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7108xVbRT3@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20230306T100000 DTEND:20230306T110000 DURATION:PT1H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Frederic Fort - Programing adaptive real-time systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7109VgR9UP@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20230302T140000 DTEND:20230302T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Arthur Perais - Exploring Instruction Fusion Opportunities in Gener al Purpose Processors END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7110E8g0vG@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20230223T110000 DTEND:20230223T130000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Léo Robert - How fast do you heal? A taxonomy for post-compromise s ecurity in secure-channel establishment. END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7110evZxsZ@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20230223T153000 DTEND:20230223T173000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Imen Sayar - Collaborative development of safe and secure cyber-phy sical systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7111dvTDkk@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20230220T140000 DTEND:20230220T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:anais durand - Exploration of 3D environments by swarms of luminous autonomous robots. END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7112V8hhKK@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20230206T140000 DTEND:20230206T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Bruno FERRES - Using Model Checking for Electrical Rule Checking o f Integrated Circuits at Transistor Level END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7138XTxuBV@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20230202T140000 DTEND:20230202T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Charlie Jacomme - A comprehensive\, formal and automated analysis o f the EDHOC protocol. END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7139p7l3BN@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20230126T140000 DTEND:20230126T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Son Ho - Aeneas: Rust Verification by Functional Translation END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7139CWIucB@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20221216T100000 DTEND:20221216T123000 DURATION:PT2H30M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Vincent Morice - Modèle haut niveau de microcontrôleurs basé sur l es dépendances pour le développement de logiciel embarqué END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7140TGrhAJ@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20221213T140000 DTEND:20221213T150000 DURATION:PT1H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Ezio Bertocci - Automatic Invariant Generations for Probabilistic L oops (Automatic Invariant Generations for Probabilistic Loops) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7141idKAPC@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20221208T140000 DTEND:20221208T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Kohei SUENAGA - Oblivious Online Monitoring for Safety LTL Specific ation via Fully Homomorphic Encryption END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7141kOEC03@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20221124T140000 DTEND:20221124T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Xavier Denis - Deductive Verification of Higher-Order Rust Programs END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7142CEXIVC@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20221124T100000 DTEND:20221124T113000 DURATION:PT1H30M0S LOCATION:Room 285 (badged access\, limited occupancy) SUMMARY:Jean-François Monin - Programmation récursive en Coq et intensional ité : oh le beau cas ! (Recursive Programming in Coq and Intensionality : oh happy case !) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7143rdVJvA@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20221117T140000 DTEND:20221117T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Arnaud Sangnier - Parameterized verification of Networks with selec tive broadcast END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7143m1whNU@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20221110T140000 DTEND:20221110T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Stephan Plassart - Equivalent Versions of Total Flow Analysis END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7144R9cfFF@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20221027T140000 DTEND:20221027T150000 DURATION:PT1H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Hugo Gimbert - Les algorithmes de ParcourSup END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7144rvrzFp@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20220929T140000 DTEND:20220929T150000 DURATION:PT1H0M0S LOCATION:Seminar Room\, ground floor (Building IMAG) SUMMARY:Merigoux Denis - Rules\, Computation and Politics: Scrutinizing Unn oticed Programming Choices in French Housing Benefits END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7145JvtURx@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20220909T140000 DTEND:20220909T150000 DURATION:PT1H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Lucas Bueri - On an Invariance Problem for Parameterized Concurrent Systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7146Obmcho@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20220712T140000 DTEND:20220712T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Dejan Nickovic - Information-flow Interfaces END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7146UdXHdW@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20220707T140000 DTEND:20220707T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Franz Meyer - Towards Efficient Active Learning of PDFA END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7147W6HKdG@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20220621T140000 DTEND:20220621T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Joel Goossens - Real-Time Computing\, Multiprocessor scheduling pro blems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7147DgFOGv@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20220616T140000 DTEND:20220616T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Joel Goossens - Periodicity of real-time priority driven schedulers with preemption delay on uniprocessor END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7148xXI6FB@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20220614T140000 DTEND:20220614T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Joel Goossens - Real-Time Computing\, foundation END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7149iucLdp@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20220603T090000 DTEND:20220603T150000 DURATION:PT6H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:CAPITAL Workshop - Workshop CAPITAL 2022 : sCalable And PrecIse Ti ming AnaLysis for multicore platforms (Workshop CAPITAL 2022 : sCalable An d PrecIse Timing AnaLysis for multicore platforms) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-71490krP46@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20220531T093000 DTEND:20220531T113000 DURATION:PT2H0M0S LOCATION:Seminar Room\, ground floor (Building IMAG) SUMMARY:Matheus Schuh - Safe Implementation of Hard Real-Time Applications on Many-Core Platforms END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7150vSist1@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20220505T100000 DTEND:20220505T120000 DURATION:PT2H0M0S LOCATION:https://bans.imag.fr/b/rad-ofn-9t8-rqc SUMMARY:Nathalie Bertrand - Reconfigurable Parameterized Broadcast Networks : Minimal Size and Execution Length for Coverability END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7151w7buaD@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20220407T100000 DTEND:20220407T120000 DURATION:PT2H0M0S LOCATION:https://bans.imag.fr/b/rad-ofn-9t8-rqc SUMMARY:Benedikt Bollig - Identifiers in Registers - Describing Network Alg orithms with Logic END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7151vawMVJ@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20220324T140000 DTEND:20220324T150000 DURATION:PT1H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:David Monniaux - The trusted computing base of the CompCert verifie d compiler END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7218Pw37V7@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20220310T140000 DTEND:20220310T150000 DURATION:PT1H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Paolo Torrini - A CompCert Backend with Symbolic Encryption END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7219WnJwLj@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20220303T143000 DTEND:20220303T163000 DURATION:PT2H0M0S LOCATION:Zoom link SUMMARY:Xiaowei Huang - Machine Learning Safety END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7220PoAprm@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20220113T140000 DTEND:20220113T160000 DURATION:PT2H0M0S LOCATION:Room 206 SUMMARY:Benjamin BLANC - Formal Methods in Practice: Model Checking in the Railway Industry END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7220unRguf@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20211213T140000 DTEND:20211213T160000 DURATION:PT2H0M0S LOCATION:https://veri-bbb.imag.fr/b/rad-ofn-9t8-rqc SUMMARY:Joseph Sifakis - Specification and Validation of Autonomous Driving Systems: A Multilevel Semantic Framework END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7221VvEvFw@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20211207T140000 DTEND:20211207T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Alessio Mansutti - Efficient complementation of semilinear sets and the VC dimension of Presburger arithmetic END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-72228W8N4b@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20211203T100000 DTEND:20211203T120000 DURATION:PT2H0M0S LOCATION:https://veri-bbb.imag.fr/b/rad-ofn-9t8-rqc SUMMARY:Miriam Garci­a - Design\, Verification and Synthesis of Hybrid Sys tems. END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7222whz7Ob@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20211202T140000 DTEND:20211202T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Leo Exibard - Reactive Synthesis over Infinite Data Domains with Ma chines with Registers END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7223eIEi1N@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20211129T140000 DTEND:20211129T160000 DURATION:PT2H0M0S LOCATION:Vidéo SUMMARY:Nicolas Basset - Uniform Sampling for Networks of Automata END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7224KtWcrl@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20211123T140000 DTEND:20211123T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:PIERRE-LEO BEGAY - Conception\, développement et certification dans Coq/MathComp d'optimisations Datalog pour la vérification réseau (Design\ , Development and certification in Coq/MathComp of Datalog optimizations f or network verification) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7224bCv9bS@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20211004T140000 DTEND:20211004T160000 DURATION:PT2H0M0S LOCATION: https://veri-bbb.imag.fr/b/rad-ofn-9t8-rqc SUMMARY:Hadi DAYEKH - Learning Automata over Large Alphabets as an Alternat ive to Recurrent Neural Networks END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7225S0J1n7@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:HDR DTSTART:20210927T150000 DTEND:20210927T170000 DURATION:PT2H0M0S LOCATION:Video SUMMARY:Sylvain Boulmé - Formally Verified Defensive Programming (efficient Coq-verified computations from untrusted ML oracles) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7226gcRvPD@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20210920T140000 DTEND:20210920T160000 DURATION:PT2H0M0S LOCATION:https://veri-bbb.imag.fr/b/rad-ofn-9t8-rqc SUMMARY:Lucas Bueri - Décidabilité de la rationalité des VAS END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-72267TWf7a@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20210830T140000 DTEND:20210830T150000 DURATION:PT1H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Yannick Zakowski - Sémantique de Vellvm (Vellvm semantics) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7227UeMGux@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20210713T150000 DTEND:20210713T170000 DURATION:PT2H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Cyril Six - Compilation optimisante et formellement prouvée pour un processeur VLIW (Optimized and formally-verified compilation for a VLI W processor) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7228ERcG4U@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20210617T140000 DTEND:20210617T160000 DURATION:PT2H0M0S LOCATION:bbb\, code d'accès 394787 SUMMARY:Pierre Courtieu - [FormalProofs] Gestion d'un environment de preuve 'moche' ([FormalProofs] Dealing with ugly proof environment.) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7228JddSvE@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20210610T150000 DTEND:20210610T170000 DURATION:PT2H0M0S LOCATION:Room 206 et BBB (code d'accès 506793) SUMMARY:Jean-François Monin - [FormalProofs] Petites inversion et récursion débridée en Coq\, la méthode de Braga ([FormalProofs] Small inversions an d unleashed recursion in Coq\, the Braga method) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7229g6rFip@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20210423T090000 DTEND:20210423T110000 DURATION:PT2H0M0S LOCATION:Zoom SUMMARY:Schoitsch Erwin - Ethical aspects and recommendations for trustwor thy highly automated/autonomous systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-72300TbNm7@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20210401T140000 DTEND:20210401T160000 DURATION:PT2H0M0S LOCATION:BBB room access code 349356 SUMMARY:Lionel Rieg - [FormalProofs] A formally-verified compiler from Este rel to circuits END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7231H8ixgG@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20210311T140000 DTEND:20210311T150000 DURATION:PT1H0M0S LOCATION:https://barbarate.imag.fr/b/dav-ygp-g07-gi0 SUMMARY:David Monniaux - [SharedResources] CompCert for Risc-V on FPGA END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7231cK1Pb3@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20210226T100000 DTEND:20210226T110000 DURATION:PT1H0M0S LOCATION:Visioconference SUMMARY:Emma AHRENS - Local Reasoning for Reconfigurable Distributed System s END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-72320usLfk@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20210225T140000 DTEND:20210225T160000 DURATION:PT2H0M0S LOCATION:BBB : Room access code 756979 SUMMARY:Cyril SIX - Certified Superblock Scheduling for the CompCert Compil er END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7233MOuGHb@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20210211T140000 DTEND:20210211T160000 DURATION:PT2H0M0S LOCATION:https://barbarate.imag.fr/b/jac-ehy-mnq-4cf SUMMARY:Franck POMMEREAU - Formal Modelling and Symbolic Analysis of Ecosys tems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7233jFkRSA@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20210128T140000 DTEND:20210128T160000 DURATION:PT2H0M0S LOCATION:https://veri-bbb.imag.fr/b/rad-ofn-9t8-rqc SUMMARY:Etienne André - Symbolic Monitoring against Specifications Parametr ic in Time and Data END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7234e1VbMf@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20210121T140000 DTEND:20210121T160000 DURATION:PT2H0M0S LOCATION:https://univ-grenoble-alpes-fr.zoom.us/j/932168111 SUMMARY:Etienne Andre - Symbolic Monitoring against Specifications Parametr ic in Time and Data END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7235bb41VI@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20210114T140000 DTEND:20210114T160000 DURATION:PT2H0M0S LOCATION:https://veri-bbb.imag.fr/b/mic-1x2-b8m-ama SUMMARY:Olivier RIDOUX - Limite de Landauer et calcul réversible : une intr oduction (Landauer limit and reversible calculus: an introduction) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-72352nTwpo@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20201218T100000 DTEND:20201218T120000 DURATION:PT2H0M0S LOCATION:By zoom (details below) SUMMARY:Guo Xiaojie - Certified Tools for Schedulability Analyses END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7236vMb72k@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:HDR DTSTART:20201217T130000 DTEND:20201217T150000 DURATION:PT2H0M0S LOCATION:Amphithéâtre de la Maison Jean Kuntzmann SUMMARY:Stéphane Devismes - Versatility and Efficiency in Self-Stabilizing Distributed Systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-72379lW64I@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20201211T103000 DTEND:20201211T123000 DURATION:PT2H0M0S LOCATION:virtual seminar SUMMARY:Marius Bozga - Compositional Generation of Invariants for Timed Sys tems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7237bZZNBW@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20201203T151500 DTEND:20201203T164500 DURATION:PT1H30M0S LOCATION:Séminaire virtuel via BigBlueButton SUMMARY:Jacques Combaz - Introduction aux effets rebond [lien visio: https: //veri-bbb.imag.fr/b/jac-lxa-inn-hnq] END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7238PvKdG1@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20201120T103000 DTEND:20201120T123000 DURATION:PT2H0M0S LOCATION:virtual seminar on zoom (see below) SUMMARY:Radu Iosif - Structural Invariants for the Verification of Systems with (Recursively Defined) Parameterized Architectures END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7239vtFMDW@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20201119T160000 DTEND:20201119T171500 DURATION:PT1H15M0S LOCATION:Séminaire virtuel via BigBlueButton SUMMARY:Aina Rasoldier - Les méthodologies d'évaluation des impacts environ nementaux des technologies de l'information et de la communication (TIC) à l'échelle mondiale END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-72397T3Bus@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20201117T140000 DTEND:20201117T160000 DURATION:PT2H0M0S LOCATION:zoom SUMMARY:Schuh Matheus - A study of predictable execution models implementat ion for industrial data-flow applicationson a multi-core platform with sha red banked memory END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7240Iukf7L@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20201106T103000 DTEND:20201106T120000 DURATION:PT1H30M0S LOCATION:Virtual seminar (the link will be sent later) SUMMARY:Akshay Mambakam - Learning Specifications for Labelled Patterns END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7241mTM8X8@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20201022T141500 DTEND:20201022T151500 DURATION:PT1H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Cyril Six - Certified and Efficient Instruction Scheduling. Applica tion to Interlocked VLIW Processors. END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7241Gh7can@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20200630T140000 DTEND:20200630T150000 DURATION:PT1H0M0S LOCATION:Online : https://veri-bbb.imag.fr/b/pie-zc2-ji9 SUMMARY:Sébastien Michelland - Une Procédure de Décision pour les Relations d'Équivalence (A Decision Procedure for Equivalence Relations) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7242IR30nV@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20200312T140000 DTEND:20200312T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Mathias RAMPARISON - Updatable Parametric Timed Automata: Decidabi lity\, Algorithms\, and Application to Security (Updatable Parametric Time d Automata: Decidability\, Algorithms\, and Application to Security) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7243hSOUHb@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20200309T153000 DTEND:20200309T173000 DURATION:PT2H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Rémy Boutonnet - Modular Analysis of Numerical Properties by Abstra ct Interpretation END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7243km4hGC@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20200221T103000 DTEND:20200221T113000 DURATION:PT1H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Michael Marcozzi - Compiler Fuzzing: How Much Does It Matter? END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-72446JrcMB@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20200213T103000 DTEND:20200213T123000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Jonathan Salwan - L'exécution symbolique pour l'aide à la rétro-ing énierie dans un cadre industriel END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7245wFivf5@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20200212T140000 DTEND:20200212T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Sébastien Bardin - From Safety to Security: The Case of Binary-lev el Code Analysis END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-72457uVeJf@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20200206T140000 DTEND:20200206T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Jules Chouquet - Lower bounds for probabilistic k-set agreement thr ough combinatorial topology END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7246v8ZEZE@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20200203T110000 DTEND:20200203T120000 DURATION:PT1H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Matthieu Jan and Asavoae Mihail - Towards Automatic Extraction of T iming models from HDL designs (Mihail Asavoae) - Tracking timing anomalies (Matthieu Jan) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7247pMvejK@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20200127T103000 DTEND:20200127T113000 DURATION:PT1H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Margus Veanes - Symbolic Regexes & Matching END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7247vWAgS7@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20200127T140000 DTEND:20200127T180000 DURATION:PT4H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Xiao XU - Thesis Defence - Xiao XU - Generalisation of Alternating Automata over Infinite Alphabets END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7248p5jCtU@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20191219T100000 DTEND:20191219T130000 DURATION:PT3H0M0S LOCATION:Seminar Room\, ground floor (Building IMAG) SUMMARY:Hang Yu - Towards an Efficient Parallel Parametric Linear Programmi ng Solver END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7249bOol1W@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20191219T140000 DTEND:20191219T150000 DURATION:PT1H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Yannick Zakowski - From representing recursive and impure programs in Coq to a modular formal semantics of LLVM IR END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-72496kaDtx@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20191125T140000 DTEND:20191125T160000 DURATION:PT2H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Moshe Vardi - Technology is Driving the Future\, But Who Is Steerin g? END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-72500dU9UK@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20191121T140000 DTEND:20191121T153000 DURATION:PT1H30M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Sophie Tourret - Stronger Higher-order Automation END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7251VCAlVO@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20191010T150000 DTEND:20191010T160000 DURATION:PT1H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Jan Reineke - Spectector: Principled detection of speculative infor mation flows END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7251AoVHP1@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20191008T160000 DTEND:20191008T180000 DURATION:PT2H0M0S LOCATION:Seminar Room\, ground floor (Building IMAG) SUMMARY:Valentin TOUZEAU - Static Analysis of Least Recently Used Caches: C omplexity\, Optimal Analysis\, and Applications to Worst-Case Execution Ti me and Security END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7252vJ3Zlv@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190926T140000 DTEND:20190926T153000 DURATION:PT1H30M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Pierre-Jean Meyer - Reachability analysis and decompositions for ab straction-based control synthesis END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7253H2I8UN@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190920T090000 DTEND:20190920T110000 DURATION:PT2H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:-- Oded Maler Memorial Day - Oded Maler Memorial Day END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7254dIvRfU@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190919T140000 DTEND:20190919T153000 DURATION:PT1H30M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Martin Franzle - What’s to Come is Still Unsure: Automatically Synt hesizing and Verifying Controllers Resilient to Delayed Interaction END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7254Vxs3MH@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190711T140000 DTEND:20190711T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Eric Gascard - Quantitative Analysis of Dynamic Fault Trees by mea ns of Monte Carlo Simulations: Event-Driven Simulation Approach ( Quantita tive Analysis of Dynamic Fault Trees by means of Monte Carlo Simulations: Event-Driven Simulation Approach) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7255u7wRI7@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190709T140000 DTEND:20190709T150000 DURATION:PT1H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Lionel Rieg - Integrating Formal Schedulability Analysis into a Ver ifed OS Kernel END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7255i0oLpU@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190704T140000 DTEND:20190704T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Radu IOSIF - Alternating Automata Modulo First Order Theories END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7256VEDBrm@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190702T140000 DTEND:20190702T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Indranil Saha - Developing Autonomous Multi-Robot Systems for Comp lex Missions END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7257Ccu8Jc@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20190628T140000 DTEND:20190628T180000 DURATION:PT4H0M0S LOCATION:Seminar Room\, ground floor (Building IMAG) SUMMARY:Braham Lotfi Mediouni - Modeling and Analysis of Stochastic Real-Ti me Systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7258SUC4dk@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20190626T140000 DTEND:20190626T160000 DURATION:PT2H0M0S LOCATION:Seminar Room Part 1\, ground floor (Building IMAG) SUMMARY:Rany Kahil - Schedulability in Mixed- criticality Systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7259csBkTl@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190625T140000 DTEND:20190625T160000 DURATION:PT2H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Hernan Ponce de Leon - BMC with Weak Memory Models END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7260clj1PW@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190614T140000 DTEND:20190614T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Benoit Barbot - Cosmos a quantitative verification tool for large s tochastic systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-72613VlRhr@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190613T140000 DTEND:20190613T150000 DURATION:PT1H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Simon IOSTI - Using neural networks to improve performances of corr ect-by-construction controllers END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7262zI3eEv@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190509T140000 DTEND:20190509T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Saddek Bensalem - Engineering Trustworthy Learning-Enabled Autono mous Systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7262VcT2iv@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190502T140000 DTEND:20190502T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Michael PERIN - Découvrir AMC en 45 Questions a Choix Multiples END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-72630TJ5DL@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190429T094500 DTEND:20190429T154500 DURATION:PT6H0M0S LOCATION:Seminar Room\, ground floor (Building IMAG) SUMMARY:Invited Speakers - Journée thématique Verimag : Many-core Kalray MP PA\, implementation and verification END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7264OvXzvv@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190405T140000 DTEND:20190405T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Radu IOSIF - On the Expressive Completeness and Complexity of Prene x Separation Logic END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7264vrUd2e@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190404T140000 DTEND:20190404T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Radu IOSIF - Checking Deadlock-Freedom of Parametric Component-Base d Systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7265mVggVl@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190401T100000 DTEND:20190401T120000 DURATION:PT2H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Edward A. Lee - Living Digital Beings END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7266iVA6UL@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190328T140000 DTEND:20190328T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Olivier VIDAL - Matières premières et énergie à l’échelle mondiale dans le contexte de la transition énergétique END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-726676vEON@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20190320T140000 DTEND:20190320T160000 DURATION:PT2H0M0S LOCATION:Rim El Ballouli SUMMARY:Rim El Ballouli - Modeling Self-configuration in Architecture-based Self-adaptive systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7267BM6Usw@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190308T100000 DTEND:20190308T110000 DURATION:PT1H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Mathias Bourgoin - An overview of the Tezos blockchain END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-72682sLlbd@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20190222T133000 DTEND:20190222T163000 DURATION:PT3H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Moustapha Lo - Implementing a Real-time Avionic application on a Ma nycore Processor END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7268ercOSx@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190218T140000 DTEND:20190218T160000 DURATION:PT2H0M0S LOCATION:IMAG Auditorium SUMMARY:Guillaume Baudart - Probabilistic Reactive Programming (Probabilist ic Reactive Programming) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7269Liuz3U@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190214T140000 DTEND:20190214T160000 DURATION:PT2H0M0S LOCATION:Auditorium (ground floor) SUMMARY:Nikos Gorogiannis - Concurrency bug detection at scale with Infer END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7270k8KFwN@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190207T140000 DTEND:20190207T150000 DURATION:PT1H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Jacques COMBAZ - L'assemblage des composants en BIP (Assembling Com ponents in BIP) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7270lbku0H@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190125T140000 DTEND:20190125T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Tom Yamaguchi - Application of Abstract Interpretation to the Autom otive Electronic Control System END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7271XiUO5F@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190124T140000 DTEND:20190124T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Maiza Claire - WCET and interference analysis for multicore sy stems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7487CdDFUI@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190122T140000 DTEND:20190122T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Georg Struth - Verifying Hybrid Systems with Modal Kleene Algebra END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7489I5RWfT@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190121T140000 DTEND:20190121T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Sergio Yovine - Formal specification and implementation of an auto mated pattern-based parallel-code generation framework END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-74906eC9je@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190118T140000 DTEND:20190118T150000 DURATION:PT1H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Chi-Hong Cheng - When neural networks meet dependability END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7491DOaKAG@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190117T140000 DTEND:20190117T153000 DURATION:PT1H30M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Paolo Torrini - Reifying and translating a monadic fragment of Gall ina END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7492JiI9hP@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190108T140000 DTEND:20190108T160000 DURATION:PT2H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Michal Valko - The power of graphs in speeding up online learning a nd decision making END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7492nVIGCW@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20190107T140000 DTEND:20190107T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Michal Valko - A simple parameter-free and adaptive approach to opt imization under a minimal local smoothness assumption END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7493uUTWcU@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20181219T140000 DTEND:20181219T160000 DURATION:PT2H0M0S LOCATION:Room 248\, IMAG SUMMARY:Khalil Ghorbal - Simulating and Verifying Cyber-Physical Systems: C urrent Challenges and Novel Research Directions END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-74941osnD9@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20181217T140000 DTEND:20181217T160000 DURATION:PT2H0M0S LOCATION:Seminar Room 2\, ground floor (Building IMAG) SUMMARY:NIKOLAOS KEKATOS - Vérification formelle des systèmes cyber-physiqu es dans le processus industriel de la conception basée sur modèle (Formal Verification of Cyber-Physical Systems in the Industrial Model-Based Desig n Process) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7494T3I1Zk@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20181211T140000 DTEND:20181211T150000 DURATION:PT1H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Bibek Kabi - Combining Zonotope Abstraction and Constraint Programm ing for Synthesizing Inductive Invariants END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7495U8deWc@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20181206T140000 DTEND:20181206T153000 DURATION:PT1H30M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Joseph Sifakis - On the Nature of Autonomy: A Rigorous Architectura l Characterization END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7496KhCZBe@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20181129T140000 DTEND:20181129T160000 DURATION:PT2H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Sylvain Boulmé - Importation d'oracles ML impératifs dans du code C oq vérifié END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7496BlAOSa@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20181122T100000 DTEND:20181122T163000 DURATION:PT6H30M0S LOCATION:Auditorium (Building IMAG) SUMMARY:analyse et verif. legeres Une journee de reflexion - Techniques d'a nalyse et de verification legeres (Lightweight analysis and verification techniques) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7497B1vCDE@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20181116T103000 DTEND:20181116T123000 DURATION:PT2H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Amaury Graillat - Parallel Code Generation of Synchronous Programs for a Many-core Architecture END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-74988Zp1B9@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20181031T140000 DTEND:20181031T170000 DURATION:PT3H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Mahieddine DELLABANI - Formal Methods for Distributed Real-Time Sys tems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7498pxe4Wg@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20181023T140000 DTEND:20181023T150000 DURATION:PT1H0M0S LOCATION:Room 206 (2nd floor\, restricted access) SUMMARY:Thusitha Asela Bandara - Un protocole de charge adaptatif pour les batteries Lithium-lon (An Adaptive Charge Protocol for Lithium-lon Batteri es) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-74995EKw1A@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20181011T140000 DTEND:20181011T160000 DURATION:PT2H0M0S LOCATION:Amphi D1\, DLST SUMMARY:Florent Chevrou - Formalisation of Asynchronous Interactions END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7500MDEdlA@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20181004T153000 DTEND:20181004T173000 DURATION:PT2H0M0S LOCATION:Salle Séminaire (rez-de-chaussée Bât IMAG) SUMMARY:Erwan Jahier - [Technical Seminar] A gentle introduction to Gitlab- CI and docker END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7500AkuTlb@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20180920T140000 DTEND:20180920T153000 DURATION:PT1H30M0S LOCATION:Salle 206 SUMMARY:Cyril Six - Compilateur CompCert certifié pour processeur VLIW Kalr ay (Extending the CompCert certified compiler for a VLIW processor of Kalr ay) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7501b9c0a1@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20180913T140000 DTEND:20180913T150000 DURATION:PT1H0M0S LOCATION:Salle 206 (salle Chamois) SUMMARY:Franz Mayr - Regular inference on artificial neural networks END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7502uKcGFk@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20180625T100000 DTEND:20180625T120000 DURATION:PT2H0M0S LOCATION:Room 206 SUMMARY:Stefano Berardi - Martin-Lof's Inductive Definitions Are Not Equiva lent to Cyclic Proofs END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7503f3UmEW@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20180622T110000 DTEND:20180622T120000 DURATION:PT1H0M0S LOCATION:Seminar Room\, ground floor (Building IMAG) SUMMARY:Pallab Dasgupta - Verification challenges in the Power Management f abric of Integrated Circuits END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7504iatMWD@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20180531T140000 DTEND:20180531T160000 DURATION:PT2H0M0S LOCATION:Auditorium (IMAG) SUMMARY:Cristina Serban - Raisonnement automatisé pour la Logique de Sépara tion avec des définitions inductives (Automated Reasoning in Separation Lo gic with Inductive Definitions) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7504MVtUf4@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20180517T140000 DTEND:20180517T150000 DURATION:PT1H0M0S LOCATION:salle 206 SUMMARY:Michael PERIN - Automatic Grading: take a CEGAR and let the machine do your work END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7505LvD7uU@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20180516T140000 DTEND:20180516T160000 DURATION:PT2H0M0S LOCATION:Auditorium (IMAG) SUMMARY:Arvind Adimoolam - A Calculus of Complex Zonotopes for Computing In variants of Affine Hybrid Systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7506ut43Dj@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20180515T140000 DTEND:20180515T160000 DURATION:PT2H0M0S LOCATION:Batiment IMAG\, Salle 206 SUMMARY:Luc Jaulin - Computing inner and outer approximations of forward re ach sets of a nonlinear dynamical system END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7506r3ubS7@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20180507T133000 DTEND:20180507T170000 DURATION:PT3H30M0S LOCATION:Auditorium (IMAG) SUMMARY:Alexandre Rocca - Méthodes formelles pour la modélisation et la val idation de modèles biologiques (Formal methods for modelling and validatio n of biological models) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7507ZPtN8x@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20180417T110000 DTEND:20180417T120000 DURATION:PT1H0M0S LOCATION:Meeting room 206 (IMAG) SUMMARY:Jim Kapinski - Verification of Learning-Enabled\, Cyber-Physical Sy stems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7508RVDamv@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20180412T140000 DTEND:20180412T150000 DURATION:PT1H0M0S LOCATION:IMAG 206 SUMMARY:Maria Méndez Real - Cache-based attacks and spatial isolation count ermeasure on multi and many-core architectures END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7508flGV4x@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20180322T150000 DTEND:20180322T160000 DURATION:PT1H0M0S LOCATION:206 SUMMARY:Anastasia Volkova - Towards reliable implementation of digital filt ers. How digital signal processing and computer arithmetic meet (candidate poste MCF) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7509juJL0G@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20180322T160000 DTEND:20180322T170000 DURATION:PT1H0M0S LOCATION:206 SUMMARY:Guilhem Jaber - Model-checking contextual equivalence of higher-ord er programs with references (candidat poste MCF) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7510vX1usP@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20180319T140000 DTEND:20180319T150000 DURATION:PT1H0M0S LOCATION:salle 206 SUMMARY:Benjamin Farinier - Model Generation for Quantified Formulas: A Tai nt-Based Approach END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-75105Pm7Uh@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20180315T150000 DTEND:20180315T160000 DURATION:PT1H0M0S LOCATION:206 SUMMARY:Ayoub Nouri - ASTROLABE: A Rigorous Approach for System-Level Perf ormance Modeling and Analysis (candidat poste MCF) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7511UREjmB@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20180315T140000 DTEND:20180315T150000 DURATION:PT1H0M0S LOCATION:206 SUMMARY:Lionel Rieg - Extending a verified OS kernel for real-time END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-76145E4P4E@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20180308T140000 DTEND:20180308T160000 DURATION:PT2H0M0S LOCATION:206 SUMMARY:Ivan Gazeau - Automated verification of privacy-type properties fo r security protocols (MCF Candidate) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7615ngh1z3@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20180215T140000 DTEND:20180215T160000 DURATION:PT2H0M0S LOCATION:Room 204 SUMMARY:Gheorghe Stefanescu - Adaptive systems made by self-assembling hete rogeneous components within regular 2D patterns END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-76168x2Upu@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20180205T103000 DTEND:20180205T123000 DURATION:PT2H0M0S LOCATION:Auditorium (IMAG) SUMMARY:Maxime Puys - Sécurité des systèmes industriels : filtrage applicat if et recherche de scénarios d’attaques (Cybersecurity of Industrial Syste ms: Applicative Filtering and Generation of Attack Scenarios) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7617AaaO0a@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20180118T140000 DTEND:20180118T150000 DURATION:PT1H0M0S LOCATION:ENSIMAG Amphi E SUMMARY:David Monniaux - SPECTRE + MELTDOWN END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7617S4ome3@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20180115T140000 DTEND:20180115T170000 DURATION:PT3H0M0S LOCATION:Seminar Room\, ground floor (Building IMAG) SUMMARY:Dogan Ulus - Filtrage par Motif Temporisé: Théorie et Applications (Pattern Matching with Time: Theory and Applications) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7618rntXLV@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20171221T140000 DTEND:20171221T150000 DURATION:PT1H0M0S LOCATION:206 SUMMARY:Mirco Giacobbe - Counterexample-guided Refinement of Template Polyh edra END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-76194jElao@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20171211T140000 DTEND:20171211T160000 DURATION:PT2H0M0S LOCATION:Auditorium (IMAG) SUMMARY:Alexandre Maréchal - New Algorithmics for Polyhedral Calculus via P arametric Linear Programming END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7620hgdsWO@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20171211T140000 DTEND:20171211T170000 DURATION:PT3H0M0S LOCATION:Seminar Room\, ground floor (Building IMAG) SUMMARY:Denis Becker - Simulation SystemC/TLM Parallèle de Composants Matér iels Décrits pour la Synthèse de Haut Niveau (Parallel SystemC/TLM Simulat ion of Hardware Components Described for High-Level Synthesis) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7620SCsTIL@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20171207T140000 DTEND:20171207T160000 DURATION:PT2H0M0S LOCATION:Seminar Room\, ground floor (Building IMAG) SUMMARY:De Oliviera Steven - Synthesizing Invariants by Solving Solvable L oops END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7621SsIV0w@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20171201T150000 DTEND:20171201T160000 DURATION:PT1H0M0S LOCATION:Salle 206 IMAG SUMMARY:Reineke Jan - On the Smoothness of Paging Algorithms END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7622eWle6l@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20171201T100000 DTEND:20171201T120000 DURATION:PT2H0M0S LOCATION:Amphi H\, Ensimag SUMMARY:Hamza RIHANI - Analyse temporelle des systèmes temps-réels sur arch itectures pluri-cœurs avec application à un processeur industriel (Many-Co re Timing Analysis of Real-Time Systems and its Application to an Industri al Processor) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7623vSAK6H@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20171123T140000 DTEND:20171123T160000 DURATION:PT2H0M0S LOCATION:Salle de séminaire (rez-de-chaussée) SUMMARY:Joseph Sifakis - How Much Hard is System Design? END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7623ASSvxU@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20171020T101500 DTEND:20171020T121500 DURATION:PT2H0M0S LOCATION:Ensimag Amphi H SUMMARY:Franck De Goer - Rétro-ingénierie de programmes binaires en une exé cution - une analyse dynamique légère basée au niveau des fonctions (Rever se Engineering binary code in one execution - A lightweight function based dynamic execution.) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7624UkO0BX@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20171019T103000 DTEND:20171019T170000 DURATION:PT6H30M0S LOCATION:Seminar Room 2\, ground floor (Building IMAG) SUMMARY: - COQ en STOCK END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7625mSDwiT@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20171010T103000 DTEND:20171010T123000 DURATION:PT2H0M0S LOCATION:Seminar Room 1\, ground floor (Building IMAG) SUMMARY:Frits Vaandrager - Learning Mealy Machines with Timers END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7625NRwCum@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20171010T140000 DTEND:20171010T160000 DURATION:PT2H0M0S LOCATION:Auditorium (IMAG) SUMMARY:Irini Eleftheria Mens - Learning Regular Languages over Large Alpha bets END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7626BaTB1v@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20170928T140000 DTEND:20170928T150000 DURATION:PT1H0M0S LOCATION:206 SUMMARY:Adrien Guatto - A Functional Language with Time Warps END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-76270GgKcN@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20170914T140000 DTEND:20170914T160000 DURATION:PT2H0M0S LOCATION:Room 106\, 1st floor SUMMARY:Joël Goossens - Feasibility & Simulation Intervals of Schedules for Recurrent Real-Time Tasks END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7627UgrfIv@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20170901T093000 DTEND:20170901T113000 DURATION:PT2H0M0S LOCATION:Auditorium (IMAG) SUMMARY:Anaïs Durand - Algorithmes distribués efficaces adaptés à un contex te incertain (Efficient Distributed Algorithms Suited for Uncertain Contex t) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7628RHHUXJ@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20170831T101500 DTEND:20170831T170000 DURATION:PT6H45M0S LOCATION:Seminar Room\, ground floor (Building IMAG) SUMMARY: - Workshop ESTATE/VERIMAG 'Distributed Algorithms' END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-76293GgVcF@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20170712T140000 DTEND:20170712T160000 DURATION:PT2H0M0S LOCATION:Auditorium (IMAG) SUMMARY:Manuel Barragan - Feature selection and design for machine learning -based test of analog\, mixed-signal and RF circuits END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7630PTBJOr@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20170626T140000 DTEND:20170626T160000 DURATION:PT2H0M0S LOCATION:Auditorium (IMAG) SUMMARY:Hosein Nazarpour - Surveillance de systèmes à composants multi-thre ads et distribués (Monitoring Multi-Threaded and Distributed (Component-Ba sed) Systems) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7630g54unB@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20170608T140000 DTEND:20170608T160000 DURATION:PT2H0M0S LOCATION:Seminar Room\, ground floor (Building IMAG) SUMMARY:Assalé ADJE - Itérations sur les politiques pour la vérification de systèmes dynamiques en temps discret. END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7631JZZVPf@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20170606T140000 DTEND:20170606T160000 DURATION:PT2H0M0S LOCATION:Amphi E Ensimag 681\, rue de la passerelle - Campus SUMMARY:Laurent Lemke - Modèles partagés et infrastructure ouverte pour l’i nternet des objets de la ville intelligente END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7632PduTZs@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20170510T090000 DTEND:20170510T110000 DURATION:PT2H0M0S LOCATION:Auditorium (IMAG) SUMMARY:Yuliia Romenska - Composants abstraits pour la vérification fonctio nnelle des systèmes sur puce (High-Level Component-Based Models for Functi onal Verification of Systems-on-a-Chip) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7633BC6BFM@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20170420T140000 DTEND:20170420T160000 DURATION:PT2H0M0S LOCATION:Room 206 (Building IMAG) SUMMARY:Vincent Penelle - On the context-freeness problem for vector additi on systems. (candidat MCF) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-763368Fbz8@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20170419T140000 DTEND:20170419T153000 DURATION:PT1H30M0S LOCATION:206 SUMMARY:Liliana Andrade - High Level Modeling and Simulation of Heterogeneo us Systems: A focus on the SystemC-AMS Synchronization Problem END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7634pHSx31@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20170411T110000 DTEND:20170411T123000 DURATION:PT1H30M0S LOCATION:206 SUMMARY:Iulia Dragomir - Compositional Design and Analysis of Embedded Syst ems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-763587taho@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20170330T140000 DTEND:20170330T150000 DURATION:PT1H0M0S LOCATION:IMAG 206 SUMMARY:Helmut Seidl - Enforcing Termination of Interprocedural Analysis END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-76365RVgeK@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20170330T100000 DTEND:20170330T120000 DURATION:PT2H0M0S LOCATION:IMAG 206 SUMMARY:Dirk Beyer - Correctness Witnesses: Exchanging Verification Results between Verifiers END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7636EPoKsN@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20170329T103000 DTEND:20170329T123000 DURATION:PT2H0M0S LOCATION:Auditorium (IMAG) SUMMARY:Josselin FEIST - Finding the Needle in the Heap: Combining Binary A nalysis Techniques to Trigger Use-After-Free END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7637zCVzv8@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20170329T140000 DTEND:20170329T170000 DURATION:PT3H0M0S LOCATION:Auditorium (IMAG) SUMMARY:Egor Karpenkov - Finding Inductive Invariants using SMT Solving and Convex Optimization END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7638Xr8xS1@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20170328T140000 DTEND:20170328T150000 DURATION:PT1H0M0S LOCATION:IMAG 206 SUMMARY:Nikolaj Bjorner - Network Verification for Microsoft Azure END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7638TP2sDP@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20170323T153000 DTEND:20170323T163000 DURATION:PT1H0M0S LOCATION:206 SUMMARY:Romaric Ludinard - Bitcoin\, la blockchain et le problème de la dou ble dépense : état des lieux et analyse de propositions d'améliorations (B itcoin\, its blockchain and the double spending problem : Bitcoin in a nut shell and safety analysis of recent improvement proposals) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7639V5dx6B@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20170323T140000 DTEND:20170323T153000 DURATION:PT1H30M0S LOCATION:206 SUMMARY:Hugues Evrard - Automated generation of a distributed implementatio n from a formal model of concurrent processes interacting via multiway ren dezvous. END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7640zTkXHS@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20170316T150000 DTEND:20170316T160000 DURATION:PT1H0M0S LOCATION:206 SUMMARY:Manuel Selva - Exécution efficace sur machine multi-cœur (Efficient execution on multi-core systems) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-76409dZPJ3@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20170309T153000 DTEND:20170309T163000 DURATION:PT1H0M0S LOCATION:206 SUMMARY:Lionel Rieg - Formal Proofs of Safety in Coq: Mobile Robot Networks and Lustre Compilation END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7641EkjwNu@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20170309T140000 DTEND:20170309T150000 DURATION:PT1H0M0S LOCATION:206 SUMMARY:Arthur Milchior - Deterministic Automaton and logically definable sets of numbers. END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7642o7A3uW@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20170302T164500 DTEND:20170302T181500 DURATION:PT1H30M0S LOCATION:206 SUMMARY:Paulin Fournier - Verification of infinite probabilistic systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7642NJ7Usl@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20170302T153000 DTEND:20170302T163000 DURATION:PT1H0M0S LOCATION:206 SUMMARY:Nicolas Basset - Uniform Sampling for Timed Automata with Applicati on to Language Inclusion Measurement END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7643og08Xj@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20170302T140000 DTEND:20170302T160000 DURATION:PT2H0M0S LOCATION:Seminar Room 1\, ground floor (Building IMAG) SUMMARY:Loïc Correnson - « De Frama-C à Lustre » (« From Frama-C to Lustre ») END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7644vVGGd5@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20170216T100000 DTEND:20170216T110000 DURATION:PT1H0M0S LOCATION:Seminar Room\, ground floor (Building IMAG) SUMMARY:Naor Seffi - Multi-label Classification with Pairwise Relations END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7644Fx0p8P@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20170216T140000 DTEND:20170216T144500 DURATION:PT0H45M0S LOCATION:Seminar Room\, ground floor (Building IMAG) SUMMARY:Abhinav Srivastav - Trade-offs in Resource Allocation Problems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7645dxJEHS@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20170216T110000 DTEND:20170216T120000 DURATION:PT1H0M0S LOCATION:Seminar Room\, ground floor (Building IMAG) SUMMARY:Mastrolilli Monaldo - High Degree Sum of Squares Proofs/Hierarchy f or 0/1 Problems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-76469R3aB8@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20170209T140000 DTEND:20170209T170000 DURATION:PT3H0M0S LOCATION:Salle 206 SUMMARY: - Second Year PhD Students Seminars - week 2/2 END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7646j4em0C@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20170202T140000 DTEND:20170202T162000 DURATION:PT2H20M0S LOCATION:Seminar Room\, ground floor (Building IMAG) SUMMARY: - Second Year PhD Students Seminars - week 1/2 END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7647ClsS6A@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20161205T170000 DTEND:20161205T183000 DURATION:PT1H30M0S LOCATION:Auditorium (IMAG) SUMMARY:Paul FEAUTRIER - New Architectures\, New Compilation Problems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-764898FJRj@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20161117T143000 DTEND:20161117T153000 DURATION:PT1H0M0S LOCATION:Salle 106 SUMMARY:Robin David - Formal Approaches for Automatic Deobfuscation and Rev erse-engineering of Protected Codes END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7649NSzB0x@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20161107T140000 DTEND:20161107T160000 DURATION:PT2H0M0S LOCATION:Auditorium (IMAG) SUMMARY:Najah BEN SAID - Sécurité de Flux d'Information dans les Modèles à Base de Composant: De la Vérification à l'Implementation (Information Flow Security in Component Based Models: From Verification to Implementation) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7649kapOs3@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20161104T140000 DTEND:20161104T170000 DURATION:PT3H0M0S LOCATION:Souha Ben Rayana SUMMARY:Souha Ben Rayana - Vérification compositionnelle des systèmes temps -réels à base de compsants et applications. (Compositional Verification of Component-Based Real-time Systems and Applications.) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7650KcuWr8@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20161102T140000 DTEND:20161102T150000 DURATION:PT1H0M0S LOCATION:ROOM 206 SUMMARY:Nikos Gorogiannis - Biabduction (and Related Problems) in Array Sep aration Logic END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7651esiXlj@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20161028T100000 DTEND:20161028T120000 DURATION:PT2H0M0S LOCATION:VERIMAG (Room 206\, 2nd floor) SUMMARY:J. Esparza\, A. Bouajjani\, and D. Nickovic - Verification: Theory and Practice END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7651JVh5vK@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20161028T150000 DTEND:20161028T170000 DURATION:PT2H0M0S LOCATION:Seminar Room\, ground floor (Building IMAG) SUMMARY:Thomas FERRERE - Assertion and Measurements for Mixed-Signal Simula tion END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-765223JExM@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20161027T140000 DTEND:20161027T160000 DURATION:PT2H0M0S LOCATION:Auditorium (IMAG) SUMMARY:Joseph Sifakis - Modeling architectures and their properties in BIP END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7653LIHwPW@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20161013T161500 DTEND:20161013T171500 DURATION:PT1H0M0S LOCATION:206 SUMMARY:Ismail Oukid - Storage Class Memory (aka NVRAM): Challenges and Opp ortunities END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7654TNUDVV@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20161012T100000 DTEND:20161012T120000 DURATION:PT2H0M0S LOCATION:Auditorium (IMAG) SUMMARY:Louis Dureuil - Analyse de code et processus d’évaluation des compo sants sécurisés contre l’injection de faute END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7654FlVWU8@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20161006T153000 DTEND:20161006T163000 DURATION:PT1H0M0S LOCATION:Room 206 (building IMAG) SUMMARY:Cristina SERBAN - A Decision Procedure for Separation Logic in SMT END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-76553UzpTg@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20160929T113000 DTEND:20160929T123000 DURATION:PT1H0M0S LOCATION:Auditorium (Builbing IMAG) SUMMARY:Parosh Abdulla - Automatic Verification of Linearization Policies END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-765512jvl4@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20160929T103000 DTEND:20160929T113000 DURATION:PT1H0M0S LOCATION:Auditorium (Builbing IMAG) SUMMARY:Joel Ouaknine - Decision Problems for Linear Dynamical Systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7656h811Sv@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20160929T093000 DTEND:20160929T103000 DURATION:PT1H0M0S LOCATION:Auditorium (Builbing IMAG) SUMMARY:Andreas Podelski - Thread Modularity on the Next Level END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7657RvHCvc@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:HDR DTSTART:20160929T140000 DTEND:20160929T170000 DURATION:PT3H0M0S LOCATION:Auditorium (Builbing IMAG) SUMMARY:Radu Iosif - Automata and Logics for Program Verification END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7658j7zTUL@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20160705T100000 DTEND:20160705T120000 DURATION:PT2H0M0S LOCATION:IMAG building\, Room 206 SUMMARY:Jyo Deshmukh - Recent progress on formal methods for CPS END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7658mgK93I@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20160705T140000 DTEND:20160705T160000 DURATION:PT2H0M0S LOCATION:Auditorium IMAG SUMMARY:Rahul Mangaram - Challenges with Medical Cyber-Physical Systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7659TVTnZs@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20160630T140000 DTEND:20160630T150000 DURATION:PT1H0M0S LOCATION:206 SUMMARY:Sergiy Bogomolov - Scalable Static Hybridization Methods for Analys is of Nonlinear Systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7660B6iuut@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20160622T140000 DTEND:20160622T160000 DURATION:PT2H0M0S LOCATION:New IMAG building Auditorium SUMMARY:Heiko FALK - WCET-Aware Compilation and Optimization for Real-Time Systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-76606PLKwV@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20160616T140000 DTEND:20160616T160000 DURATION:PT2H0M0S LOCATION:Auditorium du Bât IMAG SUMMARY:Jan Lanik - Power reduction in sequential circuits END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7661FZRwWG@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:HDR DTSTART:20160526T170000 DTEND:20160526T190000 DURATION:PT2H0M0S LOCATION:amphithéâtre\, bâtiment IMAG de l'Univ. G SUMMARY:Frehse Goran - Scalable Verification of Hybrid Systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7662BJ8NXu@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20160512T140000 DTEND:20160512T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Bruno Grenet - Factorisation de polynômes lacunaires END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-766232PxSs@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20160428T140000 DTEND:20160428T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Camille Coti - Parallel\, distributed behavioral cartography of par ametric timed automata END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7663uAoef8@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20160324T140000 DTEND:20160324T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Amaury Pouly - Solvability of Matrix-Exponential Equations END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-76647mFVAO@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20160309T090000 DTEND:20160309T100000 DURATION:PT1H0M0S LOCATION:Maison Jean Kuntzmann (MJK) SUMMARY:Alan Burns - Mixed Criticality - A Personal View END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7664UADHVT@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20160309T100000 DTEND:20160309T110000 DURATION:PT1H0M0S LOCATION:Maison Jean Kuntzmann (MJK) SUMMARY:Sanjoy Baruah - Mixed-criticality Scheduling on Multiprocessors END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7665Cc0uGB@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20160309T110000 DTEND:20160309T120000 DURATION:PT1H0M0S LOCATION:Maison Jean Kuntzmann (MJK) SUMMARY:Luca Santinelli - Mixed-Criticalities and Probabilities END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7666ZpuuVb@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20160309T140000 DTEND:20160309T160000 DURATION:PT2H0M0S LOCATION:Maison Jean Kuntzmann (MJK) SUMMARY:Dario Socci - Scheduling of Certifiable Mixed-Criticality Systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7666hZupU4@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20160302T140000 DTEND:20160302T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Alexey Bakhirkin - Towards finding non-terminating behaviours in p rograms END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-78712ece3V@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20160301T140000 DTEND:20160301T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Arnaud Sangnier - On the Complexity of Verifying Regular Properties on Flat Counter Systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7873STMZV8@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20160204T140000 DTEND:20160204T170000 DURATION:PT3H0M0S LOCATION:salle A. Turing CE4 SUMMARY: - PhD Seminars END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7874Vtaao0@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20160129T100000 DTEND:20160129T120000 DURATION:PT2H0M0S LOCATION:CTL SUMMARY:Mathilde Duclos - Méthodes pour la vérification des protocoles cryp tographiques dans le modèle calculatoire (Methods for cryptographic protoc ol verification in the computational model ) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-78755Ia2V6@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20160128T140000 DTEND:20160128T170000 DURATION:PT3H0M0S LOCATION:salle A. Turing CE4 SUMMARY: - PhD Seminars END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7875rDodpc@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20160107T140000 DTEND:20160107T170000 DURATION:PT3H0M0S LOCATION:salle A. Turing CE4 SUMMARY: - Phd Seminars END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7876r04rRO@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20151210T133000 DTEND:20151210T153000 DURATION:PT2H0M0S LOCATION:CTL SUMMARY:Alexios Lekidis - Design flow for the rigorous development of netwo rked embedded systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7877EgI5vv@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20151210T100000 DTEND:20151210T120000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:PEKTAŞ Abdurrahman - Behavior based malware classification using on line machine learning END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7878KuUHXN@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20151016T093000 DTEND:20151016T103000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Enea Zaffanella - A Few Notes on the Implementation of Convex Polyh edra Using the Double Description Framework END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7878srFDoc@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20151015T100000 DTEND:20151015T110000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Andy King - The Ying and the Yang of Binary Reversing END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7879l1SekH@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20151015T140000 DTEND:20151015T160000 DURATION:PT2H0M0S LOCATION:CTL SUMMARY:Alexis Fouilhe - Revisiting the abstract domain of polyhedra: const raints-only representation and formal proof END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-788024GDFV@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20151014T140000 DTEND:20151014T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Chantal Keller - F*: Higher-Order Effectful Program Verification END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7880eFuxw8@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20150918T100000 DTEND:20150918T120000 DURATION:PT2H0M0S LOCATION:Amphiteatre Maison Jean Kuntzmann SUMMARY:Ali Kassem - Vérification automatique de protocoles d'examen\, de m onnaie\, de réputation\, et de routage (Automated Verification of Exam\, C ash\, Reputation\, and Routing Protocols) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7881Us7c7x@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20150910T140000 DTEND:20150910T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY: Julien Signoles Nikolai Kosmatov - Combinations of Static and Dyna mic Analyses in Frama-C: An Overview (Combinations of Static and Dynamic A nalyses in Frama-C: An Overview) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7882ReW5Hf@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20150903T140000 DTEND:20150903T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Amaury Pouly - On the complexity of some continuous space reachabil ity problems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7882F4O22J@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20150702T140000 DTEND:20150702T160000 DURATION:PT2H0M0S LOCATION:Amphi E ENSIMAG SUMMARY:Christos H. Papadimitriou - Life under the Lens END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7883UPdzhX@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20150625T140000 DTEND:20150625T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Pablo Buiras - Mixing Static and Dynamic Typing for Information-Fl ow Control in Haskell END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7884U6Lr30@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20150611T140000 DTEND:20150611T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Chris Myers - LEMA: A Tool for the Formal Verification of Digitally -Intensive Analog/Mixed-Signal Circuits END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7884Lun2OK@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20150609T133000 DTEND:20150609T153000 DURATION:PT2H0M0S LOCATION:MJK SUMMARY:Ahlem TRIKI - Distributed Implementations of Timed Component-based Systems (Implémentations Distributés des Systems Temps-réel à base de Comp osants) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7885cUN4ct@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20150528T140000 DTEND:20150528T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Andrew Reynolds - Using CVC4 for Proofs by Induction in SMT END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-788653nCbl@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20150408T133000 DTEND:20150408T163000 DURATION:PT3H0M0S LOCATION:CTL (Amphitheater) SUMMARY:Ayoub Nouri - Rigorous System-level Modeling and Performance Evalua tion for Embedded System Design END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7886bzk3pB@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20150403T140000 DTEND:20150403T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Damien Pous - Algorithms for language equivalence of finite automat a END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7887mJL60d@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20150219T140000 DTEND:20150219T170000 DURATION:PT3H0M0S LOCATION:salle A. Turing CE4 SUMMARY: Seminaires doctorants 3 - Verimag PhD seminars 3 END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-78885HHZWo@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20150212T140000 DTEND:20150212T170000 DURATION:PT3H0M0S LOCATION:salle A. Turing CE4 SUMMARY: Seminaires doctorants 2 - Verimag PhD seminars 2 END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7889oULHU8@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20150205T140000 DTEND:20150205T163000 DURATION:PT2H30M0S LOCATION:salle A. Turing CE4 SUMMARY: Seminaires doctorants 1 - Verimag PhD seminars 1 END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7889KuuTPV@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20150129T140000 DTEND:20150129T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Jim Kapinski - Applying V&V technologies to automotive engine cont rol: challenges and directions END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7890CadUXL@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20150115T140000 DTEND:20150115T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Alexandre Marechal - A new Linearization Technique for Multivariate Polynomials Using Convex Polyhedra Based on Handelman-Krivine's Theorem END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-78911TsN83@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20141210T140000 DTEND:20141210T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Cristina Serban - An Introduction to Separation Logic END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7891xv6m9g@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20141121T140000 DTEND:20141121T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Chih-Hong Cheng - G4LTL-ST - Automatic Generation of PLC programs END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7892GTAcW6@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20141113T133000 DTEND:20141113T153000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Victor Magron - New applications of moment-SOS hierarchies END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7893xx7sdF@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20141107T140000 DTEND:20141107T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Jean-Baptiste Jeannin - Differential Temporal Dynamic Logic for Hyb rid Systems and Airplane Collision Avoidance END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-78933V1SZI@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20141015T140000 DTEND:20141015T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Andreas Podelski - Proof Spaces for Unbounded Parallelism END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7894vu1HPm@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20141014T140000 DTEND:20141014T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Andreas Podelski - Static Analysis Modulo Theory END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-78955GNvUE@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20141013T133000 DTEND:20141013T153000 DURATION:PT2H0M0S LOCATION:CTL SUMMARY:Pranav TENDULKAR - Allocation et Ordonnancement sur des processeurs multi-coeur avec des solveurs SMT (Mapping and Scheduling on Multi-core P rocessors using SMT Solvers) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7896rIXB0T@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20141013T153000 DTEND:20141013T173000 DURATION:PT2H0M0S LOCATION:Amphithéâtre - Maison Jean Kuntzmann SUMMARY:Julien Henry - Analyse statique de programmes par interprétation ab straite et procédures de décision (Static Analysis by Abstract Interpretat ion and Decision Procedures) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7896P93Mdn@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20141009T103000 DTEND:20141009T123000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Kim Quyên Lý - Verification automatique de certificats de terminais on (Automated verification of termination certificates) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7897Nz2CEU@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20141003T140000 DTEND:20141003T170000 DURATION:PT3H0M0S LOCATION:Maison Jean Kuntzmann SUMMARY:Raphaël Jamet - Protocoles et Modèles pour la Sécurité des Réseaux Ad Hoc Sans-Fil (Protocols and Models for the Security of Wireless Ad Hoc Networks) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7898svAI2Z@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20140912T140000 DTEND:20140912T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Jean-Marc Vincent - A Spatiotemporal Data Aggregation Technique for the Macroscopic Analysis of Large-scale Systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7898niS28L@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20140528T140000 DTEND:20140528T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Dejan Nickovic - Require\, Test and Trace It END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7899gtuidz@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20140428T130000 DTEND:20140428T160000 DURATION:PT3H0M0S LOCATION:Maison Jean Kuntzmann SUMMARY:Christian VON ESSEN - Vérification et synthèse quantitative (Quanti tative verification and synthesis) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7900F2UlpT@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20140414T140000 DTEND:20140414T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Kees Goossens - CompSOC: A Mixed-Criticality Platform\, Formalism\, and Design Flow END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-79000g5tpT@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20140403T140000 DTEND:20140403T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Florian Brandner - Refinement of Worst-Case Execution Time Bounds b y Graph Pruning END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-79015UmUR9@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20140403T100000 DTEND:20140403T120000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Jan Reineke - PRET DRAM controller: bank privatization for predicta bility and temporal isolation END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7902bk4Vv4@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:HDR DTSTART:20140313T140000 DTEND:20140313T160000 DURATION:PT2H0M0S LOCATION:Amphi H\, Ensimag SUMMARY:Matthieu Moy - High-level Models for Embedded Systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7902bgmURx@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20140227T140000 DTEND:20140227T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Eugene Asarin - Toward a Timed Theory of Channel Coding END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7903t0bZMs@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20140214T140000 DTEND:20140214T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Franck Cassez - A compositional approach to inter-procedural analy sis END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7904U1PA0V@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20140207T140000 DTEND:20140207T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY: Victor Magron - Formal Certificates for Nonlinear Inequalities END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7904SfPnrA@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20140206T140000 DTEND:20140206T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Najah Ben Said - Information Flow Security in Component-Based Syste ms. END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7905UfXNN9@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20140206T150000 DTEND:20140206T160000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Ali Kassem - Formal Security Analysis for Routing Protocols and E- exams END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7906lh5CK4@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20140130T150000 DTEND:20140130T160000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Abhinav Srivastav - Multi-objective scheduling for multi-core syste ms END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7906bvg7V6@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20140123T140000 DTEND:20140123T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Souha Ben Rayana - Compositional Verification of Component- Based R eal-time Systems and Applications END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7907Mss6MR@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20140123T160000 DTEND:20140123T170000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Alexios Lekidis - Model-based design in sensor network systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7908z00Cu5@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20140123T150000 DTEND:20140123T160000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Alexis Fouilhe - Verifying numerical static analysis results with a proof assistant END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-79084SU1s9@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20140116T160000 DTEND:20140116T170000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Irini-Eleftheria Mens - Learning Regular Languages over Large Alpha bets END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-79092TKdDZ@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20140116T150000 DTEND:20140116T160000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Jan Lanik - Switching reduction in sequential circuits END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7910oCH0fa@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20140116T140000 DTEND:20140116T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Ozgun Pinarer - Estimation of energy consumption of embedded system network END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7910rScJUc@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20140107T140000 DTEND:20140107T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Corneliu Popeea - Automated verification of multi-threaded programs (Automated verification of multi-threaded programs) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-7911O8TXVX@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20131212T133000 DTEND:20131212T153000 DURATION:PT2H0M0S LOCATION:CTL SUMMARY:Yvan Rivierre - Algorithmes auto-stabilisants pour la construction de structures couvrantes réparties (Self-Stabilizing Algorithms for Constr ucting Distributed Spanning Structures) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8086mt2dtC@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20131209T140000 DTEND:20131209T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Giuseppe Lipari - Hierarchical scheduling and component-based analy sis of real-time systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8088eOxFuT@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20131125T113000 DTEND:20131125T123000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Mahfuza Farooque - A Bisimulation between DPLL(T) and a Proof-Searc h Strategy for the Focused Sequent Calculus END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8089pmAdb8@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20131125T140000 DTEND:20131125T170000 DURATION:PT3H0M0S LOCATION:Amphiteatre Maison Jean Kuntzmann SUMMARY:Jannik Dreier - Vérification formelle des protocoles de vote et de vente aux enchères: De l'anonymat à l'équité et la vérifiabilité (Formal V erification of Voting and Auction Protocols: From Privacy to Fairness and Verifiability) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8090icH9vg@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20131031T140000 DTEND:20131031T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Mirko Fiacchini - Set-theory and invariance for complex systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8091cTnWBj@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20130926T140000 DTEND:20130926T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Garnacho Manuel - A Mechanized Semantic Framework for Real-Time Sys tems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8091hK8B9v@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20130916T140000 DTEND:20130916T160000 DURATION:PT2H0M0S LOCATION:CTL SUMMARY:Jean Quilbeuf - Implantations distribuées de modèles à base de com posants communicants par interactions multiparties avec priorités : applic ation au langage BIP. (Distributed Implementations of Component-based Sys tems with Prioritized Multiparty Interactions. Application to the BIP Fram ework.) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8092LdJ63V@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20130718T140000 DTEND:20130718T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Gaël Thomas - A Study of the Scalability of Stop-the-world Garbage Collectors on Multicores END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8093J9n3JN@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20130711T140000 DTEND:20130711T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Sriram Sankaranarayanan - Invariance and Termination for Probabilis tic Programs using Martingales. END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8094hj0v20@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20130710T140000 DTEND:20130710T160000 DURATION:PT2H0M0S LOCATION:CTL SUMMARY:Xiaomu Shi - Certification d'un simulateur de jeu d'instructions (C ertification of an Instruction Set Simulator) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8095V8E4v4@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20130627T140000 DTEND:20130627T151500 DURATION:PT1H15M0S LOCATION:salle A. Pnueli CE3 SUMMARY:Klaus Draeger - Synchronization Invariants END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8095MZSGtN@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:HDR DTSTART:20130619T131500 DTEND:20130619T151500 DURATION:PT2H0M0S LOCATION: salle Remy Lemaire (K223) à l'Institut Néel SUMMARY:Jessy Clédière - Treize années au Centre d'Evaluation de la Sécurit é des Technologies de l'Information du CEA-Grenoble (CESTI-Léti) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8096rTri8M@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20130611T143000 DTEND:20130611T151000 DURATION:PT0H40M0S LOCATION:salle A. Turing CE4 SUMMARY:Christian von Essen - Of Markov Decision Processes and Airborne Col lisions END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8097AtNjsW@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20130530T140000 DTEND:20130530T151500 DURATION:PT1H15M0S LOCATION:salle A. Turing CE4 SUMMARY:Chantal Keller - A Modular Integration of SAT/SMT Solvers to Coq th rough Proof Witnesses END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8097sVSmD3@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20130523T160000 DTEND:20130523T180000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Adam Halasz - Challenges and possible strategies in the modeling of signal initiation by membrane bound receptors END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8098MPT7aR@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20130506T140000 DTEND:20130506T160000 DURATION:PT2H0M0S LOCATION:Amphitéâtre MJK SUMMARY:Emmanuel Sifakis - Programmation efficace et sécurisé d'application s à mémoire partagée (Towards efficient and secure shared memory applicati ons) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8099LjlBB0@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20130426T140000 DTEND:20130426T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Zhoulai Fu - Picking up your targets --- aggressive strong update b eyond common sense END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-81006vnAiI@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20130425T140000 DTEND:20130425T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Deshmukh Jyotirmoy - Mining Temporal Requirements of an Industrial- Scale Control System END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8100IiNNOI@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20130412T140000 DTEND:20130412T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Florent Garnier - Verifying C-Programs memory faults freedom by mea n of Abstract Interpretation and a-posteriori model verification END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-81019g0oeH@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20130409T133000 DTEND:20130409T153000 DURATION:PT2H0M0S LOCATION:CTL Ampitheatre SUMMARY:Paraskevas Bourgos - Flot de conception rigoureux pour la programma tion de plates-formes manycore (Rigorous Design Flow for Programming Manyc ore Platforms) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-81029OWwlV@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20130322T140000 DTEND:20130322T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Karem Sakalla - Saucy3: Fast Symmetry Discovery in Graphs END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8102WcFsT6@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20130319T110000 DTEND:20130319T120000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Sanjit Seshia - Integrating Induction and Deduction for Verificatio n and Synthesis END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-81033vubvo@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20130318T110000 DTEND:20130318T123000 DURATION:PT1H30M0S LOCATION:salle A. Turing CE4 SUMMARY:Rolf Ernst - Mixed critical system design and analysis END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8104gB6eCn@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20130318T140000 DTEND:20130318T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Wang Yi - Scheduling and Analysis of Cyclic Mode-Switches END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8104hkVUva@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20130318T140000 DTEND:20130318T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Wang Yi - Scheduling and Analysis of Cyclic Mode-Switches END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8105PuHKOM@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20130306T140000 DTEND:20130306T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Marc Pouzet - Zélus: A Synchronous Language with ODEs END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8106ftErnX@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20130221T140000 DTEND:20130221T160000 DURATION:PT2H0M0S LOCATION:Amphi 22\, rez-de-chaussée de l'UFR IMAG (bat F) SUMMARY:Valentin Perrelle - Analyse Statique de Programmes Manipulant des T ableaux (Static Analysis of Programs Manipulating Arrays) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8106BWdu81@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20130131T150000 DTEND:20130131T160000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Ahlem Triki - Seminaire doctorant END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8107SkHdUg@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20130131T140000 DTEND:20130131T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Dario Socci - Seminaire doctorant END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8108Rvcl1M@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20130124T153000 DTEND:20130124T163000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Ayoub Nouri - Seminaire doctorant END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8108uGo3pS@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20130124T133000 DTEND:20130124T143000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Julien Henry - Seminaire doctorant END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8109VZ2x8u@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20130124T143000 DTEND:20130124T153000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Raphael Jamet - Seminaire doctorant END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-81109nIfAK@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20130116T140000 DTEND:20130116T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Prabhakar Pavithra - Approximation based Verification of Hybrid Sys tems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8110NnCFSs@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20121207T140000 DTEND:20121207T160000 DURATION:PT2H0M0S LOCATION:CTL SUMMARY:Romain Testylier - Reachability analysis of nonlinear dynamical sys tems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8111BBVUuR@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20121206T150000 DTEND:20121206T160000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Irina Asavoae - Bounded Model Checking of Recursive Programs with P ointers in K Abstract END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8312evNbXu@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20121206T140000 DTEND:20121206T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Mihail Asavoae - Semantics-Based WCET Analysis END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8314lIpZPu@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20121109T140000 DTEND:20121109T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Damien Massé - Inférences de propriétés de terminaison par itératio n de stratégies END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-83152Ugdd2@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:HDR DTSTART:20121106T100000 DTEND:20121106T130000 DURATION:PT3H0M0S LOCATION:Maison Jean Kuntzmann SUMMARY:Pascal Lafourcade - Sécurité assisté par ordinateur pour les primit ives cryptographiques\, les protocoles de vote électroniques et les réseau x de capteurs sans fil (Computer Aided Security for Cryptographic Primitiv es\, Voting protocols\, and Wireless Sensor Networks) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8316U8BeRu@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20121029T140000 DTEND:20121029T160000 DURATION:PT2H0M0S LOCATION:CTL SUMMARY:Jean-François KEMPF - Exploration de l'espace de design assistée pa r ordinateur pour les systèmes multi-coeurs (On Computer-Aided Design-Spac e Exploration for Multi-Cores) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8317F5Djvl@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20121024T140000 DTEND:20121024T170000 DURATION:PT3H0M0S LOCATION:CTL SUMMARY:Selma Saidi - Optimizing DMA Data Transfers for Embedded Multi-Core s END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8317PDN2DX@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20121016T153000 DTEND:20121016T173000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Guillaume Brat - An overview of formal methods for Aeronautics at N ASA END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-83188uMG8k@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20121002T140000 DTEND:20121002T160000 DURATION:PT2H0M0S LOCATION:CTL SUMMARY:Artur Pietrek - TIREX: a textual target-level intermediate represen tation for virtual execution environment\, compiler information exchange and program analysis END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-831923ikNr@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20120914T140000 DTEND:20120915T050000 DURATION:PT15H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Rance Delong - MILS and DMILS project (MILS and DMILS project) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8320KvlZvx@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20120913T140000 DTEND:20120913T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Corneliu Popeea - Synthesizing Software Verifiers from Proof Rules END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8320DmETuL@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20120712T140000 DTEND:20120713T053000 DURATION:PT15H30M0S LOCATION:salle C. Shannon CE4 SUMMARY:Roberto Bruttomesso - Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8321vaVmKT@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20120705T140000 DTEND:20120705T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Pascal Cuoq - Collaboration d\'analyses dans Frama-C END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8322pFZAUT@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20120626T103000 DTEND:20120626T123000 DURATION:PT2H0M0S LOCATION:CTL SUMMARY:Eduardo Mazza - A Formal Framework for Specifying and Analyzing Lia bilities Using Log as Digital Evidence (A Formal Framework for Specifying and Analyzing Liabilities Using Log as Digital Evidence) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8322DjueUU@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20120626T143000 DTEND:20120626T153000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Gerardo Schneider - Towards a Framework for Conflict Analysis of No rmative Texts Written in Controlled Natural Language END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8323eebfg6@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20120621T140000 DTEND:20120621T151500 DURATION:PT1H15M0S LOCATION:salle A. Turing CE4 SUMMARY:Jean-Christophe Filliâtre - Combining Interactive and Automated The orem Proving in Why3 END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8324WVvb8X@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20120607T140000 DTEND:20120607T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Gilles Muller - Remote Core Locking: Migrating Critical-Section Exe cution to Improve the Performance of Multithreaded Applications END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8324pTHSUG@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20120605T140000 DTEND:20120605T160000 DURATION:PT2H0M0S LOCATION:CTL SUMMARY:Tesnim Abdellatif - Rigorous Implementation of Real-time Systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8325De6sBv@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20120601T140000 DTEND:20120601T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Ian Mitchell - Scalable approximation of the viability kernel and s afe control synthesis for LTI systems using maximal reachability END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8326Z3lDZF@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20120531T140000 DTEND:20120531T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Pavol Cerny - Quantitative Abstraction Refinement END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8326V3iH1X@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20120529T150000 DTEND:20120529T170000 DURATION:PT2H0M0S LOCATION:CTL SUMMARY:Rajarshi RAY - Reachability Analysis of Hybrid Systems Using Suppor t Functions END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8327z3Tsui@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20120525T140000 DTEND:20120525T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Johannes Reich - A System Perspective on Processes and Their Intera ctions. END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8327jSTMuG@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20120511T100000 DTEND:20120511T120000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Xavier Urbain - Démonstration automatique : techniques\, outils et certification. END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8328zaSAbE@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20120509T140000 DTEND:20120509T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Pierre Ganty - A Perfect Model for Bounded Verification (A Perfect Model for Bounded Verification) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8329f62VnO@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20120405T140000 DTEND:20120405T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Laura Kovacs - Playing in the Grey Area of Proofs END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8329bUHSgd@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20120322T140000 DTEND:20120322T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Oded Maler - Performance Evaluation of Schedulers in a Probabilisti c Setting END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8330gRZCtH@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20120312T140000 DTEND:20120312T170000 DURATION:PT3H0M0S LOCATION:CTL SUMMARY:Nicolas Berthier - Programmation synchrone de pilotes de périphériq ues pour un contrôle global de ressources dans les systèmes embarqués (Syn chronous Programming of Device Drivers for Global Resource Control in Embe dded Systems) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8331dGIp3v@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20120308T140000 DTEND:20120308T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Goran Frehse - Safety Analysis of Hybrid Systems with SpaceEx END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8331euGeeJ@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20120305T140000 DTEND:20120305T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Sriram Rajamani - Program Analysis and Machine Learning: A Win-Win Deal END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8332jzMfg3@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20120301T140000 DTEND:20120301T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Jerôme Leroux - Vector Addition System Reachability Problem END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8333ZC0JGu@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20120223T140000 DTEND:20120223T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Franck Petit - Strength of Stabilization vs. Amount of Resources END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8333fEUa8t@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20120210T140000 DTEND:20120210T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Laurent George - Robustesse temporelle dans les systèmes embarqués mono et multiprocesseur END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8334ahBTRT@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20120209T140000 DTEND:20120209T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Jan Olaf Blech - Proof Assistant Based Certification for Modeling L anguages and its Application to PLC Development END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8335SoGGKR@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20120126T140000 DTEND:20120126T150000 DURATION:PT1H0M0S LOCATION:CTL SUMMARY:Tom Henzinger - Quantitative Reactive Modeling END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8335siTxxz@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20120119T140000 DTEND:20120119T143000 DURATION:PT0H30M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Christian von Essen - Synthesizing Efficient Controllers END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-83366RcBsb@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20120112T140000 DTEND:20120112T160000 DURATION:PT2H0M0S LOCATION:CTL SUMMARY:Marion DAUBIGNARD - Formalisation de preuves de sécurité concrète ( Formal Methods for Concrete Security Proofs) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8337XX1LR9@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20111118T140000 DTEND:20111118T160000 DURATION:PT2H0M0S LOCATION:Ensimag\, Amphi E SUMMARY:Giovanni Funchal - Contributions à la Modélisation Transactionnelle des Systèmes-sur-Puce (Contributions to Transaction-Level Modeling of Sys tems-on-a-Chip) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-83374rnb7M@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20111114T140000 DTEND:20111114T153000 DURATION:PT1H30M0S LOCATION:Grande Salle de CE4 SUMMARY:Philippe Suter - Sets with Cardinality Constraints in Satisfiabilit y Modulo Theories END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8338pR8ZVm@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20111004T140000 DTEND:20111004T160000 DURATION:PT2H0M0S LOCATION:CTL SUMMARY:Julien Legriel - Optimisation multi-critère et application aux syst èmes multi-processeurs embarqués (Multi-Criteria Optimization and its Appl ication to Multi-Processor Embedded Systems ) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-83392fC71V@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20110915T140000 DTEND:20110915T160000 DURATION:PT2H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Balaji Raman - On Buffering with Stochastic Guarantees in Resource- Constrained Media Players END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-83399UVDmI@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20110721T140000 DTEND:20110721T150000 DURATION:PT1H0M0S LOCATION:CTL SUMMARY:Pierre Ganty - Pattern-based Verification for Multithreaded Program s END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8340jFatiD@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20110630T140000 DTEND:20110630T150000 DURATION:PT1H0M0S LOCATION:CTL SUMMARY:Nathalie Bertrand - Determinizing timed automata. END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8341Vrpsxl@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20110628T140000 DTEND:20110628T160000 DURATION:PT2H0M0S LOCATION:CTL SUMMARY:Francesco Logozzo - Practical program verification for the working programmer with CodeContracts and Abstract Interpretation END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8341VBwArL@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20110621T140000 DTEND:20110621T170000 DURATION:PT3H0M0S LOCATION:Amphi CTL SUMMARY:VASSILIKI SFYRLA - Modélisation des Systèmes Synchrones en BIP (Mod eling Synchronous Systems in BIP) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-83422Iwufg@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20110526T140000 DTEND:20110526T150000 DURATION:PT1H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Jannik Dreier - Privacy Properties for Voting Protocols: The comple ted picture END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8343pmMD2H@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20110519T140000 DTEND:20110519T160000 DURATION:PT2H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Viktor Kuncak - Towards Implicit Programming END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8343B5KffV@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20110518T103000 DTEND:20110518T113000 DURATION:PT1H0M0S LOCATION:CTL - Grande Salle SUMMARY:Jinyun XUE - PAR Method and PAR Platform for Developing Reliable So ftware and Its New Development END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8344ZRWOch@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20110316T153000 DTEND:20110316T163000 DURATION:PT1H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Fabio Somenzi - Clause Manipulation for Faster Satisfiability END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8344vWo2nJ@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20110303T140000 DTEND:20110303T160000 DURATION:PT2H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Hubert Garavel - CADP 2010: A Toolbox for the Construction and Anal ysis of Distributed Processe END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-83456vAwVe@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20110203T140000 DTEND:20110203T160000 DURATION:PT2H0M0S LOCATION:CTL SUMMARY:IMENE BEN HAFAIEDH - Component-based Systems: from Design to Implem entation END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8346NcnvMn@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20110121T103000 DTEND:20110121T123000 DURATION:PT2H0M0S LOCATION:CTL SUMMARY:Sophie Quinton - Design\, verification and implementation of system s of components END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8347URgDlW@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:HDR DTSTART:20101220T140000 DTEND:20101220T160000 DURATION:PT2H0M0S LOCATION:CTL SUMMARY:John Plaice - La programmation Cartésienne (Habilitation à Diriger des Recherches) (Cartesian Programming (HDR defence)) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8347G9OUkZ@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20101118T140000 DTEND:20101118T150000 DURATION:PT1H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Antoine GERBAUD - Le modèle du marcheur pour les réseaux d'interact ions (Walker model for complex networks) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-83481xv5iZ@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20101105T140000 DTEND:20101105T160000 DURATION:PT2H0M0S LOCATION:CTL SUMMARY:Moshe Vardi - From Philosophical to Industrial Logics END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-834973vVjT@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20101028T133000 DTEND:20101028T160000 DURATION:PT2H30M0S LOCATION:CTL SUMMARY:Mohamad Jaber - Centralized and Distributed Implementations of Corr ect-by-construction Component-based Systems by using Source-to-source Tran sformations in BIP END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8349bFu52o@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20100922T150000 DTEND:20100922T173000 DURATION:PT2H30M0S LOCATION:Maison Jean Kuntzmann SUMMARY:Mathias Péron - Contributions à l’analyse statique de programmes ma nipulant des tableaux (Contributions to the Static Analysis of Programs Ha ndling Arrays) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8350rUx6xi@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20100915T140000 DTEND:20100915T170000 DURATION:PT3H0M0S LOCATION:CTL SUMMARY:Tayeb BOUHADIBA - 42\, Une Approche à Composants pour le prototypag e Virtuel des Systèmes Embarqués Hétérogènes (42\, A Component-Based App roach to Virtual Prototyping of Heterogeneous Embedded Systems ) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8350VgInOM@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20100827T100000 DTEND:20100827T120000 DURATION:PT2H0M0S LOCATION:MJK SUMMARY:Manuel Garnacho - Automatisation de la certification formelle de sy stèmes critiques par instrumentation d\\\'interpréteurs abstraits (Automat ic and formal certification of critical systems by instrumentation of abst ract interpreters) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8351factdM@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20100826T190000 DTEND:20100826T200000 DURATION:PT1H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Sébastien Bourdeauducq - Milkymist : un System-on-Chip libre et ori enté video temps réel END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8433SZD65x@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20100708T140000 DTEND:20100708T150000 DURATION:PT1H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Sophie Quinton - Achieving distributed control through model checki ng END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8434lPUuLf@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20100701T140000 DTEND:20100701T160000 DURATION:PT2H0M0S LOCATION:CTL SUMMARY:Jocelyne Troccaz - TBA END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8435PLdRX1@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20100618T100000 DTEND:20100618T120000 DURATION:PT2H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Arshia Cont - Antescofo : A performance-synchronous language for co mputer music END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8435BXXUKx@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20100617T140000 DTEND:20100617T150000 DURATION:PT1H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Karel Heurtefeux - Localisation qualitative appliquée au routage et à l\'accès au canal dans les réseaux de capteurs (Qualitative localizatio n applied to routing and MAC layer in Wireless Sensor Networks) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8436v4vdHU@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20100527T140000 DTEND:20100527T170000 DURATION:PT3H0M0S LOCATION:CTL SUMMARY:Thanh Hung NGUYEN - Vérification Constructive des Systèmes à base d e Composants (Constructive Verification for Component-based Systems) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8437g2Jpdf@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20100510T100000 DTEND:20100510T110000 DURATION:PT1H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Christophe JOUBERT - Datalog-based Program Analysis with BES and RW L END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8438fF0XpB@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20100510T151500 DTEND:20100510T161500 DURATION:PT1H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Arnaud Sangnier - Weak Time Petri Nets Strike back! END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-843848KivC@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20100510T140000 DTEND:20100510T150000 DURATION:PT1H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Nadia El Mrabet - Arithmétique des couplages\, performance et résis tance aux attaques par canaux cachés END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-84395OAPnD@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20100510T163000 DTEND:20100510T173000 DURATION:PT1H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Regis Gascon - (Verification of quantitative properties on constr aint automata ) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8440G2TN8X@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20100507T140000 DTEND:20100507T150000 DURATION:PT1H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Kevin Marquet - Vérification automatique de modèles de systèmes sur puce END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-84403A7ufl@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20100507T151500 DTEND:20100507T161500 DURATION:PT1H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Alexandre DONZE - Conception et analyse basée sur les modèles de sy stèmes hybrides: techniques par simulations\, applications et perspectives (Model-based design and analysis of hybrid systems:simulation-based techn iques\, applications and perspectives) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8441wiN1kU@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20100422T140000 DTEND:20100422T150000 DURATION:PT1H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Nikolay Kosmatov - Le traitement des alias internes dans l'outil de génération de tests PathCrawler (All-Paths Test Generation for Programs w ith Internal Aliases in PathCrawler) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8441mXtuPp@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20100407T133000 DTEND:20100407T160000 DURATION:PT2H30M0S LOCATION:CTL SUMMARY:Mohamed Yassin CHKOURI - Modélisation des systèmes temps-réel embar qués en utilisant AADL pour la génération automatique d’applications forme llement vérifiées (Modelling real-time embedded systems using AADL for the automatic generation of applications formally verified) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8442bIZl7V@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20100401T140000 DTEND:20100401T150000 DURATION:PT1H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Claire Maiza - Static analysis of interferences in the cache memory in preemptive real-time systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8443afE5s0@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20100319T100000 DTEND:20100319T110000 DURATION:PT1H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Nicolas Blanc - Static Analysis for SystemC with Scoot: From Verifi cation to Simulation (Analyse statique de SystemC avec Scoot : de la Verif ication à la Simulation) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8443G6u0iX@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20100309T100000 DTEND:20100309T120000 DURATION:PT2H0M0S LOCATION:CTL SUMMARY:Thomas GAWLITZA - Combining Strategy Iteration with Semidefinite Pr ogramming for Abstract Interpretation END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8444BhEgHc@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20100305T133000 DTEND:20100306T053000 DURATION:PT16H0M0S LOCATION:CTL SUMMARY:Marc Poulhiès - Conception et Implantation de Système Fondé sur les Composants. Vers une Unification des Paradigmes Génie Logiciel et Système . (Design and Implementation of Component Based Systems. Towards a Unifica tion of the Software Engineering and the System Paradigms. ) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8445R6oBu6@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20100304T140000 DTEND:20100304T150000 DURATION:PT1H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Ondrej Sery - Code analysis with Blast END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8445oRWanl@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20100216T140000 DTEND:20100216T150000 DURATION:PT1H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Bahareh Badban - Automated Invariant Generation for the Verificati on of Real-Time Systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8446wMg2gX@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:HDR DTSTART:20100204T133000 DTEND:20100204T163000 DURATION:PT3H0M0S LOCATION:Amphi SUMMARY:Marius Bozga - Component-Based Construction of Real-Time Systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8447t1pJx3@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:HDR DTSTART:20100129T140000 DTEND:20100129T160000 DURATION:PT2H0M0S LOCATION:Amphi F018\, UFR IMA SUMMARY:Dang Thao - Methods and tools for Computer Aided Design of Embedde d Systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8448nl5p6l@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20100114T140000 DTEND:20100114T150000 DURATION:PT1H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Arnaud Sangnier - Reversal-bounded counter machines revisited END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-84486ECvjb@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20091119T160000 DTEND:20091119T170000 DURATION:PT1H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Matthias Althoff - Reachability Analysis of Nonlinear and Hybrid Sy stems with Zonotopes END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8449SnIFnb@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20091119T140000 DTEND:20091119T160000 DURATION:PT2H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Bruce Krogh - Research Directions in Cyber-Physical Systems END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8450D0GXdm@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20091112T110000 DTEND:20091112T114500 DURATION:PT0H45M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Florent Garnier - A classification of randomized fair strategies fo r studying termination of term rewriting (A classification of randomized f air strategies for studying termination of term rewriting) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8450whhB3g@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20091109T140000 DTEND:20091109T170000 DURATION:PT3H0M0S LOCATION:CTL SUMMARY:Yliès Falcone - Etude et mise en oeuvre de méthodes de validation à l'exécution (Study and implementation of runtime validation techniques) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8451EsB8sj@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20091029T140000 DTEND:20091029T160000 DURATION:PT2H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Stephane Demri - Les problèmes de couverture et finitude pour les s ystèmes d'addition de vecteurs arborescents. (The covering and boundednes s problems for branching vector addition\nsystems ) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8452VVsvvk@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20091028T140000 DTEND:20091028T160000 DURATION:PT2H0M0S LOCATION:MJK SUMMARY:Colas Le Guernic - Calcul d'Atteignabilité des Systèmes Hybrides à Partie Continue Linéaire (Reachability Analysis of Hybrid Systems with Lin ear Continuous Dynamics) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8452sFVLNO@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20091021T140000 DTEND:20091021T170000 DURATION:PT3H0M0S LOCATION:Amphithéâtre CTL SUMMARY:Aldric Degorre - Langages formels: quelques aspects quantitatifs (O n Some Quantitative Aspects of Formal Languages) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8453TolXB7@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20090924T140000 DTEND:20090924T150000 DURATION:PT1H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Bageshri KARKARE - Efficiency\, Precision\, Simplicity\, and Gener ality in Interprocedural Data Flow Analysis. END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8454V8afDh@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20090915T140000 DTEND:20090915T150000 DURATION:PT1H0M0S LOCATION:CTL SUMMARY:Dino Distefano - Compositional Shape Analysis by means of Bi-Abduct ion END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8454o2tD66@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20090625T100000 DTEND:20090625T110000 DURATION:PT1H0M0S LOCATION:VERIMAG SUMMARY:Zvonimir Rakamaric - Static and Precise Detection of Concurrency E rrors in Systems Code Using SMT Solvers END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8455pOJAJ4@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Thesis DTSTART:20090625T140000 DTEND:20090625T150000 DURATION:PT1H0M0S LOCATION:Ampithéatre CTL SUMMARY:Scott Cotton - Sur Quelques Problèmes de la Satisfiabilité (On Some Problems in Satisfiability Solving) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8456bUwnZx@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:HDR DTSTART:20090619T101500 DTEND:20090619T131500 DURATION:PT3H0M0S LOCATION:CTL SUMMARY:David Monniaux - Analyse statique : de la théorie à la pratique (St atic analysis: from theory to practice) END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8456Hu7Cz8@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20090514T140000 DTEND:20090514T150000 DURATION:PT1H0M0S LOCATION:CTL SUMMARY:Florian Kammueller - ASPfun: un calcul pour des objets distribués END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8457IiPmpj@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20090507T140000 DTEND:20090507T150000 DURATION:PT1H0M0S LOCATION:VERIMAG SUMMARY:Villard Jules - Proving Copyless Message Passing END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8458OSzncB@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20090416T140000 DTEND:20090416T150000 DURATION:PT1H0M0S LOCATION:VERIMAG/AMPHI CTL SUMMARY:Christophe Guillon - Les représentations SSA et Psi-SSA END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8458ibMsV4@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20090409T140000 DTEND:20090409T150000 DURATION:PT1H0M0S LOCATION:VERIMAG SUMMARY:Alexandre Donzé - Calcul numérique d'ensembles atteignables pour les systèmes hybrides et applications END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8459z700Gu@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20090402T140000 DTEND:20090402T150000 DURATION:PT1H0M0S LOCATION:VERIMAG SUMMARY:Domagoj Babic - Scalable and Precise Extended Static Checking END:VEVENT BEGIN:VEVENT UID:20260720T014631UTC-8459tmOttu@129.88.40.24 DTSTAMP:20260720T014631Z CATEGORIES:Veri_sem DTSTART:20090305T140000 DTEND:20090305T150000 DURATION:PT1H0M0S LOCATION:VERIMAG SUMMARY:Thomas Gawlitza - Precise Relational Invariants Through Strateg y Iteration END:VEVENT END:VCALENDAR