BEGIN:VCALENDAR CALSCALE:GREGORIAN METHOD:PUBLISH PRODID:-//129.88.40.24//NONSGML iCalcreator 2.6// VERSION:2.0 SUMMARY:Evènements Verimag X-WR-CALNAME:Evènements Verimag X-WR-CALDESC:Liste des évènements (séminaires\, thèses\, ...) au labora toire Verimag. X-WR-TIMEZONE:Europe/Paris BEGIN:VEVENT UID:20260307T013644CET-0501kvTuBb@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20260319T140000 DTEND:20260319T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Youssouf Oualhadj - Rational Synthesis in Resource-Constrained Mult i-Agent Systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0505jA7pe7@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20260122T140000 DTEND:20260122T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Joseph Sifakis - Bringing AI to Autonomous Systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0508VCTBus@129.88.40.24 DTSTAMP:20260307T003644Z 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:20260307T013644CET-0511UBrUI9@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20251218T140000 DTEND:20251218T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Jérémie Decouchant - Defending TEE-aided Blockchain Consensus aga inst Rollback Attacks END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0514i7eiEp@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20251211T140000 DTEND:20251211T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Thaïs Baudon - Compiling types and other high-level language featu res for performance or security END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0516cAStRm@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20251204T140000 DTEND:20251204T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Jannik LAVAL - Jumeaux Numériques : Les sciences du logiciel au c œur de la transformation industrielle (Digital Twins: software engineerin g at the heart of industrial transformation) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0519UH66Gf@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20251201T140000 DTEND:20251201T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Sylvain BOULME - Introduction à la programmation orientée objet e n Crystal END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-05220jzMRa@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20251125T140000 DTEND:20251125T150000 DURATION:PT01H0M0S LOCATION:Room 106 (1st floor\, badged access) SUMMARY:Véronique Cortier - Electronic voting: design\, attack\, and forma l verification END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0525ngNsoE@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20251121T140000 DTEND:20251121T170000 DURATION:PT03H0M0S 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:20260307T013644CET-0528BBH9jh@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20251113T150000 DTEND:20251113T170000 DURATION:PT02H0M0S 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:20260307T013644CET-0530cG7vg9@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20251016T143000 DTEND:20251016T163000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Nicolas Chappe - Representing and reasoning about nondeterministic programs END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0533H99LLj@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20251009T140000 DTEND:20251009T150000 DURATION:PT01H0M0S LOCATION:BBB SUMMARY:Tiago Cogumbreiro - Verifying GPU programs with Memory Access Proto cols END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-053642AiHD@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20251003T100000 DTEND:20251003T120000 DURATION:PT02H0M0S 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:20260307T013644CET-0539V077ux@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20250626T140000 DTEND:20250626T150000 DURATION:PT01H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Nikolaus Huber - Mimosa: A Language Design for Modern Embedded Syst ems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-05416a2sWF@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20250613T100000 DTEND:20250613T110000 DURATION:PT01H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Selma Saidi - Connected Minds: Leveraging Collective Reasoning for Autonomous Systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0544dPuVmd@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20250612T140000 DTEND:20250612T150000 DURATION:PT01H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Maher Mallem - Parameterized complexity of scheduling problems with precedence delays END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0546BNg5kE@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20250605T140000 DTEND:20250605T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Sébastien Michelland - Secure compilation—with the compiler\, no t against: first experiments on 'Tracing LLVM' END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0548EJUiC9@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20250417T140000 DTEND:20250417T150000 DURATION:PT01H0M0S LOCATION:Zoom UGA 959 9591 1882 -- Passcode: 063113 SUMMARY:Riadh ROBBANA - Le Vote Électronique Sécurisé à l’Ère de la Blockchain : Contexte\, Défis et Solutions Innovantes END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0551VvNph5@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20250411T150000 DTEND:20250411T190000 DURATION:PT04H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Hadi Dayekh - L'apprentissage passif et actif des systèmes dynamiq ues non linéaires commutés (Passive and Active Learning of Switched Nonl inear Dynamical Systems) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0554AawdXP@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20250327T140000 DTEND:20250327T160000 DURATION:PT02H0M0S LOCATION:Zoom (Meeting ID: 986 9236 8072\; Passcode: 923483) SUMMARY:Youssouf Oualhadj - Robust timed synthesis END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0556V326Os@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20250313T140000 DTEND:20250313T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Thomas Carle - MINOTAuR: a timing-predictable RiscV (CVA6) core END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0559eiUrii@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20250306T140000 DTEND:20250306T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Yannick Chevalier - Logique et Cybersécurité END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-05619kAnkt@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20250123T140000 DTEND:20250123T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0564CPdh2v@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20241212T150000 DTEND:20241212T190000 DURATION:PT04H0M0S 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:20260307T013644CET-0566nVUW3S@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20241212T140000 DTEND:20241212T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0568HLS92L@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20241202T140000 DTEND:20241202T160000 DURATION:PT02H0M0S LOCATION:Amphitéatre MJK SUMMARY:Thomas Vigouroux - Analyses quantitatives pour les attaquants adapt atifs (Quantitative analysis for adaptive attackers) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0571RMKeUI@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20241128T140000 DTEND:20241128T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Grégoire BUSSONE - Réduire les copies et l'utilisation mémoire d ans les langages synchrones (Reducing copies and memory consumption in syn chronous languages) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0573u9FPV1@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20241120T140000 DTEND:20241120T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Chao Huang - Safe Reinforcement Learning with Verification in the L oss END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0576nDMImu@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20241114T140000 DTEND:20241114T160000 DURATION:PT02H0M0S 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:20260307T013644CET-05789UaomS@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20241107T140000 DTEND:20241107T150000 DURATION:PT01H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Aurèle Barrière - Formal Verification Beyond Traditional Compilat ion END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0581DCK9oV@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20240627T140000 DTEND:20240627T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0583A2sUmW@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20240619T093000 DTEND:20240619T113000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Jean-François MONIN - Recent advances on the Braga method END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0586jw7hUb@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20240618T093000 DTEND:20240618T113000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Matthieu Sozeau - Verified Extraction from Coq to OCaml END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0588mtjReu@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20240617T160000 DTEND:20240617T180000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Basile GROS - Small Inversions in Coq END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0590fBVWTC@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20240617T140000 DTEND:20240617T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0593FIiKxZ@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20240530T140000 DTEND:20240530T160000 DURATION:PT02H0M0S 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:20260307T013644CET-059632R1Eo@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20240516T140000 DTEND:20240516T150000 DURATION:PT01H0M0S LOCATION:BBB SUMMARY:Gaiyun Liu - Modeling\, analysis\, and supervisory control of netwo rked discrete event systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0598xvGTwN@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20240502T130000 DTEND:20240502T150000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Matthieu Moy - How to Build a Broken System? END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0602vT9VpE@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20240418T140000 DTEND:20240418T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Akram Idani - Formal Model-Driven Engineering END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0605fu8K4e@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20240415T140000 DTEND:20240415T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0607vj0HWf@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20240411T143000 DTEND:20240411T163000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Andrei Paskevich - Coma: an intermediate verification language with explicit abstraction barriers END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0609wIrXUS@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20240404T133000 DTEND:20240404T153000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Sébastien Michelland - Abstract Interpreters: a Monadic Approach t o Modular Verification END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0612xVAiza@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20240314T131500 DTEND:20240314T151500 DURATION:PT02H0M0S 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:20260307T013644CET-0615upbkMW@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20240313T103000 DTEND:20240313T123000 DURATION:PT02H0M0S 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:20260307T013644CET-0618c09pOl@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20240307T143000 DTEND:20240307T163000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Sylvain Boulmé - Développement logiciel formellement vérifié: p ourquoi et comment ? END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-06213hPOhL@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20240222T140000 DTEND:20240222T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0623Mhj4kz@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20240212T100000 DTEND:20240212T130000 DURATION:PT03H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Aina Rasoldier - Comment évaluer le potentiel d'une solution num érique face à l'urgence écologique ? Application aux plateformes de cov oiturage régulier à l'échelle locale END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0626GJh3pS@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20240208T140000 DTEND:20240208T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0629T9LD4i@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20231214T140000 DTEND:20231214T150000 DURATION:PT01H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Alessandro De Palma - From Neural Network Verification to Efficient Robust Training END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0631jjxndU@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20231212T093000 DTEND:20231212T113000 DURATION:PT02H0M0S LOCATION:Seminar Room 2\, ground floor (Building IMAG) SUMMARY:Leo Gourdin - Validation Formelle de Transformations Intra-Procédu rales par Simulation Symbolique Défensive (Formal Validation of Intra-Pro cedural Transformations by Defensive Symbolic Simulation) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0634UUuv1a@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20231130T140000 DTEND:20231130T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Yutaka Nagashima - AI-Enhanced Theorem Proving: Tactical Approaches for Induction Problems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0637fO7pHN@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20231117T143000 DTEND:20231117T163000 DURATION:PT02H0M0S 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:20260307T013644CET-06394JiVTu@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20231109T140000 DTEND:20231109T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Gidon Ernst - Automating software verification with respect to stro ng specifications END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0642AOw8fj@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20231019T140000 DTEND:20231019T160000 DURATION:PT02H0M0S LOCATION:zoom SUMMARY:Michael Foster - Active Inference of Extended Finite State Machines Without Reset END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0645io5uuL@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20231012T140000 DTEND:20231012T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Nicola Gigante - Temporal Logics Modulo Theories for Infinite-State Verification END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0647ntEWar@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20230712T140000 DTEND:20230712T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Dejan Nickovic - Attribute Repair for Threat Prevention END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0649dkRemi@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20230707T100000 DTEND:20230707T120000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Akshay Mambakam - Parametric timed formalisms for specification and monitoring (PhD defense) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0652ZI5cke@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20230706T140000 DTEND:20230706T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Nicola Paoletti - Causal Temporal Reasoning for Markov Decision Pro cesses END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0654Vhra9j@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20230630T140000 DTEND:20230630T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0657fi24kG@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:HDR DTSTART:20230609T150000 DTEND:20230609T170000 DURATION:PT02H0M0S LOCATION:Auditorium\, ground floor (Building IMAG) SUMMARY:claire maiza - Analyses matérielles et logicielles pour obtenir un e analyse temporelle précise et efficace (Hardware and software analyses for precise and efficient timing analysis) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0659avIz0b@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20230609T100000 DTEND:20230609T110000 DURATION:PT01H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Jean-Luc Scharbarg - Trends in real-time embedded networks: towards TSN END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0662a1EU2R@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20230608T140000 DTEND:20230608T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0664UERPMi@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20230525T140000 DTEND:20230525T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0667JiEUmS@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20230504T140000 DTEND:20230504T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Joseph Sifakis - Artificial Intelligence and autonomous systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0669lpMmeR@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20230428T110000 DTEND:20230428T120000 DURATION:PT01H0M0S 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:20260307T013644CET-0672E5Ulum@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20230428T140000 DTEND:20230428T170000 DURATION:PT03H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Etienne Boespflug - Outils pour l’analyse de code et de contre-me sures pour l'injection de fautes multiples END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0674fwUOEt@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20230309T140000 DTEND:20230309T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0676c2oNSa@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20230306T100000 DTEND:20230306T110000 DURATION:PT01H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Frederic Fort - Programing adaptive real-time systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0679EUwATH@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20230302T140000 DTEND:20230302T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Arthur Perais - Exploring Instruction Fusion Opportunities in Gener al Purpose Processors END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0682FSj83c@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20230223T110000 DTEND:20230223T130000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Léo Robert - How fast do you heal? A taxonomy for post-compromise security in secure-channel establishment. END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0685vRk60o@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20230223T153000 DTEND:20230223T173000 DURATION:PT02H0M0S 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:20260307T013644CET-0687DJcNSA@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20230220T140000 DTEND:20230220T160000 DURATION:PT02H0M0S 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:20260307T013644CET-06900C2Rtj@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20230206T140000 DTEND:20230206T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0692vNU1gF@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20230202T140000 DTEND:20230202T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0694aVFMvM@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20230126T140000 DTEND:20230126T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Son Ho - Aeneas: Rust Verification by Functional Translation END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0696Rw0zHm@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20221216T100000 DTEND:20221216T123000 DURATION:PT02H30M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Vincent Morice - Modèle haut niveau de microcontrôleurs basé su r les dépendances pour le développement de logiciel embarqué END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0699UXFKOv@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20221213T140000 DTEND:20221213T150000 DURATION:PT01H0M0S 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:20260307T013644CET-07014CVj1k@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20221208T140000 DTEND:20221208T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0704OxI3Us@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20221124T140000 DTEND:20221124T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Xavier Denis - Deductive Verification of Higher-Order Rust Programs END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0707w2n2Wx@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20221124T100000 DTEND:20221124T113000 DURATION:PT01H30M0S LOCATION:Room 285 (badged access\, limited occupancy) SUMMARY:Jean-François Monin - Programmation récursive en Coq et intension alité : oh le beau cas ! (Recursive Programming in Coq and Intensionality : oh happy case !) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0709IcZivI@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20221117T140000 DTEND:20221117T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Arnaud Sangnier - Parameterized verification of Networks with selec tive broadcast END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0712ftE6G4@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20221110T140000 DTEND:20221110T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Stephan Plassart - Equivalent Versions of Total Flow Analysis END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0714h3E9RJ@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20221027T140000 DTEND:20221027T150000 DURATION:PT01H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Hugo Gimbert - Les algorithmes de ParcourSup END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0717Jl8P2o@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20220929T140000 DTEND:20220929T150000 DURATION:PT01H0M0S 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:20260307T013644CET-0719WNEcWM@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20220909T140000 DTEND:20220909T150000 DURATION:PT01H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Lucas Bueri - On an Invariance Problem for Parameterized Concurrent Systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0723o5euJh@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20220712T140000 DTEND:20220712T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Dejan Nickovic - Information-flow Interfaces END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0726kfTJrv@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20220707T140000 DTEND:20220707T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Franz Meyer - Towards Efficient Active Learning of PDFA END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0728VaoLrt@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20220621T140000 DTEND:20220621T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Joel Goossens - Real-Time Computing\, Multiprocessor scheduling pro blems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0730HurorD@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20220616T140000 DTEND:20220616T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0733IwrouC@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20220614T140000 DTEND:20220614T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Joel Goossens - Real-Time Computing\, foundation END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0735wKGbBz@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20220603T090000 DTEND:20220603T150000 DURATION:PT06H0M0S 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:20260307T013644CET-0737FZAhPu@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20220531T093000 DTEND:20220531T113000 DURATION:PT02H0M0S 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:20260307T013644CET-0740EthLvV@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20220505T100000 DTEND:20220505T120000 DURATION:PT02H0M0S 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:20260307T013644CET-0742EUbrH5@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20220407T100000 DTEND:20220407T120000 DURATION:PT02H0M0S 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:20260307T013644CET-0744jrvbTr@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20220324T140000 DTEND:20220324T150000 DURATION:PT01H0M0S 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:20260307T013644CET-0746aHevxU@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20220310T140000 DTEND:20220310T150000 DURATION:PT01H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Paolo Torrini - A CompCert Backend with Symbolic Encryption END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0749rt2DuK@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20220303T143000 DTEND:20220303T163000 DURATION:PT02H0M0S LOCATION:Zoom link SUMMARY:Xiaowei Huang - Machine Learning Safety END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0752UHiFrG@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20220113T140000 DTEND:20220113T160000 DURATION:PT02H0M0S LOCATION:Room 206 SUMMARY:Benjamin BLANC - Formal Methods in Practice: Model Checking in the Railway Industry END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0755D7XuXc@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20211213T140000 DTEND:20211213T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0758zfU8JA@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20211207T140000 DTEND:20211207T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0762ifZJRX@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20211203T100000 DTEND:20211203T120000 DURATION:PT02H0M0S LOCATION:https://veri-bbb.imag.fr/b/rad-ofn-9t8-rqc SUMMARY:Miriam Garci­a - Design\, Verification and Synthesis of Hybrid Sy stems. END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-07655mHRtu@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20211202T140000 DTEND:20211202T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0767KuDuzL@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20211129T140000 DTEND:20211129T160000 DURATION:PT02H0M0S LOCATION:Vidéo SUMMARY:Nicolas Basset - Uniform Sampling for Networks of Automata END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0769NxMtOi@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20211123T140000 DTEND:20211123T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:PIERRE-LEO BEGAY - Conception\, développement et certification dan s Coq/MathComp d'optimisations Datalog pour la vérification réseau (Desi gn\, Development and certification in Coq/MathComp of Datalog optimization s for network verification) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-07723BeIDt@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20211004T140000 DTEND:20211004T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0774mnhJnu@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:HDR DTSTART:20210927T150000 DTEND:20210927T170000 DURATION:PT02H0M0S LOCATION:Video SUMMARY:Sylvain Boulmé - Formally Verified Defensive Programming (efficien t Coq-verified computations from untrusted ML oracles) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0776GD96sP@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20210920T140000 DTEND:20210920T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0778ssU5Ka@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20210830T140000 DTEND:20210830T150000 DURATION:PT01H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Yannick Zakowski - Sémantique de Vellvm (Vellvm semantics) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0781KXoK8v@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20210713T150000 DTEND:20210713T170000 DURATION:PT02H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Cyril Six - Compilation optimisante et formellement prouvée pour un processeur VLIW (Optimized and formally-verified compilation for a VLIW processor) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0783vUVxdT@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20210617T140000 DTEND:20210617T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0785LTVJDI@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20210610T150000 DTEND:20210610T170000 DURATION:PT02H0M0S LOCATION:Room 206 et BBB (code d'accès 506793) SUMMARY:Jean-François Monin - [FormalProofs] Petites inversion et récursi on débridée en Coq\, la méthode de Braga ([FormalProofs] Small inversio ns and unleashed recursion in Coq\, the Braga method) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0788mb5UPP@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20210423T090000 DTEND:20210423T110000 DURATION:PT02H0M0S LOCATION:Zoom SUMMARY:Schoitsch Erwin - Ethical aspects and recommendations for trustwor thy highly automated/autonomous systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0790LMUZpD@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20210401T140000 DTEND:20210401T160000 DURATION:PT02H0M0S LOCATION:BBB room access code 349356 SUMMARY:Lionel Rieg - [FormalProofs] A formally-verified compiler from Este rel to circuits END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0793g19ADp@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20210311T140000 DTEND:20210311T150000 DURATION:PT01H0M0S 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:20260307T013644CET-0795pGP2WF@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20210226T100000 DTEND:20210226T110000 DURATION:PT01H0M0S LOCATION:Visioconference SUMMARY:Emma AHRENS - Local Reasoning for Reconfigurable Distributed System s END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0798j7vzPU@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20210225T140000 DTEND:20210225T160000 DURATION:PT02H0M0S LOCATION:BBB : Room access code 756979 SUMMARY:Cyril SIX - Certified Superblock Scheduling for the CompCert Compil er END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0801SjKHPE@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20210211T140000 DTEND:20210211T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0803uAUX6a@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20210128T140000 DTEND:20210128T160000 DURATION:PT02H0M0S LOCATION:https://veri-bbb.imag.fr/b/rad-ofn-9t8-rqc SUMMARY:Etienne André - Symbolic Monitoring against Specifications Paramet ric in Time and Data END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0806cacbDS@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20210121T140000 DTEND:20210121T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0808nNvjt7@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20210114T140000 DTEND:20210114T160000 DURATION:PT02H0M0S LOCATION:https://veri-bbb.imag.fr/b/mic-1x2-b8m-ama SUMMARY:Olivier RIDOUX - Limite de Landauer et calcul réversible : une int roduction (Landauer limit and reversible calculus: an introduction) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0810jsLzXf@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20201218T100000 DTEND:20201218T120000 DURATION:PT02H0M0S LOCATION:By zoom (details below) SUMMARY:Guo Xiaojie - Certified Tools for Schedulability Analyses END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0813abfsHu@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:HDR DTSTART:20201217T130000 DTEND:20201217T150000 DURATION:PT02H0M0S 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:20260307T013644CET-0815XUuc3a@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20201211T103000 DTEND:20201211T123000 DURATION:PT02H0M0S LOCATION:virtual seminar SUMMARY:Marius Bozga - Compositional Generation of Invariants for Timed Sys tems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-08188UscVp@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20201203T151500 DTEND:20201203T164500 DURATION:PT01H30M0S 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:20260307T013644CET-082026Bv0W@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20201120T103000 DTEND:20201120T123000 DURATION:PT02H0M0S 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:20260307T013644CET-08231o6DvR@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20201119T160000 DTEND:20201119T171500 DURATION:PT01H15M0S LOCATION:Séminaire virtuel via BigBlueButton SUMMARY:Aina Rasoldier - Les méthodologies d'évaluation des impacts envir onnementaux des technologies de l'information et de la communication (TIC) à l'échelle mondiale END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0826rnr82V@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20201117T140000 DTEND:20201117T160000 DURATION:PT02H0M0S 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:20260307T013644CET-08280a3gVs@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20201106T103000 DTEND:20201106T120000 DURATION:PT01H30M0S LOCATION:Virtual seminar (the link will be sent later) SUMMARY:Akshay Mambakam - Learning Specifications for Labelled Patterns END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0830koSrJn@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20201022T141500 DTEND:20201022T151500 DURATION:PT01H0M0S 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:20260307T013644CET-0833AUpe4D@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20200630T140000 DTEND:20200630T150000 DURATION:PT01H0M0S LOCATION:Online : https://veri-bbb.imag.fr/b/pie-zc2-ji9 SUMMARY:Sébastien Michelland - Une Procédure de Décision pour les Relati ons d'Équivalence (A Decision Procedure for Equivalence Relations) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0835ImJIHk@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20200312T140000 DTEND:20200312T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0838Ihxs9L@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20200309T153000 DTEND:20200309T173000 DURATION:PT02H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Rémy Boutonnet - Modular Analysis of Numerical Properties by Abstr act Interpretation END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0840SkC72j@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20200221T103000 DTEND:20200221T113000 DURATION:PT01H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Michael Marcozzi - Compiler Fuzzing: How Much Does It Matter? END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0843UXziAH@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20200213T103000 DTEND:20200213T123000 DURATION:PT02H0M0S 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:20260307T013644CET-0846gv9V40@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20200212T140000 DTEND:20200212T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Sébastien Bardin - From Safety to Security: The Case of Binary-le vel Code Analysis END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0850KBbOUN@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20200206T140000 DTEND:20200206T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0852hIuCjb@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20200203T110000 DTEND:20200203T120000 DURATION:PT01H0M0S 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:20260307T013644CET-0854URJlrk@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20200127T103000 DTEND:20200127T113000 DURATION:PT01H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Margus Veanes - Symbolic Regexes & Matching END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0857Mr6V3A@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20200127T140000 DTEND:20200127T180000 DURATION:PT04H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Xiao XU - Thesis Defence - Xiao XU - Generalisation of Alternating Automata over Infinite Alphabets END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0860huSAKw@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20191219T100000 DTEND:20191219T130000 DURATION:PT03H0M0S LOCATION:Seminar Room\, ground floor (Building IMAG) SUMMARY:Hang Yu - Towards an Efficient Parallel Parametric Linear Programmi ng Solver END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0862gC8buz@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20191219T140000 DTEND:20191219T150000 DURATION:PT01H0M0S 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:20260307T013644CET-0865VEvn8K@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20191125T140000 DTEND:20191125T160000 DURATION:PT02H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Moshe Vardi - Technology is Driving the Future\, But Who Is Steerin g? END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0867HkD9a9@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20191121T140000 DTEND:20191121T153000 DURATION:PT01H30M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Sophie Tourret - Stronger Higher-order Automation END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0869weeU2n@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20191010T150000 DTEND:20191010T160000 DURATION:PT01H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Jan Reineke - Spectector: Principled detection of speculative infor mation flows END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0872App7zU@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20191008T160000 DTEND:20191008T180000 DURATION:PT02H0M0S 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:20260307T013644CET-0874zRVVPN@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190926T140000 DTEND:20190926T153000 DURATION:PT01H30M0S 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:20260307T013644CET-08779vZF5Z@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190920T090000 DTEND:20190920T110000 DURATION:PT02H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:-- Oded Maler Memorial Day - Oded Maler Memorial Day END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0880zuNXdL@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190919T140000 DTEND:20190919T153000 DURATION:PT01H30M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Martin Franzle - What’s to Come is Still Unsure: Automatically Sy nthesizing and Verifying Controllers Resilient to Delayed Interaction END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0882JVGgnJ@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190711T140000 DTEND:20190711T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0885pZ20Gu@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190709T140000 DTEND:20190709T150000 DURATION:PT01H0M0S 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:20260307T013644CET-0887LgaUOW@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190704T140000 DTEND:20190704T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Radu IOSIF - Alternating Automata Modulo First Order Theories END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0890tlt5m8@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190702T140000 DTEND:20190702T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Indranil Saha - Developing Autonomous Multi-Robot Systems for Comp lex Missions END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0892axf3xH@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20190628T140000 DTEND:20190628T180000 DURATION:PT04H0M0S 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:20260307T013644CET-0895l0PWWV@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20190626T140000 DTEND:20190626T160000 DURATION:PT02H0M0S LOCATION:Seminar Room Part 1\, ground floor (Building IMAG) SUMMARY:Rany Kahil - Schedulability in Mixed- criticality Systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0897dchIF5@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190625T140000 DTEND:20190625T160000 DURATION:PT02H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Hernan Ponce de Leon - BMC with Weak Memory Models END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0900bdRUai@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190614T140000 DTEND:20190614T160000 DURATION:PT02H0M0S 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:20260307T013644CET-09028NPZed@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190613T140000 DTEND:20190613T150000 DURATION:PT01H0M0S 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:20260307T013644CET-0904oVhMP6@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190509T140000 DTEND:20190509T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Saddek Bensalem - Engineering Trustworthy Learning-Enabled Autono mous Systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0906d1lTMf@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190502T140000 DTEND:20190502T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Michael PERIN - Découvrir AMC en 45 Questions a Choix Multiples END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0909lSHUnF@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190429T094500 DTEND:20190429T154500 DURATION:PT06H0M0S LOCATION:Seminar Room\, ground floor (Building IMAG) SUMMARY:Invited Speakers - Journée thématique Verimag : Many-core Kalray MPPA\, implementation and verification END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0911SZ8CLw@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190405T140000 DTEND:20190405T160000 DURATION:PT02H0M0S 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:20260307T013644CET-09149DL979@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190404T140000 DTEND:20190404T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Radu IOSIF - Checking Deadlock-Freedom of Parametric Component-Base d Systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0917U4ZUs7@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190401T100000 DTEND:20190401T120000 DURATION:PT02H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Edward A. Lee - Living Digital Beings END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-09194wELm1@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190328T140000 DTEND:20190328T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Olivier VIDAL - Matières premières et énergie à l’échelle mo ndiale dans le contexte de la transition énergétique END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-09220Aj4eH@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20190320T140000 DTEND:20190320T160000 DURATION:PT02H0M0S LOCATION:Rim El Ballouli SUMMARY:Rim El Ballouli - Modeling Self-configuration in Architecture-based Self-adaptive systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0924IR69pu@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190308T100000 DTEND:20190308T110000 DURATION:PT01H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Mathias Bourgoin - An overview of the Tezos blockchain END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0927MSP4vw@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20190222T133000 DTEND:20190222T163000 DURATION:PT03H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Moustapha Lo - Implementing a Real-time Avionic application on a Ma nycore Processor END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-09295cUgVE@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190218T140000 DTEND:20190218T160000 DURATION:PT02H0M0S LOCATION:IMAG Auditorium SUMMARY:Guillaume Baudart - Probabilistic Reactive Programming (Probabilist ic Reactive Programming) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0932dLIxVd@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190214T140000 DTEND:20190214T160000 DURATION:PT02H0M0S LOCATION:Auditorium (ground floor) SUMMARY:Nikos Gorogiannis - Concurrency bug detection at scale with Infer END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-09351UhE0f@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190207T140000 DTEND:20190207T150000 DURATION:PT01H0M0S 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:20260307T013644CET-0937LvwnUl@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190125T140000 DTEND:20190125T160000 DURATION:PT02H0M0S 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:20260307T013644CET-09403O5f5d@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190124T140000 DTEND:20190124T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Maiza Claire - WCET and interference analysis for multicore sy stems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0942deFiRs@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190122T140000 DTEND:20190122T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Georg Struth - Verifying Hybrid Systems with Modal Kleene Algebra END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-09452jvrgu@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190121T140000 DTEND:20190121T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0947uO77LP@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190118T140000 DTEND:20190118T150000 DURATION:PT01H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Chi-Hong Cheng - When neural networks meet dependability END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-09490voJi8@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190117T140000 DTEND:20190117T153000 DURATION:PT01H30M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Paolo Torrini - Reifying and translating a monadic fragment of Gall ina END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0952WoRZKT@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190108T140000 DTEND:20190108T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0955oDExcP@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20190107T140000 DTEND:20190107T160000 DURATION:PT02H0M0S 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:20260307T013644CET-0958wORbzv@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20181219T140000 DTEND:20181219T160000 DURATION:PT02H0M0S 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:20260307T013644CET-09619WLbT7@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20181217T140000 DTEND:20181217T160000 DURATION:PT02H0M0S LOCATION:Seminar Room 2\, ground floor (Building IMAG) SUMMARY:NIKOLAOS KEKATOS - Vérification formelle des systèmes cyber-physi ques dans le processus industriel de la conception basée sur modèle (For mal Verification of Cyber-Physical Systems in the Industrial Model-Based D esign Process) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0964ElMFot@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20181211T140000 DTEND:20181211T150000 DURATION:PT01H0M0S 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:20260307T013644CET-09660WMVO0@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20181206T140000 DTEND:20181206T153000 DURATION:PT01H30M0S 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:20260307T013644CET-09680rf9Vh@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20181129T140000 DTEND:20181129T160000 DURATION:PT02H0M0S LOCATION:Room 206 (2nd floor\, badged access) SUMMARY:Sylvain Boulmé - Importation d'oracles ML impératifs dans du code Coq vérifié END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0971SBzOJm@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20181122T100000 DTEND:20181122T163000 DURATION:PT06H30M0S 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:20260307T013644CET-0974MdGPIu@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20181116T103000 DTEND:20181116T123000 DURATION:PT02H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Amaury Graillat - Parallel Code Generation of Synchronous Programs for a Many-core Architecture END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0977b7FFof@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20181031T140000 DTEND:20181031T170000 DURATION:PT03H0M0S LOCATION:Auditorium (Building IMAG) SUMMARY:Mahieddine DELLABANI - Formal Methods for Distributed Real-Time Sys tems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0979HlOagr@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20181023T140000 DTEND:20181023T150000 DURATION:PT01H0M0S 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:20260307T013644CET-0982ZrNd37@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20181011T140000 DTEND:20181011T160000 DURATION:PT02H0M0S LOCATION:Amphi D1\, DLST SUMMARY:Florent Chevrou - Formalisation of Asynchronous Interactions END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0984BEpSbb@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20181004T153000 DTEND:20181004T173000 DURATION:PT02H0M0S 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:20260307T013644CET-0986E3X70W@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20180920T140000 DTEND:20180920T153000 DURATION:PT01H30M0S LOCATION:Salle 206 SUMMARY:Cyril Six - Compilateur CompCert certifié pour processeur VLIW Kal ray (Extending the CompCert certified compiler for a VLIW processor of Kal ray) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-09898j9bxx@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20180913T140000 DTEND:20180913T150000 DURATION:PT01H0M0S LOCATION:Salle 206 (salle Chamois) SUMMARY:Franz Mayr - Regular inference on artificial neural networks END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0991odEGvA@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20180625T100000 DTEND:20180625T120000 DURATION:PT02H0M0S LOCATION:Room 206 SUMMARY:Stefano Berardi - Martin-Lof's Inductive Definitions Are Not Equiva lent to Cyclic Proofs END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0994e9VF1L@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20180622T110000 DTEND:20180622T120000 DURATION:PT01H0M0S 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:20260307T013644CET-0996BZvo5I@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20180531T140000 DTEND:20180531T160000 DURATION:PT02H0M0S LOCATION:Auditorium (IMAG) SUMMARY:Cristina Serban - Raisonnement automatisé pour la Logique de Sépa ration avec des définitions inductives (Automated Reasoning in Separation Logic with Inductive Definitions) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-0999EfGmkv@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20180517T140000 DTEND:20180517T150000 DURATION:PT01H0M0S LOCATION:salle 206 SUMMARY:Michael PERIN - Automatic Grading: take a CEGAR and let the machine do your work END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1002CdlMnI@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20180516T140000 DTEND:20180516T160000 DURATION:PT02H0M0S LOCATION:Auditorium (IMAG) SUMMARY:Arvind Adimoolam - A Calculus of Complex Zonotopes for Computing In variants of Affine Hybrid Systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1005rgkJAn@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20180515T140000 DTEND:20180515T160000 DURATION:PT02H0M0S 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:20260307T013644CET-1007uJxjXF@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20180507T133000 DTEND:20180507T170000 DURATION:PT03H30M0S LOCATION:Auditorium (IMAG) SUMMARY:Alexandre Rocca - Méthodes formelles pour la modélisation et la v alidation de modèles biologiques (Formal methods for modelling and valida tion of biological models) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1009CxOh8g@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20180417T110000 DTEND:20180417T120000 DURATION:PT01H0M0S LOCATION:Meeting room 206 (IMAG) SUMMARY:Jim Kapinski - Verification of Learning-Enabled\, Cyber-Physical Sy stems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-10124UI13D@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20180412T140000 DTEND:20180412T150000 DURATION:PT01H0M0S LOCATION:IMAG 206 SUMMARY:Maria Méndez Real - Cache-based attacks and spatial isolation coun termeasure on multi and many-core architectures END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1014EXEN7C@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20180322T160000 DTEND:20180322T170000 DURATION:PT01H0M0S LOCATION:206 SUMMARY:Guilhem Jaber - Model-checking contextual equivalence of higher-ord er programs with references (candidat poste MCF) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1016dUmwvb@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20180322T150000 DTEND:20180322T160000 DURATION:PT01H0M0S 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:20260307T013644CET-1019ObWcF0@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20180319T140000 DTEND:20180319T150000 DURATION:PT01H0M0S LOCATION:salle 206 SUMMARY:Benjamin Farinier - Model Generation for Quantified Formulas: A Tai nt-Based Approach END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1022eAvBM0@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20180315T140000 DTEND:20180315T150000 DURATION:PT01H0M0S LOCATION:206 SUMMARY:Lionel Rieg - Extending a verified OS kernel for real-time END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1024polr5x@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20180315T150000 DTEND:20180315T160000 DURATION:PT01H0M0S 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:20260307T013644CET-1027sJC9Kv@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20180308T140000 DTEND:20180308T160000 DURATION:PT02H0M0S LOCATION:206 SUMMARY:Ivan Gazeau - Automated verification of privacy-type properties fo r security protocols (MCF Candidate) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1030v2Tvtn@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20180215T140000 DTEND:20180215T160000 DURATION:PT02H0M0S LOCATION:Room 204 SUMMARY:Gheorghe Stefanescu - Adaptive systems made by self-assembling hete rogeneous components within regular 2D patterns END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1033R6dKUP@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20180205T103000 DTEND:20180205T123000 DURATION:PT02H0M0S LOCATION:Auditorium (IMAG) SUMMARY:Maxime Puys - Sécurité des systèmes industriels : filtrage appli catif et recherche de scénarios d’attaques (Cybersecurity of Industrial Systems: Applicative Filtering and Generation of Attack Scenarios) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1035Ls77U4@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20180118T140000 DTEND:20180118T150000 DURATION:PT01H0M0S LOCATION:ENSIMAG Amphi E SUMMARY:David Monniaux - SPECTRE + MELTDOWN END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-10380b4m6L@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20180115T140000 DTEND:20180115T170000 DURATION:PT03H0M0S LOCATION:Seminar Room\, ground floor (Building IMAG) SUMMARY:Dogan Ulus - Filtrage par Motif Temporisé: Théorie et Application s (Pattern Matching with Time: Theory and Applications) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1041ZcHXaV@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20171221T140000 DTEND:20171221T150000 DURATION:PT01H0M0S LOCATION:206 SUMMARY:Mirco Giacobbe - Counterexample-guided Refinement of Template Polyh edra END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1044PF17zw@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20171211T140000 DTEND:20171211T160000 DURATION:PT02H0M0S LOCATION:Auditorium (IMAG) SUMMARY:Alexandre Maréchal - New Algorithmics for Polyhedral Calculus via Parametric Linear Programming END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1046mOcVea@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20171211T140000 DTEND:20171211T170000 DURATION:PT03H0M0S LOCATION:Seminar Room\, ground floor (Building IMAG) SUMMARY:Denis Becker - Simulation SystemC/TLM Parallèle de Composants Mat ériels Décrits pour la Synthèse de Haut Niveau (Parallel SystemC/TLM Si mulation of Hardware Components Described for High-Level Synthesis) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1049sMUMKl@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20171207T140000 DTEND:20171207T160000 DURATION:PT02H0M0S LOCATION:Seminar Room\, ground floor (Building IMAG) SUMMARY:De Oliviera Steven - Synthesizing Invariants by Solving Solvable L oops END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1052gVAduF@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20171201T150000 DTEND:20171201T160000 DURATION:PT01H0M0S LOCATION:Salle 206 IMAG SUMMARY:Reineke Jan - On the Smoothness of Paging Algorithms END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1054VVXz1e@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20171201T100000 DTEND:20171201T120000 DURATION:PT02H0M0S LOCATION:Amphi H\, Ensimag SUMMARY:Hamza RIHANI - Analyse temporelle des systèmes temps-réels sur ar chitectures pluri-cœurs avec application à un processeur industriel (Man y-Core Timing Analysis of Real-Time Systems and its Application to an Indu strial Processor) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-10578i4nPC@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20171123T140000 DTEND:20171123T160000 DURATION:PT02H0M0S LOCATION:Salle de séminaire (rez-de-chaussée) SUMMARY:Joseph Sifakis - How Much Hard is System Design? END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1060pVgUod@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20171020T101500 DTEND:20171020T121500 DURATION:PT02H0M0S LOCATION:Ensimag Amphi H SUMMARY:Franck De Goer - Rétro-ingénierie de programmes binaires en une e xécution - une analyse dynamique légère basée au niveau des fonctions (Reverse Engineering binary code in one execution - A lightweight function based dynamic execution.) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1063VEzSIo@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20171019T103000 DTEND:20171019T170000 DURATION:PT06H30M0S LOCATION:Seminar Room 2\, ground floor (Building IMAG) SUMMARY: - COQ en STOCK END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1066GdnfNA@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20171010T140000 DTEND:20171010T160000 DURATION:PT02H0M0S LOCATION:Auditorium (IMAG) SUMMARY:Irini Eleftheria Mens - Learning Regular Languages over Large Alpha bets END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1068AFcXlF@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20171010T103000 DTEND:20171010T123000 DURATION:PT02H0M0S LOCATION:Seminar Room 1\, ground floor (Building IMAG) SUMMARY:Frits Vaandrager - Learning Mealy Machines with Timers END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1071jzAcl5@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20170928T140000 DTEND:20170928T150000 DURATION:PT01H0M0S LOCATION:206 SUMMARY:Adrien Guatto - A Functional Language with Time Warps END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1074wdoCHH@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20170914T140000 DTEND:20170914T160000 DURATION:PT02H0M0S LOCATION:Room 106\, 1st floor SUMMARY:Joël Goossens - Feasibility & Simulation Intervals of Schedules fo r Recurrent Real-Time Tasks END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1076RndoxP@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20170901T093000 DTEND:20170901T113000 DURATION:PT02H0M0S LOCATION:Auditorium (IMAG) SUMMARY:Anaïs Durand - Algorithmes distribués efficaces adaptés à un co ntexte incertain (Efficient Distributed Algorithms Suited for Uncertain Co ntext) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1078OEPffc@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20170831T101500 DTEND:20170831T170000 DURATION:PT06H45M0S LOCATION:Seminar Room\, ground floor (Building IMAG) SUMMARY: - Workshop ESTATE/VERIMAG 'Distributed Algorithms' END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1081MamrPH@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20170712T140000 DTEND:20170712T160000 DURATION:PT02H0M0S 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:20260307T013644CET-1084boUkJ0@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20170626T140000 DTEND:20170626T160000 DURATION:PT02H0M0S LOCATION:Auditorium (IMAG) SUMMARY:Hosein Nazarpour - Surveillance de systèmes à composants multi-th reads et distribués (Monitoring Multi-Threaded and Distributed (Component -Based) Systems) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1086fdjuVk@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20170608T140000 DTEND:20170608T160000 DURATION:PT02H0M0S 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:20260307T013644CET-1088wtrSvJ@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20170606T140000 DTEND:20170606T160000 DURATION:PT02H0M0S LOCATION:Amphi E Ensimag 681\, rue de la passerelle - Campus SUMMARY:Laurent Lemke - Modèles partagés et infrastructure ouverte pour l ’internet des objets de la ville intelligente END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1091X5pVwV@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20170510T090000 DTEND:20170510T110000 DURATION:PT02H0M0S LOCATION:Auditorium (IMAG) SUMMARY:Yuliia Romenska - Composants abstraits pour la vérification foncti onnelle des systèmes sur puce (High-Level Component-Based Models for Func tional Verification of Systems-on-a-Chip) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1094UFsRVG@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20170420T140000 DTEND:20170420T160000 DURATION:PT02H0M0S 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:20260307T013644CET-1096oSm4i5@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20170419T140000 DTEND:20170419T153000 DURATION:PT01H30M0S 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:20260307T013644CET-1099F6OgmM@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20170411T110000 DTEND:20170411T123000 DURATION:PT01H30M0S LOCATION:206 SUMMARY:Iulia Dragomir - Compositional Design and Analysis of Embedded Syst ems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1101cvjWHL@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20170330T140000 DTEND:20170330T150000 DURATION:PT01H0M0S LOCATION:IMAG 206 SUMMARY:Helmut Seidl - Enforcing Termination of Interprocedural Analysis END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1104W4k3RO@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20170330T100000 DTEND:20170330T120000 DURATION:PT02H0M0S LOCATION:IMAG 206 SUMMARY:Dirk Beyer - Correctness Witnesses: Exchanging Verification Results between Verifiers END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1106sOzzOO@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20170329T140000 DTEND:20170329T170000 DURATION:PT03H0M0S LOCATION:Auditorium (IMAG) SUMMARY:Egor Karpenkov - Finding Inductive Invariants using SMT Solving and Convex Optimization END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-11098rO3z1@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20170329T103000 DTEND:20170329T123000 DURATION:PT02H0M0S 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:20260307T013644CET-1111R30bJE@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20170328T140000 DTEND:20170328T150000 DURATION:PT01H0M0S LOCATION:IMAG 206 SUMMARY:Nikolaj Bjorner - Network Verification for Microsoft Azure END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1114Lmwn7P@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20170323T140000 DTEND:20170323T153000 DURATION:PT01H30M0S 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:20260307T013644CET-1116GPrk92@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20170323T153000 DTEND:20170323T163000 DURATION:PT01H0M0S LOCATION:206 SUMMARY:Romaric Ludinard - Bitcoin\, la blockchain et le problème de la do uble dépense : état des lieux et analyse de propositions d'amélioration s (Bitcoin\, its blockchain and the double spending problem : Bitcoin in a nutshell and safety analysis of recent improvement proposals) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1118HliW8C@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20170316T150000 DTEND:20170316T160000 DURATION:PT01H0M0S LOCATION:206 SUMMARY:Manuel Selva - Exécution efficace sur machine multi-cœur (Efficie nt execution on multi-core systems) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-11216FWpOd@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20170309T153000 DTEND:20170309T163000 DURATION:PT01H0M0S LOCATION:206 SUMMARY:Lionel Rieg - Formal Proofs of Safety in Coq: Mobile Robot Networks and Lustre Compilation END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1124uELCwN@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20170309T140000 DTEND:20170309T150000 DURATION:PT01H0M0S LOCATION:206 SUMMARY:Arthur Milchior - Deterministic Automaton and logically definable sets of numbers. END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-11270t5EDb@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20170302T164500 DTEND:20170302T181500 DURATION:PT01H30M0S LOCATION:206 SUMMARY:Paulin Fournier - Verification of infinite probabilistic systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1129A6mxo7@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20170302T153000 DTEND:20170302T163000 DURATION:PT01H0M0S LOCATION:206 SUMMARY:Nicolas Basset - Uniform Sampling for Timed Automata with Applicati on to Language Inclusion Measurement END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1132V9iVNV@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20170302T140000 DTEND:20170302T160000 DURATION:PT02H0M0S LOCATION:Seminar Room 1\, ground floor (Building IMAG) SUMMARY:Loïc Correnson - « De Frama-C à Lustre » (« From Frama-C to Lu stre ») END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1135f4Gsn2@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20170216T100000 DTEND:20170216T110000 DURATION:PT01H0M0S LOCATION:Seminar Room\, ground floor (Building IMAG) SUMMARY:Naor Seffi - Multi-label Classification with Pairwise Relations END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-11374cuPCu@129.88.40.24 DTSTAMP:20260307T003644Z 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:20260307T013644CET-1140xSZwns@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20170216T110000 DTEND:20170216T120000 DURATION:PT01H0M0S 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:20260307T013644CET-1142u4K1Hu@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20170209T140000 DTEND:20170209T170000 DURATION:PT03H0M0S LOCATION:Salle 206 SUMMARY: - Second Year PhD Students Seminars - week 2/2 END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1145IVR4Sw@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20170202T140000 DTEND:20170202T162000 DURATION:PT02H20M0S LOCATION:Seminar Room\, ground floor (Building IMAG) SUMMARY: - Second Year PhD Students Seminars - week 1/2 END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1148z56zT9@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20161205T170000 DTEND:20161205T183000 DURATION:PT01H30M0S LOCATION:Auditorium (IMAG) SUMMARY:Paul FEAUTRIER - New Architectures\, New Compilation Problems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1150BueHjN@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20161117T143000 DTEND:20161117T153000 DURATION:PT01H0M0S LOCATION:Salle 106 SUMMARY:Robin David - Formal Approaches for Automatic Deobfuscation and Rev erse-engineering of Protected Codes END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1153bR46u6@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20161107T140000 DTEND:20161107T160000 DURATION:PT02H0M0S 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 (Informatio n Flow Security in Component Based Models: From Verification to Implementa tion) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1155zCMvTu@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20161104T140000 DTEND:20161104T170000 DURATION:PT03H0M0S LOCATION:Souha Ben Rayana SUMMARY:Souha Ben Rayana - Vérification compositionnelle des systèmes tem ps-réels à base de compsants et applications. (Compositional Verificatio n of Component-Based Real-time Systems and Applications.) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-11579uZvxu@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20161102T140000 DTEND:20161102T150000 DURATION:PT01H0M0S LOCATION:ROOM 206 SUMMARY:Nikos Gorogiannis - Biabduction (and Related Problems) in Array Sep aration Logic END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1160Vse4SL@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20161028T100000 DTEND:20161028T120000 DURATION:PT02H0M0S LOCATION:VERIMAG (Room 206\, 2nd floor) SUMMARY:J. Esparza\, A. Bouajjani\, and D. Nickovic - Verification: Theory and Practice END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1164HHGVZz@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20161028T150000 DTEND:20161028T170000 DURATION:PT02H0M0S LOCATION:Seminar Room\, ground floor (Building IMAG) SUMMARY:Thomas FERRERE - Assertion and Measurements for Mixed-Signal Simula tion END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-11664igjc2@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20161027T140000 DTEND:20161027T160000 DURATION:PT02H0M0S LOCATION:Auditorium (IMAG) SUMMARY:Joseph Sifakis - Modeling architectures and their properties in BIP END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1169KmI53z@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20161013T161500 DTEND:20161013T171500 DURATION:PT01H0M0S LOCATION:206 SUMMARY:Ismail Oukid - Storage Class Memory (aka NVRAM): Challenges and Opp ortunities END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1171kmu4Ox@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20161012T100000 DTEND:20161012T120000 DURATION:PT02H0M0S LOCATION:Auditorium (IMAG) SUMMARY:Louis Dureuil - Analyse de code et processus d’évaluation des co mposants sécurisés contre l’injection de faute END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1174U9sGzV@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20161006T153000 DTEND:20161006T163000 DURATION:PT01H0M0S LOCATION:Room 206 (building IMAG) SUMMARY:Cristina SERBAN - A Decision Procedure for Separation Logic in SMT END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1176U8oahg@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20160929T113000 DTEND:20160929T123000 DURATION:PT01H0M0S LOCATION:Auditorium (Builbing IMAG) SUMMARY:Parosh Abdulla - Automatic Verification of Linearization Policies END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1179BV3vId@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20160929T103000 DTEND:20160929T113000 DURATION:PT01H0M0S LOCATION:Auditorium (Builbing IMAG) SUMMARY:Joel Ouaknine - Decision Problems for Linear Dynamical Systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-11827zaK9r@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20160929T093000 DTEND:20160929T103000 DURATION:PT01H0M0S LOCATION:Auditorium (Builbing IMAG) SUMMARY:Andreas Podelski - Thread Modularity on the Next Level END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1184ZsiKBS@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:HDR DTSTART:20160929T140000 DTEND:20160929T170000 DURATION:PT03H0M0S LOCATION:Auditorium (Builbing IMAG) SUMMARY:Radu Iosif - Automata and Logics for Program Verification END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1187O5Pvwf@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20160705T100000 DTEND:20160705T120000 DURATION:PT02H0M0S LOCATION:IMAG building\, Room 206 SUMMARY:Jyo Deshmukh - Recent progress on formal methods for CPS END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-118903j4PV@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20160705T140000 DTEND:20160705T160000 DURATION:PT02H0M0S LOCATION:Auditorium IMAG SUMMARY:Rahul Mangaram - Challenges with Medical Cyber-Physical Systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1192oihS24@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20160630T140000 DTEND:20160630T150000 DURATION:PT01H0M0S LOCATION:206 SUMMARY:Sergiy Bogomolov - Scalable Static Hybridization Methods for Analys is of Nonlinear Systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1194sh4sL5@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20160622T140000 DTEND:20160622T160000 DURATION:PT02H0M0S LOCATION:New IMAG building Auditorium SUMMARY:Heiko FALK - WCET-Aware Compilation and Optimization for Real-Time Systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1197vMXxAG@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20160616T140000 DTEND:20160616T160000 DURATION:PT02H0M0S LOCATION:Auditorium du Bât IMAG SUMMARY:Jan Lanik - Power reduction in sequential circuits END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1199UluUbF@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:HDR DTSTART:20160526T170000 DTEND:20160526T190000 DURATION:PT02H0M0S LOCATION:amphithéâtre\, bâtiment IMAG de l'Univ. G SUMMARY:Frehse Goran - Scalable Verification of Hybrid Systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1202NVbZZh@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20160512T140000 DTEND:20160512T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Bruno Grenet - Factorisation de polynômes lacunaires END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-12048ULGVp@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20160428T140000 DTEND:20160428T150000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Camille Coti - Parallel\, distributed behavioral cartography of par ametric timed automata END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1207p8SKO3@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20160324T140000 DTEND:20160324T150000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Amaury Pouly - Solvability of Matrix-Exponential Equations END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1209tVb2Dp@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20160309T090000 DTEND:20160309T100000 DURATION:PT01H0M0S LOCATION:Maison Jean Kuntzmann (MJK) SUMMARY:Alan Burns - Mixed Criticality - A Personal View END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-12126HmUx6@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20160309T100000 DTEND:20160309T110000 DURATION:PT01H0M0S LOCATION:Maison Jean Kuntzmann (MJK) SUMMARY:Sanjoy Baruah - Mixed-criticality Scheduling on Multiprocessors END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-12141T4gOb@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20160309T110000 DTEND:20160309T120000 DURATION:PT01H0M0S LOCATION:Maison Jean Kuntzmann (MJK) SUMMARY:Luca Santinelli - Mixed-Criticalities and Probabilities END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1217VTwUHi@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20160309T140000 DTEND:20160309T160000 DURATION:PT02H0M0S LOCATION:Maison Jean Kuntzmann (MJK) SUMMARY:Dario Socci - Scheduling of Certifiable Mixed-Criticality Systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1220AvU17E@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20160302T140000 DTEND:20160302T150000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Alexey Bakhirkin - Towards finding non-terminating behaviours in p rograms END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1222BXpGi7@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20160301T140000 DTEND:20160301T150000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Arnaud Sangnier - On the Complexity of Verifying Regular Properties on Flat Counter Systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-12250NsVo1@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20160204T140000 DTEND:20160204T170000 DURATION:PT03H0M0S LOCATION:salle A. Turing CE4 SUMMARY: - PhD Seminars END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1227xGezn3@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20160129T100000 DTEND:20160129T120000 DURATION:PT02H0M0S LOCATION:CTL SUMMARY:Mathilde Duclos - Méthodes pour la vérification des protocoles cr yptographiques dans le modèle calculatoire (Methods for cryptographic pro tocol verification in the computational model ) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-123007ohUh@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20160128T140000 DTEND:20160128T170000 DURATION:PT03H0M0S LOCATION:salle A. Turing CE4 SUMMARY: - PhD Seminars END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-12322sv1Xb@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20160107T140000 DTEND:20160107T170000 DURATION:PT03H0M0S LOCATION:salle A. Turing CE4 SUMMARY: - Phd Seminars END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-12343Z7WOG@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20151210T133000 DTEND:20151210T153000 DURATION:PT02H0M0S LOCATION:CTL SUMMARY:Alexios Lekidis - Design flow for the rigorous development of netwo rked embedded systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1237ekg2eC@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20151210T100000 DTEND:20151210T120000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:PEKTAŞ Abdurrahman - Behavior based malware classification using o nline machine learning END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1239rUnk8h@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20151016T093000 DTEND:20151016T103000 DURATION:PT01H0M0S 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:20260307T013644CET-1242skTeAr@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20151015T100000 DTEND:20151015T110000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Andy King - The Ying and the Yang of Binary Reversing END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1245AvOLdG@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20151015T140000 DTEND:20151015T160000 DURATION:PT02H0M0S LOCATION:CTL SUMMARY:Alexis Fouilhe - Revisiting the abstract domain of polyhedra: const raints-only representation and formal proof END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1247OEr9rO@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20151014T140000 DTEND:20151014T150000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Chantal Keller - F*: Higher-Order Effectful Program Verification END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1249Isf5Pb@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20150918T100000 DTEND:20150918T120000 DURATION:PT02H0M0S LOCATION:Amphiteatre Maison Jean Kuntzmann SUMMARY:Ali Kassem - Vérification automatique de protocoles d'examen\, de monnaie\, de réputation\, et de routage (Automated Verification of Exam\, Cash\, Reputation\, and Routing Protocols) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1252mvVu40@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20150910T140000 DTEND:20150910T160000 DURATION:PT02H0M0S 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:20260307T013644CET-1255gHWnif@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20150903T140000 DTEND:20150903T150000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Amaury Pouly - On the complexity of some continuous space reachabil ity problems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-12573kU5LB@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20150702T140000 DTEND:20150702T160000 DURATION:PT02H0M0S LOCATION:Amphi E ENSIMAG SUMMARY:Christos H. Papadimitriou - Life under the Lens END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1259INvbZO@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20150625T140000 DTEND:20150625T150000 DURATION:PT01H0M0S 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:20260307T013644CET-1261XLHD6P@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20150611T140000 DTEND:20150611T150000 DURATION:PT01H0M0S 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:20260307T013644CET-1264At2HzU@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20150609T133000 DTEND:20150609T153000 DURATION:PT02H0M0S LOCATION:MJK SUMMARY:Ahlem TRIKI - Distributed Implementations of Timed Component-based Systems (Implémentations Distributés des Systems Temps-réel à base de Composants) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1266kWW4uU@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20150528T140000 DTEND:20150528T150000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Andrew Reynolds - Using CVC4 for Proofs by Induction in SMT END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1269EVxdtv@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20150408T133000 DTEND:20150408T163000 DURATION:PT03H0M0S LOCATION:CTL (Amphitheater) SUMMARY:Ayoub Nouri - Rigorous System-level Modeling and Performance Evalua tion for Embedded System Design END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-127195L19c@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20150403T140000 DTEND:20150403T150000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Damien Pous - Algorithms for language equivalence of finite automat a END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-127396DLLP@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20150219T140000 DTEND:20150219T170000 DURATION:PT03H0M0S LOCATION:salle A. Turing CE4 SUMMARY: Seminaires doctorants 3 - Verimag PhD seminars 3 END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1276lm6P3i@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20150212T140000 DTEND:20150212T170000 DURATION:PT03H0M0S LOCATION:salle A. Turing CE4 SUMMARY: Seminaires doctorants 2 - Verimag PhD seminars 2 END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1278Xmzx1V@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20150205T140000 DTEND:20150205T163000 DURATION:PT02H30M0S LOCATION:salle A. Turing CE4 SUMMARY: Seminaires doctorants 1 - Verimag PhD seminars 1 END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1281HV0uux@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20150129T140000 DTEND:20150129T160000 DURATION:PT02H0M0S 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:20260307T013644CET-12844epVws@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20150115T140000 DTEND:20150115T160000 DURATION:PT02H0M0S 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:20260307T013644CET-1286xDtUC6@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20141210T140000 DTEND:20141210T150000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Cristina Serban - An Introduction to Separation Logic END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1289Kiz9PV@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20141121T140000 DTEND:20141121T150000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Chih-Hong Cheng - G4LTL-ST - Automatic Generation of PLC programs END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1292pLovSS@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20141113T133000 DTEND:20141113T153000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Victor Magron - New applications of moment-SOS hierarchies END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1294zuo4Mz@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20141107T140000 DTEND:20141107T160000 DURATION:PT02H0M0S 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:20260307T013644CET-1297GORDcM@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20141015T140000 DTEND:20141015T150000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Andreas Podelski - Proof Spaces for Unbounded Parallelism END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1299oBRB8v@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20141014T140000 DTEND:20141014T150000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Andreas Podelski - Static Analysis Modulo Theory END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-13016V9xLu@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20141013T153000 DTEND:20141013T173000 DURATION:PT02H0M0S LOCATION:Amphithéâtre - Maison Jean Kuntzmann SUMMARY:Julien Henry - Analyse statique de programmes par interprétation a bstraite et procédures de décision (Static Analysis by Abstract Interpre tation and Decision Procedures) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1304hst6JJ@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20141013T133000 DTEND:20141013T153000 DURATION:PT02H0M0S 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:20260307T013644CET-1306A4VM0V@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20141009T103000 DTEND:20141009T123000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Kim Quyên Lý - Verification automatique de certificats de termina ison (Automated verification of termination certificates) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1308KxzVTJ@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20141003T140000 DTEND:20141003T170000 DURATION:PT03H0M0S LOCATION:Maison Jean Kuntzmann SUMMARY:Raphaël Jamet - Protocoles et Modèles pour la Sécurité des Rés eaux Ad Hoc Sans-Fil (Protocols and Models for the Security of Wireless Ad Hoc Networks) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1311pK3WOk@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20140912T140000 DTEND:20140912T160000 DURATION:PT02H0M0S 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:20260307T013644CET-1313FPCirW@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20140528T140000 DTEND:20140528T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Dejan Nickovic - Require\, Test and Trace It END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1316DOUlhS@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20140428T130000 DTEND:20140428T160000 DURATION:PT03H0M0S LOCATION:Maison Jean Kuntzmann SUMMARY:Christian VON ESSEN - Vérification et synthèse quantitative (Quan titative verification and synthesis) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1318jsB64A@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20140414T140000 DTEND:20140414T150000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Kees Goossens - CompSOC: A Mixed-Criticality Platform\, Formalism\, and Design Flow END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1321cl8PEw@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20140403T140000 DTEND:20140403T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Florian Brandner - Refinement of Worst-Case Execution Time Bounds b y Graph Pruning END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-13237rumJh@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20140403T100000 DTEND:20140403T120000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Jan Reineke - PRET DRAM controller: bank privatization for predicta bility and temporal isolation END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1325vWs51s@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:HDR DTSTART:20140313T140000 DTEND:20140313T160000 DURATION:PT02H0M0S LOCATION:Amphi H\, Ensimag SUMMARY:Matthieu Moy - High-level Models for Embedded Systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1328UtVANX@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20140227T140000 DTEND:20140227T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Eugene Asarin - Toward a Timed Theory of Channel Coding END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1331gGTlle@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20140214T140000 DTEND:20140214T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Franck Cassez - A compositional approach to inter-procedural analy sis END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1333V8ANlm@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20140207T140000 DTEND:20140207T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY: Victor Magron - Formal Certificates for Nonlinear Inequalitie s END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1336WRSkDu@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20140206T150000 DTEND:20140206T160000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Ali Kassem - Formal Security Analysis for Routing Protocols and E- exams END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1338aOv2pS@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20140206T140000 DTEND:20140206T150000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Najah Ben Said - Information Flow Security in Component-Based Syste ms. END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1340IARNHV@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20140130T150000 DTEND:20140130T160000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Abhinav Srivastav - Multi-objective scheduling for multi-core syste ms END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1342C7ejK0@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20140123T160000 DTEND:20140123T170000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Alexios Lekidis - Model-based design in sensor network systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1345Kvje0K@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20140123T150000 DTEND:20140123T160000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Alexis Fouilhe - Verifying numerical static analysis results with a proof assistant END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1347snPKj3@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20140123T140000 DTEND:20140123T150000 DURATION:PT01H0M0S 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:20260307T013644CET-1349v38Ixa@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20140116T150000 DTEND:20140116T160000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Jan Lanik - Switching reduction in sequential circuits END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1352UPOU0F@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20140116T160000 DTEND:20140116T170000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Irini-Eleftheria Mens - Learning Regular Languages over Large Alpha bets END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-13553RIzkd@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20140116T140000 DTEND:20140116T150000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Ozgun Pinarer - Estimation of energy consumption of embedded system network END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1357kVUaMv@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20140107T140000 DTEND:20140107T160000 DURATION:PT02H0M0S 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:20260307T013644CET-1359sBlHrp@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20131212T133000 DTEND:20131212T153000 DURATION:PT02H0M0S LOCATION:CTL SUMMARY:Yvan Rivierre - Algorithmes auto-stabilisants pour la construction de structures couvrantes réparties (Self-Stabilizing Algorithms for Const ructing Distributed Spanning Structures) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1363WRuu6K@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20131209T140000 DTEND:20131209T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Giuseppe Lipari - Hierarchical scheduling and component-based analy sis of real-time systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1365iUFGK5@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20131125T113000 DTEND:20131125T123000 DURATION:PT01H0M0S 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:20260307T013644CET-1368pZcFu0@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20131125T140000 DTEND:20131125T170000 DURATION:PT03H0M0S 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é (F ormal Verification of Voting and Auction Protocols: From Privacy to Fairne ss and Verifiability) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1370PvLMOB@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20131031T140000 DTEND:20131031T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Mirko Fiacchini - Set-theory and invariance for complex systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1372bm7388@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20130926T140000 DTEND:20130926T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Garnacho Manuel - A Mechanized Semantic Framework for Real-Time Sys tems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1374p6uZWS@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20130916T140000 DTEND:20130916T160000 DURATION:PT02H0M0S LOCATION:CTL SUMMARY:Jean Quilbeuf - Implantations distribuées de modèles à base de composants communicants par interactions multiparties avec priorités : ap plication au langage BIP. (Distributed Implementations of Component-based Systems with Prioritized Multiparty Interactions. Application to the BIP Framework.) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1377VvukRX@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20130718T140000 DTEND:20130718T160000 DURATION:PT02H0M0S 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:20260307T013644CET-1379wvJuTc@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20130711T140000 DTEND:20130711T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Sriram Sankaranarayanan - Invariance and Termination for Probabilis tic Programs using Martingales. END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1381gKcdpj@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20130710T140000 DTEND:20130710T160000 DURATION:PT02H0M0S 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:20260307T013644CET-1384sxFvDz@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20130627T140000 DTEND:20130627T151500 DURATION:PT01H15M0S LOCATION:salle A. Pnueli CE3 SUMMARY:Klaus Draeger - Synchronization Invariants END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1386i5pUvC@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:HDR DTSTART:20130619T131500 DTEND:20130619T151500 DURATION:PT02H0M0S LOCATION: salle Remy Lemaire (K223) à l'Institut Néel SUMMARY:Jessy Clédière - Treize années au Centre d'Evaluation de la Séc urité des Technologies de l'Information du CEA-Grenoble (CESTI-Léti) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1388BimU2u@129.88.40.24 DTSTAMP:20260307T003644Z 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:20260307T013644CET-13915ViAeB@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20130530T140000 DTEND:20130530T151500 DURATION:PT01H15M0S 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:20260307T013644CET-13938On0gg@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20130523T160000 DTEND:20130523T180000 DURATION:PT02H0M0S 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:20260307T013644CET-13964Njznc@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20130506T140000 DTEND:20130506T160000 DURATION:PT02H0M0S LOCATION:Amphitéâtre MJK SUMMARY:Emmanuel Sifakis - Programmation efficace et sécurisé d'applicati ons à mémoire partagée (Towards efficient and secure shared memory appl ications) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1398uavbvv@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20130426T140000 DTEND:20130426T150000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Zhoulai Fu - Picking up your targets --- aggressive strong update b eyond common sense END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1400NnJKjS@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20130425T140000 DTEND:20130425T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Deshmukh Jyotirmoy - Mining Temporal Requirements of an Industrial- Scale Control System END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1403wAgJbT@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20130412T140000 DTEND:20130412T160000 DURATION:PT02H0M0S 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:20260307T013644CET-1406lMfWMr@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20130409T133000 DTEND:20130409T153000 DURATION:PT02H0M0S 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:20260307T013644CET-1408HH8uOO@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20130322T140000 DTEND:20130322T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Karem Sakalla - Saucy3: Fast Symmetry Discovery in Graphs END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1410rcPp7u@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20130319T110000 DTEND:20130319T120000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Sanjit Seshia - Integrating Induction and Deduction for Verificatio n and Synthesis END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1413rilXKH@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20130318T140000 DTEND:20130318T150000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Wang Yi - Scheduling and Analysis of Cyclic Mode-Switches END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1415Rv9mjo@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20130318T110000 DTEND:20130318T123000 DURATION:PT01H30M0S LOCATION:salle A. Turing CE4 SUMMARY:Rolf Ernst - Mixed critical system design and analysis END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1418Z0bBh2@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20130318T140000 DTEND:20130318T150000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Wang Yi - Scheduling and Analysis of Cyclic Mode-Switches END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1420uhnHVd@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20130306T140000 DTEND:20130306T150000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Marc Pouzet - Zélus: A Synchronous Language with ODEs END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-14223ImaFg@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20130221T140000 DTEND:20130221T160000 DURATION:PT02H0M0S 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:20260307T013644CET-1424SPNELV@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20130131T150000 DTEND:20130131T160000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Ahlem Triki - Seminaire doctorant END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1427xhumA3@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20130131T140000 DTEND:20130131T150000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Dario Socci - Seminaire doctorant END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1429IxbvOI@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20130124T153000 DTEND:20130124T163000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Ayoub Nouri - Seminaire doctorant END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1431zh5vUN@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20130124T133000 DTEND:20130124T143000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Julien Henry - Seminaire doctorant END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1434wGvnMw@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20130124T143000 DTEND:20130124T153000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Raphael Jamet - Seminaire doctorant END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1436WTvrzz@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20130116T140000 DTEND:20130116T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Prabhakar Pavithra - Approximation based Verification of Hybrid Sys tems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1438SPdFtb@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20121207T140000 DTEND:20121207T160000 DURATION:PT02H0M0S LOCATION:CTL SUMMARY:Romain Testylier - Reachability analysis of nonlinear dynamical sys tems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1441pLePdV@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20121206T150000 DTEND:20121206T160000 DURATION:PT01H0M0S 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:20260307T013644CET-1443PIHbF8@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20121206T140000 DTEND:20121206T150000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Mihail Asavoae - Semantics-Based WCET Analysis END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1446CaWEoO@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20121109T140000 DTEND:20121109T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Damien Massé - Inférences de propriétés de terminaison par it ération de stratégies END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1448hWJVv4@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:HDR DTSTART:20121106T100000 DTEND:20121106T130000 DURATION:PT03H0M0S LOCATION:Maison Jean Kuntzmann SUMMARY:Pascal Lafourcade - Sécurité assisté par ordinateur pour les pri mitives cryptographiques\, les protocoles de vote électroniques et les r éseaux de capteurs sans fil (Computer Aided Security for Cryptographic Pr imitives\, Voting protocols\, and Wireless Sensor Networks) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1451eoNnmt@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20121029T140000 DTEND:20121029T160000 DURATION:PT02H0M0S LOCATION:CTL SUMMARY:Jean-François KEMPF - Exploration de l'espace de design assistée par ordinateur pour les systèmes multi-coeurs (On Computer-Aided Design-S pace Exploration for Multi-Cores) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1453AxCZis@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20121024T140000 DTEND:20121024T170000 DURATION:PT03H0M0S LOCATION:CTL SUMMARY:Selma Saidi - Optimizing DMA Data Transfers for Embedded Multi-Core s END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1456sFotFo@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20121016T153000 DTEND:20121016T173000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Guillaume Brat - An overview of formal methods for Aeronautics at N ASA END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-14596svtFV@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20121002T140000 DTEND:20121002T160000 DURATION:PT02H0M0S 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:20260307T013644CET-1461wFFGRl@129.88.40.24 DTSTAMP:20260307T003644Z 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:20260307T013644CET-1464V6AgPU@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20120913T140000 DTEND:20120913T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Corneliu Popeea - Synthesizing Software Verifiers from Proof Rules END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1466kaKv6M@129.88.40.24 DTSTAMP:20260307T003644Z 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:20260307T013644CET-1468x1Pxcu@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20120705T140000 DTEND:20120705T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Pascal Cuoq - Collaboration d\'analyses dans Frama-C END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1470NOm9i6@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20120626T103000 DTEND:20120626T123000 DURATION:PT02H0M0S 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:20260307T013644CET-1473TdjOzO@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20120626T143000 DTEND:20120626T153000 DURATION:PT01H0M0S 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:20260307T013644CET-1475G7fpBA@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20120621T140000 DTEND:20120621T151500 DURATION:PT01H15M0S LOCATION:salle A. Turing CE4 SUMMARY:Jean-Christophe Filliâtre - Combining Interactive and Automated Th eorem Proving in Why3 END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1477jb8wUW@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20120607T140000 DTEND:20120607T160000 DURATION:PT02H0M0S 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:20260307T013644CET-1480MsAIbN@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20120605T140000 DTEND:20120605T160000 DURATION:PT02H0M0S LOCATION:CTL SUMMARY:Tesnim Abdellatif - Rigorous Implementation of Real-time Systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1482DzFuh4@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20120601T140000 DTEND:20120601T160000 DURATION:PT02H0M0S 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:20260307T013644CET-1485MPHav3@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20120531T140000 DTEND:20120531T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Pavol Cerny - Quantitative Abstraction Refinement END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1487UADfJN@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20120529T150000 DTEND:20120529T170000 DURATION:PT02H0M0S LOCATION:CTL SUMMARY:Rajarshi RAY - Reachability Analysis of Hybrid Systems Using Suppor t Functions END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1489UvamBN@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20120525T140000 DTEND:20120525T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Johannes Reich - A System Perspective on Processes and Their Intera ctions. END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1492Rr5v1G@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20120511T100000 DTEND:20120511T120000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Xavier Urbain - Démonstration automatique : techniques\, outils et certification. END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1494HPlvcx@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20120509T140000 DTEND:20120509T150000 DURATION:PT01H0M0S 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:20260307T013644CET-14965PdVgn@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20120405T140000 DTEND:20120405T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Laura Kovacs - Playing in the Grey Area of Proofs END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1498pWvgbR@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20120322T140000 DTEND:20120322T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Oded Maler - Performance Evaluation of Schedulers in a Probabilisti c Setting END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-15013TB4fK@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20120312T140000 DTEND:20120312T170000 DURATION:PT03H0M0S LOCATION:CTL SUMMARY:Nicolas Berthier - Programmation synchrone de pilotes de périphér iques pour un contrôle global de ressources dans les systèmes embarqués (Synchronous Programming of Device Drivers for Global Resource Control in Embedded Systems) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1503AWXa1S@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20120308T140000 DTEND:20120308T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Goran Frehse - Safety Analysis of Hybrid Systems with SpaceEx END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1506bUcZOP@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20120305T140000 DTEND:20120305T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Sriram Rajamani - Program Analysis and Machine Learning: A Win-Win Deal END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1508aXA2VR@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20120301T140000 DTEND:20120301T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Jerôme Leroux - Vector Addition System Reachability Problem END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-151097pfZz@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20120223T140000 DTEND:20120223T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Franck Petit - Strength of Stabilization vs. Amount of Resources END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1512LA3IVZ@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20120210T140000 DTEND:20120210T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Laurent George - Robustesse temporelle dans les systèmes embarqu és mono et multiprocesseur END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1515Wg2VLS@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20120209T140000 DTEND:20120209T160000 DURATION:PT02H0M0S 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:20260307T013644CET-15174t5r0o@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20120126T140000 DTEND:20120126T150000 DURATION:PT01H0M0S LOCATION:CTL SUMMARY:Tom Henzinger - Quantitative Reactive Modeling END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1520ZjBOCe@129.88.40.24 DTSTAMP:20260307T003644Z 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:20260307T013644CET-15230OUM9c@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20120112T140000 DTEND:20120112T160000 DURATION:PT02H0M0S LOCATION:CTL SUMMARY:Marion DAUBIGNARD - Formalisation de preuves de sécurité concrèt e (Formal Methods for Concrete Security Proofs) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1526CUkduN@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20111118T140000 DTEND:20111118T160000 DURATION:PT02H0M0S LOCATION:Ensimag\, Amphi E SUMMARY:Giovanni Funchal - Contributions à la Modélisation Transactionnel le des Systèmes-sur-Puce (Contributions to Transaction-Level Modeling of Systems-on-a-Chip) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-15281BGZSt@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20111114T140000 DTEND:20111114T153000 DURATION:PT01H30M0S LOCATION:Grande Salle de CE4 SUMMARY:Philippe Suter - Sets with Cardinality Constraints in Satisfiabilit y Modulo Theories END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1531UWNWnc@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20111004T140000 DTEND:20111004T160000 DURATION:PT02H0M0S LOCATION:CTL SUMMARY:Julien Legriel - Optimisation multi-critère et application aux sys tèmes multi-processeurs embarqués (Multi-Criteria Optimization and its A pplication to Multi-Processor Embedded Systems ) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1533Hih5TB@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20110915T140000 DTEND:20110915T160000 DURATION:PT02H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Balaji Raman - On Buffering with Stochastic Guarantees in Resource- Constrained Media Players END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1535nUoU3g@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20110721T140000 DTEND:20110721T150000 DURATION:PT01H0M0S LOCATION:CTL SUMMARY:Pierre Ganty - Pattern-based Verification for Multithreaded Program s END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1538r2c9pn@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20110630T140000 DTEND:20110630T150000 DURATION:PT01H0M0S LOCATION:CTL SUMMARY:Nathalie Bertrand - Determinizing timed automata. END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1540tEfcIZ@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20110628T140000 DTEND:20110628T160000 DURATION:PT02H0M0S LOCATION:CTL SUMMARY:Francesco Logozzo - Practical program verification for the working programmer with CodeContracts and Abstract Interpretation END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1542Pml1EJ@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20110621T140000 DTEND:20110621T170000 DURATION:PT03H0M0S LOCATION:Amphi CTL SUMMARY:VASSILIKI SFYRLA - Modélisation des Systèmes Synchrones en BIP (M odeling Synchronous Systems in BIP) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1545Tp43Pz@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20110526T140000 DTEND:20110526T150000 DURATION:PT01H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Jannik Dreier - Privacy Properties for Voting Protocols: The comple ted picture END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1547dRc3kz@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20110519T140000 DTEND:20110519T160000 DURATION:PT02H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Viktor Kuncak - Towards Implicit Programming END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1550IMUakK@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20110518T103000 DTEND:20110518T113000 DURATION:PT01H0M0S 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:20260307T013644CET-1552Ve0Ue9@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20110316T153000 DTEND:20110316T163000 DURATION:PT01H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Fabio Somenzi - Clause Manipulation for Faster Satisfiability END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1554PRkxC1@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20110303T140000 DTEND:20110303T160000 DURATION:PT02H0M0S 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:20260307T013644CET-1556pAecUP@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20110203T140000 DTEND:20110203T160000 DURATION:PT02H0M0S LOCATION:CTL SUMMARY:IMENE BEN HAFAIEDH - Component-based Systems: from Design to Implem entation END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1559sHURa7@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20110121T103000 DTEND:20110121T123000 DURATION:PT02H0M0S LOCATION:CTL SUMMARY:Sophie Quinton - Design\, verification and implementation of system s of components END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-15614Ib0jZ@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:HDR DTSTART:20101220T140000 DTEND:20101220T160000 DURATION:PT02H0M0S LOCATION:CTL SUMMARY:John Plaice - La programmation Cartésienne (Habilitation à Dirige r des Recherches) (Cartesian Programming (HDR defence)) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1564aEO5pp@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20101118T140000 DTEND:20101118T150000 DURATION:PT01H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Antoine GERBAUD - Le modèle du marcheur pour les réseaux d'intera ctions (Walker model for complex networks) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1566xRCdUj@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20101105T140000 DTEND:20101105T160000 DURATION:PT02H0M0S LOCATION:CTL SUMMARY:Moshe Vardi - From Philosophical to Industrial Logics END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1568HvFrtM@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20101028T133000 DTEND:20101028T160000 DURATION:PT02H30M0S 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:20260307T013644CET-1571wOSGjv@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20100922T150000 DTEND:20100922T173000 DURATION:PT02H30M0S LOCATION:Maison Jean Kuntzmann SUMMARY:Mathias Péron - Contributions à l’analyse statique de programme s manipulant des tableaux (Contributions to the Static Analysis of Program s Handling Arrays) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1573hzRs6S@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20100915T140000 DTEND:20100915T170000 DURATION:PT03H0M0S LOCATION:CTL SUMMARY:Tayeb BOUHADIBA - 42\, Une Approche à Composants pour le prototypa ge Virtuel des Systèmes Embarqués Hétérogènes (42\, A Component-Bas ed Approach to Virtual Prototyping of Heterogeneous Embedded Systems ) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1576xpdS5k@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20100827T100000 DTEND:20100827T120000 DURATION:PT02H0M0S LOCATION:MJK SUMMARY:Manuel Garnacho - Automatisation de la certification formelle de sy stèmes critiques par instrumentation d\\\'interpréteurs abstraits (Autom atic and formal certification of critical systems by instrumentation of ab stract interpreters) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1578lVPk6a@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20100826T190000 DTEND:20100826T200000 DURATION:PT01H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Sébastien Bourdeauducq - Milkymist : un System-on-Chip libre et or ienté video temps réel END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1581Gzruxi@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20100708T140000 DTEND:20100708T150000 DURATION:PT01H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Sophie Quinton - Achieving distributed control through model checki ng END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-15834WkUAB@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20100701T140000 DTEND:20100701T160000 DURATION:PT02H0M0S LOCATION:CTL SUMMARY:Jocelyne Troccaz - TBA END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1585hgTmaS@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20100618T100000 DTEND:20100618T120000 DURATION:PT02H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Arshia Cont - Antescofo : A performance-synchronous language for c omputer music END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1588VKn3C9@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20100617T140000 DTEND:20100617T150000 DURATION:PT01H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Karel Heurtefeux - Localisation qualitative appliquée au routage e t à l\'accès au canal dans les réseaux de capteurs (Qualitative localiz ation applied to routing and MAC layer in Wireless Sensor Networks) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1590hecNvh@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20100527T140000 DTEND:20100527T170000 DURATION:PT03H0M0S LOCATION:CTL SUMMARY:Thanh Hung NGUYEN - Vérification Constructive des Systèmes à bas e de Composants (Constructive Verification for Component-based Systems) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1592MVMPVK@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20100510T100000 DTEND:20100510T110000 DURATION:PT01H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Christophe JOUBERT - Datalog-based Program Analysis with BES and RW L END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1595EF6Vui@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20100510T151500 DTEND:20100510T161500 DURATION:PT01H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Arnaud Sangnier - Weak Time Petri Nets Strike back! END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1597v6p0sI@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20100510T140000 DTEND:20100510T150000 DURATION:PT01H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Nadia El Mrabet - Arithmétique des couplages\, performance et rés istance aux attaques par canaux cachés END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1600T43TaW@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20100510T163000 DTEND:20100510T173000 DURATION:PT01H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Regis Gascon - (Verification of quantitative properties on constr aint automata ) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1602vONCin@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20100507T140000 DTEND:20100507T150000 DURATION:PT01H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Kevin Marquet - Vérification automatique de modèles de systèmes sur puce END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1605wSuf89@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20100507T151500 DTEND:20100507T161500 DURATION:PT01H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Alexandre DONZE - Conception et analyse basée sur les modèles de systèmes hybrides: techniques par simulations\, applications et perspecti ves (Model-based design and analysis of hybrid systems:simulation-based te chniques\, applications and perspectives) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1607iTXEgR@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20100422T140000 DTEND:20100422T150000 DURATION:PT01H0M0S 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 with Internal Aliases in PathCrawler) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1610ga79KJ@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20100407T133000 DTEND:20100407T160000 DURATION:PT02H30M0S LOCATION:CTL SUMMARY:Mohamed Yassin CHKOURI - Modélisation des systèmes temps-réel em barqués en utilisant AADL pour la génération automatique d’applicatio ns formellement vérifiées (Modelling real-time embedded systems using AA DL for the automatic generation of applications formally verified) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1612HLFObu@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20100401T140000 DTEND:20100401T150000 DURATION:PT01H0M0S 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:20260307T013644CET-1614UB4JLG@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20100319T100000 DTEND:20100319T110000 DURATION:PT01H0M0S 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:20260307T013644CET-1616Rts2Ta@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20100309T100000 DTEND:20100309T120000 DURATION:PT02H0M0S LOCATION:CTL SUMMARY:Thomas GAWLITZA - Combining Strategy Iteration with Semidefinite Pr ogramming for Abstract Interpretation END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-16191LuOIA@129.88.40.24 DTSTAMP:20260307T003644Z 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 Sys tème. (Design and Implementation of Component Based Systems. Towards a Un ification of the Software Engineering and the System Paradigms. ) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1621ocnkuj@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20100304T140000 DTEND:20100304T150000 DURATION:PT01H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Ondrej Sery - Code analysis with Blast END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1624dSZu7w@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20100216T140000 DTEND:20100216T150000 DURATION:PT01H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Bahareh Badban - Automated Invariant Generation for the Verificati on of Real-Time Systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1628KKJcup@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:HDR DTSTART:20100204T133000 DTEND:20100204T163000 DURATION:PT03H0M0S LOCATION:Amphi SUMMARY:Marius Bozga - Component-Based Construction of Real-Time Systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1630fvci2b@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:HDR DTSTART:20100129T140000 DTEND:20100129T160000 DURATION:PT02H0M0S LOCATION:Amphi F018\, UFR IMA SUMMARY:Dang Thao - Methods and tools for Computer Aided Design of Embedde d Systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1632KREnBH@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20100114T140000 DTEND:20100114T150000 DURATION:PT01H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Arnaud Sangnier - Reversal-bounded counter machines revisited END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1635VLXwhu@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20091119T160000 DTEND:20091119T170000 DURATION:PT01H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Matthias Althoff - Reachability Analysis of Nonlinear and Hybrid Sy stems with Zonotopes END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1637bBazoV@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20091119T140000 DTEND:20091119T160000 DURATION:PT02H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Bruce Krogh - Research Directions in Cyber-Physical Systems END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1640uvwcaw@129.88.40.24 DTSTAMP:20260307T003644Z 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:20260307T013644CET-1642hN2Ge4@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20091109T140000 DTEND:20091109T170000 DURATION:PT03H0M0S 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 technique s) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1645wmjvUv@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20091029T140000 DTEND:20091029T160000 DURATION:PT02H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Stephane Demri - Les problèmes de couverture et finitude pour les systèmes d'addition de vecteurs arborescents. (The covering and boundedn ess problems for branching vector addition\nsystems ) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1648ONGl2O@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20091028T140000 DTEND:20091028T160000 DURATION:PT02H0M0S LOCATION:MJK SUMMARY:Colas Le Guernic - Calcul d'Atteignabilité des Systèmes Hybrides à Partie Continue Linéaire (Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-16516H4RVu@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20091021T140000 DTEND:20091021T170000 DURATION:PT03H0M0S 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:20260307T013644CET-1653JjFEw4@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20090924T140000 DTEND:20090924T150000 DURATION:PT01H0M0S LOCATION:Grande Salle de VERIMAG SUMMARY:Bageshri KARKARE - Efficiency\, Precision\, Simplicity\, and Gener ality in Interprocedural Data Flow Analysis. END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-16563EURNU@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20090915T140000 DTEND:20090915T150000 DURATION:PT01H0M0S LOCATION:CTL SUMMARY:Dino Distefano - Compositional Shape Analysis by means of Bi-Abduct ion END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1658HudKwl@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20090625T100000 DTEND:20090625T110000 DURATION:PT01H0M0S LOCATION:VERIMAG SUMMARY:Zvonimir Rakamaric - Static and Precise Detection of Concurrency E rrors in Systems Code Using SMT Solvers END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1661zKtAja@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Thesis DTSTART:20090625T140000 DTEND:20090625T150000 DURATION:PT01H0M0S LOCATION:Ampithéatre CTL SUMMARY:Scott Cotton - Sur Quelques Problèmes de la Satisfiabilité (On So me Problems in Satisfiability Solving) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1663DHsS9A@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:HDR DTSTART:20090619T101500 DTEND:20090619T131500 DURATION:PT03H0M0S LOCATION:CTL SUMMARY:David Monniaux - Analyse statique : de la théorie à la pratique (Static analysis: from theory to practice) END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-16657P7THb@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20090514T140000 DTEND:20090514T150000 DURATION:PT01H0M0S LOCATION:CTL SUMMARY:Florian Kammueller - ASPfun: un calcul pour des objets distribués END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1667UFtu6A@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20090507T140000 DTEND:20090507T150000 DURATION:PT01H0M0S LOCATION:VERIMAG SUMMARY:Villard Jules - Proving Copyless Message Passing END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-16706kh7bJ@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20090416T140000 DTEND:20090416T150000 DURATION:PT01H0M0S LOCATION:VERIMAG/AMPHI CTL SUMMARY:Christophe Guillon - Les représentations SSA et Psi-SSA END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1672GXXuww@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20090409T140000 DTEND:20090409T150000 DURATION:PT01H0M0S LOCATION:VERIMAG SUMMARY:Alexandre Donzé - Calcul numérique d'ensembles atteignables po ur les systèmes hybrides et applications END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-1674jfDE8B@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20090402T140000 DTEND:20090402T150000 DURATION:PT01H0M0S LOCATION:VERIMAG SUMMARY:Domagoj Babic - Scalable and Precise Extended Static Checking END:VEVENT BEGIN:VEVENT UID:20260307T013644CET-16762VjBiJ@129.88.40.24 DTSTAMP:20260307T003644Z CATEGORIES:Veri_sem DTSTART:20090305T140000 DTEND:20090305T150000 DURATION:PT01H0M0S LOCATION:VERIMAG SUMMARY:Thomas Gawlitza - Precise Relational Invariants Through Strateg y Iteration END:VEVENT END:VCALENDAR