Home > Verimag > Seminars > Archives

Verimag Seminars before 2009

decembre 2008

    Jeudi 18  / 14:00 /  Barbara Jobstmann    EPFL   Specification-Driven Synthesis and Repair
    Lundi 15  / 13:30 /  Ananda Basu    Verimag   THÈSE : Component-based Modeling of Heterogeneous Real Time Systems in BIP
    Jeudi 11  / 14:00 /  Felix Klaedtke    ETZ Zurich   Alternation Elimination Constructions with an Application to PSL Extended with Past Operators

novembre 2008

    Jeudi 13  / 14:00 /  Jerome Feret    LIENS   Réduction de sémantiques différentielles pour réseaux d'interactions entre protéines par Interprétation Abstraite.

octobre 2008

    Vendredi 31  / 14:00 /  Jasmin Fisher    Computational Biology Group, Microsoft Research Cambridge, UK   The Executable Pathway to Signalling Networks
    Mercredi 29  / 14:00 /  Dejan Nickovic    Verimag   THÈSE : Checking Timed and Hybrid Properties: Theory and Applications
    Jeudi 16  / 14:00 /  Sergio Yovine    Verimag   Séminaire labo : Quelques axes de recherche sur l'implantation de systèmes embarqués soumis aux contraintes non-fonctionnelles

septembre 2008

    Jeudi 25  / 14:00 /  Leandro Buss Becker    Université Fédérale de Santa Catarina, Florianopolis, Brésil   Modeling and Deploying Distributed Embedded Control Systems
    Mercredi 24  / 10:00 /  Steven P. Miller    Rockwell Collins   Formal Methods for Critical Systems
    Vendredi 19  / 10:30 /  Loic Strus    Verimag   THÈSE : Contrôle de qualité de service optimal d'application multimédia
    Jeudi 18  / 14:00 /  Nicolas Halbwachs    Verimag   Séminaire labo : Interprétation abstraite dans l'équipe Synchrone

juillet 2008

    Mardi 15  / 14:00 /  Florian Hölzl    Technische Universität München   Modeling distributed, timed, reactive systems with FOCUS and AutoFOCUS 3 (From theory to practice)
    Mardi 1  / 14:00 /  Mohamad Sawan    Ecole Polytechnique de Montreal   Wireless multi-channel stimulation and sensing from the cortex: Design, test and validation challenges

juin 2008

    Jeudi 12  / 14:00 /  Avshalom Eli    Visiting Professor/UJF   Quantum Measurement: Riddles and Insights into the Micro-World
    Jeudi 05  / 14:00 /  Ananda Basu    Verimag   Distributed Semantics and Implementation for Systems with Interaction and Priority

may 2008

    Mardi 06  / 17:15 /  Pierre Corbineau    Radboud Universiteit Nijmegen, Pays-Bas   A Declarative Language For The Coq Proof Assistant
    Mardi 06  / 16:00 /  Ouassila Labbani    ENS Lyon   Modélisation à haut niveau des applications de traitement systématique à parallélisme massif : Introduction du contrôle et interopérabilité de modèles
    Mardi 06  / 14:00 /  Julien DeAntoni    INRIA Bretagne - équipe Triskell   Utilisation de modèles pour raisonner sur les systèmes temps réels embarqués
    Mardi 06  / 10:00 /  Lobna Kriaa    TIMA   Modélisation des systèmes hétérogènes sur puce : simulation et analyse des performances
    Lundi 05  / 16:00 /  Cecile Braunstein    University of Paris VI   SAT-based fault localization in a Abstraction Refinement Framework

avril 2008

    Mercredi 30  / 14:00 /  Reinhard Wilhelm    Saarland University and AbsInt   Timing Analysis for Hard Real-Time Systems
    Vendredi 25  / 15:00 /  Jérôme Cornet    Verimag   THÈSE : Separation of Functional and Non-Functional Aspects in Transactional Level Models of Systems-on-Chip
    Vendredi 25  / 10:00 /  Reinhard von Hanxleden    University of Kiel   A Multi-Threaded Reactive Processor
    Lundi 21  / 15:00 /  Tahiry Razafindralambo    CNRS/INRIA/Univ. Lille 1   Autour de la couche MAC pour les réseaux sans fil
    Lundi 21  / 13:30 /  Kevin Marquet    INRIA Lille - (projet POPS)   Gestion de mémoire à objets pour système embarqué
    Jeudi 10  / 14:30 /  Guillaume Salagnac    Verimag   THÈSE : Synthèse de gestionnaires mémoire pour applications Java temps-réel embarquées
    Jeudi 10  / 10:00 /  Gilles Muller    École des Mines de Nantes   Documenting and Automating Collateral Evolutions in Linux Device Drivers
    Mercredi 9  / 10:30 /  Susanne Graf    Verimag   Models and Methods for Modelling and Verification of Complex Concurrent Systems
    Lundi 7  / 15:00 /  Ludovic Samper    Verimag   THÈSE : Modélisations et analyses de réseaux de capteurs
    Jeudi 3  / 14:00 /  Khaled El-Fakih    Visitor at Verimag/American University of Sharjah (UAE)   Extended Finite State Machine Based Test Derivation Driven By User Defined Faults

mars 2008

decembre 2007

    Jeudi 20  / 13:30 /  Moez Krichen    Verimag   THÈSE : Model Based Testing for Real-Time Systems.
    Mercredi 19  / 14:00 /  Yussef Bouzouzou    Verimag   Accélération des simulations de systèmes sur puce au niveau transactionnel
    Jeudi 13  / 14:00 /  Aaron Bradley    CU Boulder (currently EPFL)   Reasoning about Arrays
    Jeudi 6  / 15:00 /  Stephane Le Roux    ENS Lyon   CANCELLED Acyclicity of Preferences, Nash Equilibria , and Subgame Perfect Equilibria: Two Proofs of the Equivalence.
    Jeudi 6  / 14:00 /  Matthieu Moy    Verimag   An introduction to (distributed) version control with the example of Git

novembre 2007

    Mercredi 14  / 14:00 /  Mario Sudholt    INRIA, LINA   Flexible and Safe Pointcut/Advice Bindings
    Mercredi 14  / 10:00 /  Shmuel Katz    Technion   Detecting Semantic Interference Among Aspects
    Mardi 13  / 16:00 /  David Stauch    Verimag   THÈSE : Larissa, an Aspect-Oriented Language for Reactive Systems
    Lundi 12  / 16:00 /  Boris Kopf    ETH Zürich   Formal Models for Side-Channel Attacks

Octobre 2007

    Vendredi 26  / 15:00 /  Susan Horwitz    University of Wisconsin-Madison   Better Debugging via Output Tracing and Callstack-Sensitive Slicing
    Vendredi 26  / 14:00 /  Thomas Reps    University of Wisconsin and GrammaTech, Inc   WYSINWYX: What You See Is Not What You eXecute
    Jeudi 25  / 14:00 /  Laure Gonnord    Verimag   THÈSE : Accélération abstraite pour l'amélioration de la précision en analyse des relations linéaires
    Lundi 15  / 14:30 /  Tarik Nahhal    Verimag   THÈSE : Model-Based Testing of Hybrid Systems
    Vendredi 12  / 14:00 /  Ramzi Salah    Verimag   THÈSE : On Timing Analysis of Large Systems

juin 2007

    Lundi 25  / 14:00 /  Alexandre Donze    Verimag   THÈSE : Trajectoires pour la Vérification et la Commande de Systèmes Continus et Hybrides

may 2007

    Jeudi 10  / 14:00 /  Gregory Batt    Verimag   Vérification de réseaux de régulation génique en présence d'incertitudes sur les paramêtres
    Mercredi 2  / 14:00 /  FU Yuxi    Shanghai Jiaotong University   On the Expressiveness of Pi Calculus
    Jeudi 3  / 14:00 /  FU Yuxi    Shanghai Jiaotong University   Fair Ambient

avril 2007

    Jeudi 19  / 14:00 /  Romain Janvier    INRIA Sophia-Antipolis   Vers une certification des preuves de sécurité des algorithmes cryptographiques

mars 2007

    Jeudi 29  / 14:00 /  Simon Bliudze    Verimag   The Algebra of Connectors --- Structuring Interaction in BIP
    lundi 26  / 14:00 /  Claude Helmstetter    Verimag   THÈSE : Validation de modèles de systèmes sur puce en présence d'ordonnancements indéterministes et de temps imprécis
    jeudi 15  / 14:00 /  Loïc Strus    Verimag   Using Speed Diagrams for Symbolic Quality Management

fevrier 2007

    Jeudi 22  / 14:00 /  Arnaud Sangnier    LSV, ENS Cachan   Towards Model-Checking Pointer Systems
    Jeudi 15  / 14:00 /  Maria Sorea    EADS   Dubious Witnesses and Spurious Counterexamples
    Jeudi 8  / 14:00 /  ac.at/people/lkovacs/"> Laura Kovacs    Research Institute for Symbolic Computation (RISC) Linz, Austria   Using Symbolic Summation and Polynomial Algebra for Automated Generation of Polynomial Invariants in Theorema
    Vendredi 2  / 14:00 /  John Plaice    University of New South Wales, Sydney, Australia   La programmation cartésienne: Le langage de programmation TransLucid

++++

janvier 2007

    Jeudi 25  / 14:00 /  Maria Sorea    EADS   CANCELLED Model Checking a Fault-Tolerant Startup Algorithm: From Design Exploration to Exhaustive Fault Simulation
    Mercredi 17  / 14:00 /  Norman Scaife    LASMEA   Vision and control applications in the Hume Language
    jeudi 11  / 14:00 /  David Monniaux    LIENS   Analyseur Astree : realisations et perspectives
    vendredi 5  / 14:00 /  Jean-Charles Tournier    University of New Mexico   Developpement a base de composants - Des systemes hautes performances aux reseaux de capteurs

decembre 2006

    jeudi 21  / 14:00 /  Grigore Rosu    Urbana-Champaign University   Monitoring-based Programming and Analysis
    mardi 19  / 10:00 /  Philippe Clauss    Universite Louis Pasteur de Strasbourg   Maximisation symbolique de polynomes definis sur des ensembles convexes et applications a l'estimation du besoin memoire des programmes
    lundi 18  / 10:00 /  Cesar Sanchez    Stanford University   Deadlock Avoidance for Distributed Real-Time and Embedded Systems
    lundi 18  / 14:00 /  Ismail Assayad    Verimag   THÈSE: A Scalable Framework for Modelling and Performance Analysis of Multiprocessor Embedded Systems

novembre 2006

    jeudi 23  / 14:00 /  Adam Rogalewicz    Brno University of Technology   Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
    mercredi 15  / 14:00 /  Christos Sofronis    Verimag   THÈSE: Embedded Code Generation from High-level Heterogeneous Components

Octobre 2006

    Mercredi 11  / 14:00 /  Laurent Mazare    Verimag   THÈSE: Computational Soundness of Symbolic Models for Cryptographic Protocols
    Lundi 2  / 14:00 /  Abdelkarim-Aziz Kerbaa    Verimag   THÈSE: Strategies d'Ordonnancement Conditionnelles Utilisant des Automates Temporises

Septembre 2006

    Jeudi 28  / 14:00 /  Graham Steel    University of Edinburgh   Formal Analysis of Security APIs
    Lundi 25  / 14:00 /  Marc Duranton    Philips Research   Challenges in programming high performance embedded streaming applications
    Vendredi 22  / 11:00 /  Georgios Fainekos    University of Pennsylvania Philadelphia   Robustness of Temporal Logic Specifications (and an application to verification using simulation)
    Jeudi 14  / 14:00 /  Edith Elkind    University of Liverpool   How to buy a subgraph: game theory meets algorithm design
    Lundi 11  / 14:00 /  Romain Janvier    Verimag   THÈSE: Liens entre modeles symboliques et computationnels pour les protocoles cryptographiques utilisant des hachages
    Jeudi 7  / 14:00 /  Cedric Fournet    Microsoft Research   Verified Interoperable Implementations of Security Protocols

Juin 2006

    Jeudi 29  / 14:00 /  Tristan LeGall    IRISA   Verification de protocoles de communication / Interpretation abstraite des langages reguliers
    Jeudi 15  / 10:00 /  Jacques Combaz    Verimag/STMicroelectronics   THÈSE: Conception de Systemes Adaptatifs Surs et Optimaux
    Jeudi 1  / 14:00 /  Bruno Berstel    ILOG SA   Using Constraint Programming to Analyze Rule Programs

May 2006

    Jeudi 4  / 14:00 /  Jean-Philippe Babau    INSA Lyon   Formalisation et structuration des architecture operationnelle pour les systemes embarques temps reels

Avril 2006

    Jeudi 27  / 14:00 /  Philippe Audebaud    INRIA Sophia   Verification formelle d'algorithmes probabilistes dans Coq
    Vendredi 14  / 14:00 /  Goran Frehse    Verimag   Les Systemes Hybrides dans la Conception des Systemes Embarques
    Vendredi 14  / 15:00 /  Antoine Girard    Verimag   Methodes Algorithmiques pour l'Analyse de Systemes Hybrides

Avril 2006

    Jeudi 6  / 14:00 /  Renaud Lachaize    Institute of Computer Science - Foundation for Research and Technology Hellas   Systemes flexibles pour applications communicantes

Mars 2006

    Jeudi 23  / 14:00 /  Franck Cassez    IRCCyN - UMR CNRS 6597   Sensor Minimization Problems in Fault Diagnosis
    Jeudi 16  / 14:00 /  Mark Greenstreet    University of British Columbia   Surfing Interconnect

Fevrier 2006

    Jeudi 16  / 14:00 /  Mathieu Baudet    Laboratoire Specification et Verification - ENS Cachan   Protecting security protocols against guessing attacks: towards computationally-sound, automatic analyses.
    Jeudi 9  / 14:00 /  Gregor Goessler    INRIA Rhone-Alpes Projet Pop-Art   Construction basee sur composants de systemes reactifs en Prometheus
    Mercredi 8  / 10:00 /  David Teller    University of Sussex   Ressources + pi-calcul = controle

Janvier 2006

    Mercredi 18  / 14:00 /  Moni Naor    Weizmann Institute of Science   Spam fighting and The Complexity of Pebbling Graphs

Decembre 2005

    Vendredi 9  / 15:00 /  Stephen Edwards    Columbia University   SHIM: A Deterministic Model for Heterogeneous Embedded Systems
    Vendredi 9  / 10:30 /  Matthieu Moy    Verimag / ST Microelectronics   THÈSE: Techniques et outils pour la verification de Systemes-sur-Puce au niveau transaction
    Jeudi 8  / 14:00 /  Katerina Pokozy    Universita degli Studi di Trento   Analysis of UML specifications using formal methods techniques

Novembre 2005

    Jeudi 24  / 14:00 /  Amir Pnueli    New York University   Abstraction-Aided Verification of Procedural Programs
    Mardi 22  / 10:00 /  Daniel Mery    LORIA   Characterizing Provability in BI's Pointer Logic through Resource Graphs
    Lundi 14  / 14:30 /  Jan Mikac    Verimag   THÈSE: Raffinements et preuves de systemes Lustre
    Jeudi 3  / 14:00 /  Christos Sofronis    Verimag   Semantics-preserving and memory-efficient implementation of inter-task communication on static-priority or EDF schedulers

Octobre 2005

    Vendredi 28  / 14:00 /  Adrian Curic    Verimag   THÈSE: Implementing Lustre Programs on Distributed Platforms with Real-time Constrains
    Jeudi 27  / 14:00 /  Gilles Grimaud    RD2P/POPS   Pre-deploiement et gestion des memoires dans JITS
    Jeudi 20  / 14:00 /  Franck Cassez    IRCCYN   Optimal Strategies in Priced Timed Game Automata
    Jeudi 13  / 14:00 /  Oded Maler    Verimag   On Optimal and Reasonable Control in the Presence of Adversaries
    Mardi 4  / 15:15 /  Cyril Pachon    Verimag   THESE : Une approche basee sur les modeles pour le test de robustesse

Septembre 2005

    Vendredi 2  / 10:00 /  Chaker Nakhli    Verimag   THESE : Approche Fondee sur les Modeles pour Java Temps-Reel

Juillet 2005

    Mercredi 13  / 14:00 /  Kanchi Gopinath    Indian Institute of Science   Improved Probabilistic Models for 802.11 Protocol Verification
    Lundi 11  / 14:00 /  Ferucio Laurentiu Tiplea    University of Iasi   Abstractions of Data Types
    Mardi 5  / 14:00 /  Rajeev Alur    University of Pennsylvania   The Benefits of Exposing Calls and Returns

Juin 2005

14:00 /  -->
    Mercredi 1  / 12:30 /  Benoit Meister    LSIIT   Methodes polyedriques en nombres entiers pour les nids de boucles
K. Gopinath    Indian Institute of Science   Improved Probabilistic Models for 802.11 Protocol Verification

May 2005

    Mercredi 18  / 14:00 /  David Merchat    Verimag   THÈSE: Reduction du nombre de variables en analyse de relations lineaires

Avril 2005

    Jeudi 14  / 14:00 /  Claude Jard    ENS Cachan   Depliage symbolique de reseaux de Petri temporels pour le diagnostic temporise de systemes repartis

Mars 2005

    Jeudi 31  / 14:00 /  Mila Majster-Cederbaum    Institut fuer Informatik, Universitaet Manheim   Towards the hierarchical verification of reactive systems
    Mercredi 16  / 10:00 /  Lionel Morel    Verimag   THÈSE: Exploitation des structures regulieres et des specifications locales pour le developpement correct de systemes reactifs de grande taille
    Mardi 15  / 14:00 /  Antoine Girard    University of Pennsylvania   Approximation metrics for discrete and continuous systems
    Jeudi 3  / 14:00 /  Katell Morin-Allory    IRISA/TIMA   Verification formelle dans le Modele Polyedrique

Fevrier 2005

    Jeudi 24  / 14:00 /  Yu ZHANG    LSV   Verification of cryptographic protocols via logical relations
    Jeudi 17  / ANNULE /  Katell Morin-Allory    IRISA/TIMA   Verification formelle dans le Modele Polyedrique

Janvier 2005

++++

Decembre 2004

   
    Jeudi 9  / 14:00 /  Christophe Wolinski    IRISA   A Constraints Programming Approach to Communication Scheduling on SoPC Architectures
    Jeudi 9  / 10:00 /  Liana Bozga    Verimag   THÈSE: Methodes algorithmiques de verification des protocoles cryptographiques

Novembre 2004

    Jeudi 25  / 14:00 /  Stephane Messika    LSV   Coupling et auto-stabilisation

Juin 2004

    Jeudi 24  / 14:00 /  Alfredo Olivero    Univ. Argentina de la Empresa   A Timed Automata Slicer based on Observers
    Mardi 22  / 10:00 /  Philippe Clauss    Univ. Louis Pasteur, Strasbourg   Approche symbolique de l'expansion de Bernstein pour l'analyse et l'optimisation de programmes
    Mardi 22  / 14:00 /  Marcelo Zanconi    Verimag   THÈSE: Modelisation et Analyse de Systemes Temps Reel avec Preemption, Incertitude et Dependences
    Jeudi 17  / 14:00 /  Cuihtlauac ALVARADO    FT RD   Mobile (Phone not Code) Application Evaluation Issues
    Mercredi 16  / 14:00 /  Doron Peled    University of Warwick   Black Box Checking
    Lundi 14  / 10:00 /  Victor Braberman    Univ. Buenos Aires   VTS: Visual Timed Event Scenarios
    Jeudi 10  / 14:00 /  Yves Sorel    INRIA Rocquencourt   AAA/SynDEx and scheduling of distributed embedded systems with multiple real-time constraints
    Vendredi 4  / 14:00 /  Francois Felix Ingrand    LAAS   Problemes de Planification des Robots Autonomes
    Jeudi 17  / ANNULE /  Doron Peled    University of Warwick   Black Box Checking
    Jeudi 10  / ANNULE /  Raja Sengupta    UC Berkeley   The Distribution of Synchronous Programs
    Jeudi 3  / ANNULE /  Raja Sengupta    UC Berkeley   On the Control of Networked Multi-Vehicle Systems

Mai 2004

    Jeudi 27  / 14:00 /  Paul Caspi    Verimag   Modeles synchrones et ordonnancements pre-emptifs

Avril 2004

    Jeudi 29  / ANNULE /  Christophe Wolinski    IRISA   A Constraints Programming Approach to Communication Scheduling on SoPC Architectures
    Mercredi 28  / 14:00 /  Dumitru Potop    INRIA   Concurrence dans les systemes synchrones
    Mercredi 28  / 12:00 /  Yannick LeMoullec    Aalborg University   Aide a la conception de systemes sur puces heterogenes par l'exploration parametrable des solutions au niveau systeme
    Vendredi 23  / 11:00 /  Cedric Lhoussaine    University of Sussex   Un systeme de types dependants pour le calcul des Ambiants
    Jeudi 22  / 14:00 /  Nicolas Markey    LSV   Paths Model Checking
    Mercredi 21  / 14:00 /  Miramond Benoit    EVRY   Methodologie de partitionnement logiciel/materiel de systemes a description multi-modeles
    Mercredi 21  / 12:00 /  Christophe Rippert    INRIA Futurs   Systemes embarques adaptables et securises
    Jeudi 15  / 14:00 /  Samy Metfali       Environnement de simulation distribue et heterogene de SoCs
    Mercredi 14  / 12:00 /  Yannick Chevalier    LORIA   Problemes d'accessibilite appliques a l'analyse automatique de protocoles cryptographiques.
    Mercredi 14  / 14:00 /  Ferid Gharsalli    TIMA   HW-SW Interfaces Modeling & Design for Multi-Processor** SoC
    Jeudi 8  / 14:00 /  Jerome Leroux    Universite de Montreal   Image Computation In Infinite State Model Checking

Mars 2004

    Jeudi 25  / 14:00 /  Christos Kloukinas    VERIMAG   Scheduler Synthesis, Analysis & Implementation of Real-Time Java Applications
    Jeudi 18  / 14:00 /  Razvan Diaconescu    IMAR   Formal specification and verification with CafeOBJ: logical foundations and methodologies
    Jeudi 11  / 14:00 /  Didier Galmiche    LORIA   Modeles de ressources et preuves en logique BI
    Jeudi 4  / 14:00 /  Stavros Tripakis    VERIMAG   Testing conformance of real-time applications by automatic generation of observers

Fevrier 2004

    Jeudi 12  / 14:00 /  Tom Hirschowitz    ENS Lyon   Les modules mixins

Janvier 2004

    Jeudi 8  / 14:00 /  Klaus Havelund    NASA Ames   Rule-Based Runtime Verification
++++

Decembre 2003

    Vendredi 19  / 14:00 /  Stefan Leue    Albert-Ludwigs-University Freiburg   A Scalable Incomplete Boundedness Test for CFSM-based Modeling Languages
    Vendredi 19  / 10:15 /  Manuel AGUILAR    Verimag   THÈSE: Contribution a la validation de systhmes de processus communiquant par files d'attente: analyse statique pour la riduction de files

Novembre 2003

    Jeudi 20  / 10:30 /  Thierry Cachat    LSV ENS Cachan    Introduction à la théorie des jeux
    Jeudi 20  / 14:00 /  Fabien Gaucher    VERIMAG    THÈSE: ÉTUDE DU DÉBOGAGE DES SYSTÈMES RÉACTIFS ET APPLICATION AU LANGAGE SYNCHRONE LUSTRE

Septembre 2003

    Mardi 18  / 14:00 /  Marco Sanvido    UC Berkeley    xGiotto: Structured Reactive Programming

Juillet 2003

    Mardi 18  / 14:00 /  Nicola Muscettola    NASA    TALK 1: Planning, Execution, Life, the Universe and Everything
TALK 2: Computing the Envelope for Stepwise-Constant Resource Allocations

Juin 2003

    Mardi 17  / 14:00 /  Grigore Rosu    Urbana Champaign University    Runtime Safety Analysis of Multithreaded Programs
    Mercredi 18  / ANNULÉ /  Nicola Muscettola    NASA    TALK 1: Planning, Execution, Life, the Universe and Everything
TALK 2: Computing the Envelope for Stepwise-Constant Resource Allocations
      lundi 2  / 14:00 /  Marsha Chechik    University of Toronto    Multi-Valued Model-Checking (Theory, Implementation, Applications)

Mai 2003

      mercredi 28  / ANNULÉ /  Sébastien GÉ    CEA, France    Outlines of the ACCORD/UML methodology
      mardi 27  / 10:00 /  Moez Mahf    VERIMAG    THÈSE : Sur la vérification de la satisfaction pour la logique des différences
      jeudi 15  / 14:00 /  Christos Klouk    VERIMAG    Synthesis of Safe, QoS Extendible, Application Specific Schedulers for Heterogeneous Real-Time Systems

Avril 2003

      jeudi 24  / 14:00 /  Marco S    UC Berkeley    Platform-based Design Methodologies for Wireless Protocols
      mardi 22  / 12:00 /  Christophe Woli    Irisa/Inria-Rennes   
      jeudi 17  / 14:00 /  Jean-François M    CNET    Peut-on formaliser simplement des systèmes complexes ?
      vendredi 18  / 10:00 /  Thierry Ca    RWTH Aachen    Méthodes symboliques pour les jeux à pile
      jeudi 10  / 14:00 /  Areski Nait Abda    Université de Western - Ontario & invité du Projet Logical, INRIA Futurs    Reasoning with partial information: a Coq experiment

Mars 2003

      jeudi 20 /  14:00  /  Philippe Gerner ICPS, Strasbourg La sémantique des directives au compilateur
      jeudi 13 /  14:00  /  Thao Dang VERIMAG Counter-Example Guided Predicate Abstraction of Hybrid Systems
      mercredi 12 /  10:00  /  Klaus Have NASA Ames Reducing False Positives in Runtime Analysis of Deadlocks
      lundi 10 /  10:00  /  Mooly Sagiv Tel-Aviv University Verifying Temporal Heap Properties Specified via Evolution Logic

Février 2003

      mercredi 26 /  14:00  /  VERIMAG   :   Jean-Luc Lambert TNI-Valiosys LPV: a new technique, based on linear programming, to formally prove or disprove safety properties on software and hardware systems
      mercredi 19 /  10:30  /  VERIMAG   :   Seffi Naor Technion Haifa, Israel Control Message Aggregation in Group Communication Protocols
      jeudi 13 /  14:00  /  Yassine Lakhnech VERIMAG Modèles et abstractions pour la vérification des protocoles cryptographiques

Janvier 2003

      jeudi 16 /  14:00  /  Alexandre BOISSEAU LSV Abstractions dédiées à l'analyse formelle de protocoles d'échanges optimistes

++++

Décembre 2002

      jeudi 19 /  14:00  /  Olivier Bournez Inria Lorraine Caractérisations Syntaxiques des Classes de Complexité
      jeudi 12 /  14:00  /  Joseph Sifakis VERIMAG Composition pour l'ingénierie à base de composants

Novenmbre 2002

      jeudi 28 /  14:00  /  Yasmina Abded VERIMAG Thèse : Modélisation et résolution de problèmes d'ordonnancement à l'aide d'automates temporisés.
      reporté au jeudi 21 /  14:00  /  Frédéric Prost Leibniz Grenoble Analyse de non-interference pour les processus mobiles par abstraction de sortes

Octobre 2002

      jeudi 03 /  14:00  /  David Harel Weizmann Institute An Algorithmic Approach to Odor Communication and Reproduction

Septembre 2002

      mardi 24 /  14:00  /  Carnegie Mellon University Verifying Switched-Mode Computer Controlled Systems
      jeudi 19 /  14:00  /  VERIMAG Speedup Prediction for Selective Compilation of Embedded Java Programs
      vendredi 13 /  14:00  /  University of California, Santa Cruz Interfaces: a formal model for system design

Juillet 2002

      vendredi 12 /  14:00  /  Lucian Gh VERIMAG Thèse : Génération automatique de tests de conformité pour les protocoles de télécommunication
      vendredi 05 /  14:00  /  VERIMAG Thèse : Analyse Algorithmique de Systèmes Hybrides Polygonaux

Juin 2002

      jeudi 27 /  14:00  /  Catalin VERIMAG Computing reachability relations in timed automata
      jeudi 13 /  14:00  /  Oded M VERIMAG On Control with Bounded Computational Ressources
      jeudi 06 /  14:00  /  Jean-François M FT R&D Invariants inductifs dans un système temporisé

Mai 2002

      vendredi 24 /  14:00  /  VERIMAG   :   J.M. Davoren Australian University of Canberra Design and synthesis of robust switching controllers for hybrid systems, using modal logic
      vendredi 24 /  10:00  /  VERIMAG   :   Paulo Tabuada University of Pennsylvania Compositional Abstractions for Continuous and Hybrid Systems
      jeudi 23 /  11:00  /  Philippe Cl Université de Strasbourg La compilation et l'optimisation de programme pour les systèmes enfouis
      jeudi 16 /  14:00  /  David Harel Weizmann Institute An Algorithmic Approach to Odor Communication and Reproduction
      mercredi 15 /  17:00  /  David Harel Weizmann Institute Computers are Not Omnipotent
      vendredi 3 /  14:00  /  Saddek Bens VERIMAG vérification des systèmes infinis : limites et complexité

Avril 2002

      lundi 29 /  11:00  /  Kamel Bark CEDRIC Vérification paramétrée de systèmes concurrents : l'apport de l'analyse structurelle des réseaux de Petri
      jeudi 25 /  15:30  /  Sorin Strat INRIA Sophia Proofs by Induction with Contextual Cover Sets
      jeudi 25 /  14:00  /  Pascal Fr INRIA Rennes Cadres et contrôles pour la programmation par aspects
      mercredi 24 /  14:00  /  Abdelhakim Khatab< INSA Lyon Contrôle stabilisant des systèmes à événements discrets temporels : application au recouvrement des défaillances des systèmes de production

Mars 2002

      jeudi 21 /  14:00  /  ENSIMAG amphi E   :   Fabien Dagnat ENSEEIHT, Toulouse Vérification statique de programmes répartis
      vendredi   1 /  14:00  /  VERIMAG   :   P.S. Thiagarajan Université de Singapour Modeling Interfaces as Cyclic Transaction Processes

Janvier 2002

      jeudi 17 /  14:00  /  VERIMAG   :   Thomas Genet IRISA/IFSIC, Rennes Analyse d'atteignabilité dans les systèmes de réécriture à l'aide de Timbuk
      jeudi 03 /  15:00  /  VERIMAG   :   Radu Iosif Kansas State University Symmetry Reductions for Explicit-State Model Checking of Software
++++

Décembre 2002

      jeudi 19 /  14:00  /  Olivier Bournez Inria Lorraine Caractérisations Syntaxiques des Classes de Complexité
      jeudi 12 /  14:00  /  Joseph Sifakis VERIMAG Composition pour l'ingénierie à base de composants


Novenmbre 2002

      jeudi 28 /  14:00  /  Yasmina Abdedd VERIMAG Thèse : Modélisation et résolution de problèmes d'ordonnancement à l'aide d'automates temporisés.
      reporté au jeudi 21 /  14:00  /  Frédéric Prost Leibniz Grenoble Analyse de non-interference pour les processus mobiles par abstraction de sortes


Octobre 2002

      jeudi 03 /  14:00  /  David Harel Weizmann Institute An Algorithmic Approach to Odor Communication and Reproduction


Septembre 2002

      mardi 24 /  14:00  /  Carnegie Mellon University Verifying Switched-Mode Computer Controlled Systems
      jeudi 19 /  14:00  /  VERIMAG Speedup Prediction for Selective Compilation of Embedded Java Programs
      vendredi 13 /  14:00  /  University of California, Santa Cruz Interfaces: a formal model for system design


Juillet 2002

      vendredi 12 /  14:00  /  Lucian Gh VERIMAG Thèse : Génération automatique de tests de conformité pour les protocoles de télécommunication
      vendredi 05 /  14:00  /  VERIMAG Thèse : Analyse Algorithmique de Systèmes Hybrides Polygonaux


Juin 2002

      jeudi 27 /  14:00  /  Catalin VERIMAG Computing reachability relations in timed automata
      jeudi 13 /  14:00  /  Oded M VERIMAG On Control with Bounded Computational Ressources
      jeudi 06 /  14:00  /  Jean-François Mo FT R&D Invariants inductifs dans un système temporisé


Mai 2002

      vendredi 24 /  14:00  /  VERIMAG   :   J.M. Davoren Australian University of Canberra Design and synthesis of robust switching controllers for hybrid systems, using modal logic
      vendredi 24 /  10:00  /  VERIMAG   :   Paulo Tabuada University of Pennsylvania Compositional Abstractions for Continuous and Hybrid Systems
      jeudi 23 /  11:00  /  Philippe Cla Université de Strasbourg La compilation et l'optimisation de programme pour les systèmes enfouis
      jeudi 16 /  14:00  /  David Harel Weizmann Institute An Algorithmic Approach to Odor Communication and Reproduction
      mercredi 15 /  17:00  /  David Harel Weizmann Institute Computers are Not Omnipotent
      vendredi 3 /  14:00  /  Saddek Bensalem VERIMAG vérification des systèmes infinis : limites et complexité

Avril 2002

      lundi 29 /  11:00  /  Kamel Barkaoui CEDRIC Vérification paramétrée de systèmes concurrents : l'apport de l'analyse structurelle des réseaux de Petri
      jeudi 25 /  15:30  /  Sorin Stratulat INRIA Sophia Proofs by Induction with Contextual Cover Sets
      jeudi 25 /  14:00  /  Pascal Fradet INRIA Rennes Cadres et contrôles pour la programmation par aspects
      mercredi 24 /  14:00  /  Abdelhakim Khatab INSA Lyon Contrôle stabilisant des systèmes à événements discrets temporels : application au recouvrement des défaillances des systèmes de production


Mars 2002

      jeudi 21 /  14:00  /  ENSIMAG amphi E   :   Fabien Dagnat ENSEEIHT, Toulouse Vérification statique de programmes répartis
      vendredi   1 /  14:00  /  VERIMAG   :   P.S. Thiagarajan Université de Singapour Modeling Interfaces as Cyclic Transaction Processes


Janvier 2002

      jeudi 17 /  14:00  /  VERIMAG   :   Thomas Genet IRISA/IFSIC, Rennes Analyse d'atteignabilité dans les systèmes de réécriture à l'aide de Timbuk
      jeudi 03 /  15:00  /  VERIMAG   :   Radu Iosif Kansas State University Symmetry Reductions for Explicit-State Model Checking of Software
++++

Décembre 2001

      mardi 18 /  10:30  /  MJK   :   Karine Altisen VERIMAG Thèse : Application de la synthèse de contrôleur à l'ordonnancement de systèmes temps-réel
      mercredi 12 /  14:00  /  VERIMAG   :   Claude Jard IRISA/CNRS, Rennes Principes pour synthétiser des cas de test répartis en utilisant un modèle de "true-concurrency"
      mercredi 12 /  10:30  /  MJK   :   Aurore Collomb-Annichini VERIMAG Thèse : Vérification d'automates étendus : algorithmes d'analyse symbolique et mise en oeuvre.
      mardi 11 /  14:00  /  MJK   :   Catalin Dima VERIMAG Thèse : Théorie algébrique des langages formels temps réel
      lundi 10 /  15:30  /  VERIMAG   :   Gilles Muller INRIA Projet Compose Domain Specific Languages: a Safe and Efficient Approach to Operating System Design
      lundi 10 /  14:00  /  VERIMAG   :   Nils Klarlund AT&T Labs-Research Mona tutorial--automata-based symbolic computation
      jeudi   6  /  14:00  /  VERIMAG   :   Jérôme Feret LIENS, Paris Interprétation Abstraite des Systèmes Mobiles


Novembre 2001

      jeudi 29  /  14:00  /  VERIMAG   :   Christoph Meyer Kirsch University of Berkeley The Embedded Abstract Machine


Octobre 2001

      18  /  14:00  /  VERIMAG   :   Christos Kloukinas INRIA Rocquencourt Spin-ning Software Architectures: A Method for Exploring Complex Systems
      11  /  14:00  /  VERIMAG   :   Véronique Cortier LSV, ENS Cachan Un algorithme pour prouver le secret des protocoles cryptographiques


Juin 2001

      28  /  14:00  /  VERIMAG   :  A. Boisseau LSV, ENS Cachan Interpretation abstraite : une approche algébrique


Mai 2001

      31  /  14:00  /  VERIMAG   :  P. Bouyer LSV, ENS Cachan Updatable timed automata
      10  /  11:00  /  VERIMAG   :  A. Rabinovich Tel-Aviv University On Compositional method and its limitations


Avril 2001

       5  /  14:00  /  VERIMAG   :  M. Fränzle Oldenburg, Allemagne What will be eventually true of hybrid automata?


Mars 2001

      22  /  14:00  /  VERIMAG   :  G. Schneider VERIMAG On the decidability of the reachability problem for planar differential inclusions
      15  /  14:00  /  VERIMAG   :  G. Pace VERIMAG Verification Techniques for Hardware Compilers of Embedded Language

Décembre 2000

       7  /  14:00  /  VERIMAG   :  R. Morin T. U. Dresden, Allemagne Quelques resultats recents sur les langages reguliers de MSC


Novembre 2000

      30  /  14:00  /  VERIMAG   :  P. Koiran ENS, Lyon Propriétés décidables et indécidables des systèmes linéaires saturés
      17  /  14:00  /  MJK   :  C. Dumas VERIMAG Méthodes déductives pour la preuve de programmes Lustre
       9  /  14:00  /  VERIMAG   :  A. Miné Ecole Normale Supérieure Représentation d'ensembles de contraintes de somme ou de différence de deux variables et application à l'analyse automatique de programmes


Octobre 2000

      27  /  14:00  /  VERIMAG   :  J. Goubault-Larrecq LSV, ENS Cachan Une méthode automatique de vérification de protocoles cryptographiques
      11  /  14:00  /  VERIMAG   :  J.F. Raskin Université Libre de Bruxelles, Belgique Abstract Interpretation of Game Properties
      10  /  14:00  /  MJK   :  T. Dang VERIMAG Vérification et synthèse des systèmes hybrides


Septembre 2000

      25  /  14:00  /  MJK   :  B. Jeannet VERIMAG Partitionnement dynamique dans l'Analyse de Relation Linéaire et application à la vérification de programmes synchrones


Juin, 2000

15 VERIMAG 16:00 A. Kurzhanski Moscow State University New turns in ellipsoidal calculus
17:00 I. Digailova Moscow State University Dynamic systems with mixed uncertainty: their evolution and estimation
8 VERIMAG 14:00 Gordon Pace Chalmers, Suède Embedding Hardware Description Languages
Koen Claessen Chalmers, Suède Verifying Safety Properties using Induction
6 VERIMAG 16:00 Jean Francois Raskin Universté Libre de Bruxelles, Belgique Logics, Automata and Classical Theories for Deciding Real Time

Mai, 2000

1819 Journées VERIMAG:
18 Amphi F22, ENSIMAG 14:00 Eric Gressier CNAM, France Cohérence Causale Temporelle : Définitions, Algorithmes, et Utilisation
15:30 John Rushby SRI International Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification
19 MJK 09:30 Oded Maler VERIMAG Vérification des Systèmes Discrets, Temporisés et Hybrides
11:30 Saddek Bensalem VERIMAG Vérification Algorithmique et Déductive basée sur l'Abstraction : Méthodes et Outils
16:00 Wolfgang Thomas Univ. Aachen Uniform and nonuniform recognizability
17 Amphi D, ENSIMAG 14:00 Florence Maraninchi VERIMAG Aspects "langage" dans le développement sûr de systèmes et logiciels critiques
15:30 Laurence Pierre CMI, Marseille Travaux en cours dans le cadre de la verification formelle de systemes informatiques
11 VERIMAG 13:00 Yves Ledru LSR-IMAG Vers l'intégration d'UML et de méthodes formelles
4 VERIMAG 14:00 Zakariae Bouziane Valiosys, Caen A primitive recursive algorithm for the general Petri net reachability problem

Avril, 2000

7 VERIMAG 14:00 Hans Toetenel University of Delft, The Netherlands Splitting Trees in Parametrical Model Checking

Mars, 2000

16 VERIMAG 16:30 Uwe Glaesser Heinz Nixdorf Institut, Paderborn Model-Based Engineering of Distributed Embedded Systems: a Case Study from Industrial Manufacturing
13 VERIMAG 13:00 Richard Trefler Univ. of Texas at Austin Symmetry in Verification

Février, 2000

24 MJK 14:00 Bruce Lewis US Army Aviation and Missile Command MetaH, An Architecture Description Language and Integration Toolset for Real-Time High Assurance Systems
10 VERIMAG 14:00 Jan H. van Schuppen CWI, The Netherlands Decentralized control of discrete-event systems
3 VERIMAG 14:00 Amir Pnueli Weizmann, Israel Progress in Regular Model Checking: Acceleration and Liveness

Decembre, 1999

17 MJK 14:00 Marius Bozga VERIMAG These: Verification symbolique pour les protocoles de communication

Novembre, 1999

26 MJK 10:00 Hermann Kopetz Technical University of Vienna, Austria Architecture Design is Interface Design
4 VERIMAG 14:00 Stefan Leue Waterloo, Canada The Formal Treatment of Message Sequence Chart Specifications

Octobre, 1999

14 Salle 1, Tour IRMA, RDC 16:00 Alexander Kurzhanski Moscow State University Mathematical Problems of Reachability Analysis: from Theory to Computation
7 VERIMAG 14:00 Peter Niebert VERIMAG, France Partial Order Reductions in State Space Search Tutorial -- and an new method too!

Septembre, 1999

30 ENSIMAG, Amphi "D" 14:00 Shankar Sastry Berkeley, USA Millirobotics for Minimally Invasive Telesurgery
16 ENSIMAG, Amphi "E" 14:00 Leslie Lamport Compaq, USA The Bakery Algorithm Rises Again or Golden Oldies from the '70s

Juin, 1999

24 VERIMAG 14:00 Christel Baier Mannheim, Allemagne Verification of probabilistic systems: an overview of the temporal logical approach
10 VERIMAG 16:00 Bertrand Jeannet VERIMAG, France Vérification de propriétés numériques par raffinement automatique

Mai, 1999

28 MJK 14:00 Eugène Asarin IPI, Moscow, Russie Systèmes temporisés - résultats et perspectives
28 MJK 16:00 Yassine Lakhnech Kiel, Allemagne Vérification des Systèmes: Synthèse et Perspective
20 MJK 16:00 Anne Mignotte ENS Lyon, France Ordonnancement pour la synthèse de systèmes intégrés
20 VERIMAG 14:00 Vlad Rusu IRISA Rennes, France Symbolic Test Generation and Abstraction

Avril, 1999

29 VERIMAG 14:00 Richard Gerber Maryland, USA Designing real-time systems for end-to-end performance
22 VERIMAG 14:00 Hubert Comon ENS Cachan, France Automates temporisés et théorie des nombres

Mars, 1999

18 VERIMAG 14:00 Laurent El Ghaoui ENSTA, France Robust optimization and applications to reachable set approximations
17-18 VERIMAG VIRES Esprit Project Program

News

Seminars

New publications

Jobs and internships

Contact | Site Map | Site powered by SPIP 4.4.2 + AHUNTSIC [CC License]

info visites 4453184