Le séminaire MV a été remplacé par le Séminaire de l'équipe Méthodes Formelles.

Date | Orateur | Titre |
---|---|---|

jeudi 10 décembre 2015 | Assalé Adjé (IRIT) | Optimisation sous-contraintes appliquée à l'analyse statique de programmes |

jeudi 24 septembre 2015 | Thanh Tung Tran (LaBRI) | Improving search order for reachability testing in timed automata |

jeudi 25 juin 2015 | Diego Figueira (LaBRI) | Path Logics for Querying Graphs: Combining Expressiveness and Efficiency |

jeudi 11 juin 2015 | Marek Trtik (VERIMAG) | Abstracting Path Conditions |

jeudi 04 juin 2015 | Igor Walukiewicz (LaBRI) | Safety of parametrized asynchronous shared-memory systems is almost always decidable |

jeudi 28 mai 2015 | Alessia Milani (LaBRI) | An Introduction to Software Transactional Memory |

jeudi 21 mai 2015 | Jérôme Leroux (LaBRI) | Ideals And Well Quasi Orders (Part III) |

jeudi 07 mai 2015 | Jérôme Leroux (LaBRI) | Ideals And Well Quasi Orders (Part II) |

jeudi 16 avril 2015 | Jérôme Leroux (LaBRI) | Ideals And Well Quasi Orders (Part I) |

jeudi 02 avril 2015 | Jean-Michel Couvreur (LIFO) | Vérification de propriétés MSO sur les pomsets |

jeudi 19 mars 2015 | Thomas Chatain (LSV) | The subtle alchemy of concurrency and real-time |

jeudi 05 mars 2015 | Benjamin Monmege (ULB) | Reachability in MDPs: Refining Convergence of Value Iteration |

jeudi 22 janvier 2015 | Anca Muscholl (LaBRI) | On the parameterized verification of asynchronous shared-memory systems |

jeudi 18 décembre 2014 | Denis Kuperberg (IRIT/ONERA) | Cost functions and Value 1 problem in practice |

jeudi 04 décembre 2014 | Sylvain Schmitz (LSV) | Alternating Vector Addition Systems with States |

jeudi 27 novembre 2014 | Igor Walukiewicz & Laurent Simon (LaBRI) | IC3: model checking avec SAT, 2ème partie |

jeudi 06 novembre 2014 | Paulin de Naurois (LIPN) | Reachability In Vector Addition with States and Split/Join Transitions |

jeudi 23 octobre 2014 | Igor Walukiewicz & Laurent Simon (LaBRI) | IC3: model checking avec SAT |

jeudi 16 octobre 2014 | Ranko Lazic (Univ. Warwick) | Zeno, Hercules and the Hydra |

jeudi 18 septembre 2014 | Piotr Hofman (Univ. Bayreuth) | Branching bisimulation for normed commutative context free grammars |

jeudi 19 juin 2014 | Thème MV (LaBRI) | Réunion de Thème |

jeudi 05 juin 2014 | Salvatore La Torre (Univ. Salerno) | Sequentialization and Bounded Model-checking |

lundi 02 juin 2014 | Chris Newcombe (Amazon.com) | Why Amazon Chose TLA+ |

jeudi 22 mai 2014 | Salvatore La Torre (Univ. Salerno) | Analysis of Concurrent Programs via Sequentialization |

jeudi 17 avril 2014 | Patrick Totzke (LaBRI) | Monotonicity in One-Counter-Systems: what gives? |

jeudi 13 mars 2014 | Sylvain Schmitz (LSV) | The Power of Priority Channel Systems |

jeudi 20 février 2014 | Valentin Perrelle (IRT SystemX) | Static analysis of programs manipulating arrays |

jeudi 13 février 2014 | Emmanuel Fleury (LaBRI) | Binary Analysis: Theory and Practice |

jeudi 06 février 2014 | Philippe Schnoebelen (LSV) | The Power of Well-Structured Systems |

jeudi 23 janvier 2014 | Yliès Falcone (LIG, Univ. Grenoble 1) | Towards distributed monitoring (of Android applications) |

jeudi 16 janvier 2014 | Mickael Randour (Univ. Mons) | Meet Your Expectations With Guarantees: Beyond Worst-Case Synthesis in Quantitative Games |

jeudi 19 décembre 2013 | Amélie Stainer (ULB, Belgium) | Contribution à la vérification d'automates temporisés: déterminisation et vérification quantitative |

jeudi 12 décembre 2013 | Ahmed Bouajjani (LIAFA) | Verification of Concurrent Programs: Decidability, Complexity, Reductions |

jeudi 05 décembre 2013 | Jean-Marie Lagniez (CRIL) | Knowledge Compilation for Model Counting: Afﬁne Decision Trees |

jeudi 28 novembre 2013 | Thème MV (LaBRI) | [Discussion] Exploitation de la structure dans les modèles |

jeudi 21 novembre 2013 | M. Praveen (LaBRI) | Hyper Ackermannian Bounds for Pushdown Vector Addition Systems |

jeudi 14 novembre 2013 | Patrick Totzke (Univ. Edinburgh) | Inclusion problems for One-Counter Nets |

jeudi 07 novembre 2013 | Salvatore La Torre (Univ. Salerno) | Multistack Pushdown Systems: formal languages theories |

jeudi 24 octobre 2013 | Alain Griffault et Gérald Point (LaBRI) | AltaRica |

jeudi 17 octobre 2013 | Laurent Simon (LaBRI) | SAT Solvers and Model Checking |

jeudi 03 octobre 2013 | Philipp Ruemmer (Univ. Uppsala) | Disjunctive Interpolants for Horn-Clause Verification |

jeudi 20 juin 2013 | Aiswarya Cyriac (LSV) | Split-width technique for the verification of concurrent programs with data structures |

jeudi 13 juin 2013 | Jérôme Leroux (LaBRI) | Acceleration For Presburger Petri Nets |

jeudi 06 juin 2013 | Vincent Penelle (LIGM) | On the Context-freeness Problem for Vector Addition Systems |

jeudi 30 mai 2013 | Elias Tsigaridas (LIP6 ) | Exact algorithms for stochastic games and real algebraic geometry |

jeudi 16 mai 2013 | Hugues Cassé (IRIT) | Path Analysis in OTAWA Framework |

jeudi 25 avril 2013 | Pascal Lafourcade (VERIMAG) | Automatic security proof of cryptographic primitives: public encryption, symmetric encryption modes, MAC |

jeudi 04 avril 2013 | Aymeric Vincent (LaBRI) | The Insight binary analysis framework |

jeudi 28 mars 2013 | Loïg Jezequel (ENS Cachan Bretagne) | Cost-optimal factored planning using weighted automata calculus |

jeudi 07 mars 2013 | Shibashis Guha (IIT Delhi) | A semi-decidable approach for determining language inclusion for timed automata |

jeudi 21 février 2013 | Stefan Göller (Univ. Bremen) | Equivalence Checking of Pushdown Automata and One-Counter Automata |

jeudi 31 janvier 2013 | M. Praveen (LaBRI) | Reasoning about Data Repetitions with Counter Systems |

jeudi 24 janvier 2013 | Radu Iosif (VERIMAG) | Underapproximation of Procedure Summaries for Recursive Integer Programs |

jeudi 17 janvier 2013 | Sven Schewe (Univ. Liverpool) | Beautiful Games You Cannot Stop Playing |

jeudi 10 janvier 2013 | Gilles Geeraerts (ULB, Belgium) | Time-bounded reachability for monotonic hybrid automata |

jeudi 20 décembre 2012 | Antoine Rollet (LaBRI) | Runtime Enforcement of Timed Properties |

jeudi 06 décembre 2012 | Javier Esparza (TUM, Germany) | A perfect model for bounded verification |

jeudi 06 décembre 2012 | Jean-Francois Raskin (ULB, Belgium) | Multi-dimension Quantitative Games: Complexity and Strategy Synthesis |

jeudi 29 novembre 2012 | Grégoire Sutre (LaBRI) | Safety Verification of Communicating One-Counter Machines |

jeudi 08 novembre 2012 | Frédéric Herbreteau (LaBRI) | Coarse abstractions make Zeno behaviors difficult to detect |

jeudi 04 octobre 2012 | Lorenzo Clemente (LaBRI) | Reachability of Communicating Timed Processes |

jeudi 27 septembre 2012 | Sven Schewe (Liverpool University) | Strategy Synthesis (From Specification to Implementation) |

jeudi 07 juin 2012 | M Praveen (LSV) | Parameterized Complexity of some Petri Net Problems |

jeudi 24 mai 2012 | Pierre Bourhis () | Querying Schemas With Access Restrictions |

jeudi 10 mai 2012 | Madhavan Mukund (CMI, India) | Tagging Make Local Testing of Message-Passing Systems Feasible |

jeudi 03 mai 2012 | Michael Emmi (LIAFA, Paris) | Bounded Phase Analysis of Message-Passing Programs |

jeudi 12 avril 2012 | Aiswarya Cyriac (LSV, ENS Cachan) | Model Checking Languages of Data Words |

jeudi 05 avril 2012 | Rémi Bonnet (LSV) | Forward Analysis for WSTS : Beyond Regular Accelerations |

jeudi 29 mars 2012 | Uli Fahrenberg (IRISA, Rennes) | The Quantitative Linear-Time–Branching-Time Spectrum |

jeudi 22 mars 2012 | Emmanuel Filiot (ULB) | Exploiting Structure in LTL Synthesis |

jeudi 15 mars 2012 | Benoît Delahaye () | Compositional Specification Theories for Stochastic Systems |

jeudi 08 mars 2012 | Gabriele Puppis (LaBRI) | The Cost of Repairing Regular Specifications |

jeudi 16 février 2012 | Lorenzo Clemente (LaBRI) | Fixed-word simulations and ranks |

jeudi 09 février 2012 | Cezara Dragoi (IST Austria ) | Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data |

jeudi 26 janvier 2012 | Peter Habermehl (LIAFA, Paris) | Forest Automata for Verification of Heap Manipulation |

jeudi 19 janvier 2012 | Lorenzo Clemente (LaBRI) | Optimizing Buechi Automata Inclusion Checking with Subsumption Preorders |

jeudi 12 janvier 2012 | Ocan Sankur (LSV, ENS Cachan) | Robustness and Implementability of Timed Automata |

jeudi 08 décembre 2011 | André Arnold (LaBRI) () | Propriétés de séparation dans la hiérarchie du mu-calcul sur les arbres (3) |

jeudi 01 décembre 2011 | André Arnold (LaBRI) | Propriétés de séparation dans la hiérarchie du mu-calcul sur les arbres (2) |

jeudi 24 novembre 2011 | André Arnold (LaBRI) | Propriétés de séparation dans la hiérarchie du mu-calcul sur les arbres |

jeudi 17 novembre 2011 | Pierre-Alain Reynier (LIF (Marseille)) | Visibly Pushdown Transducers: Functionality, k-Valuedness and Streamability |

jeudi 10 novembre 2011 | Xavier Blanc (LaBRI) | Vpraxis et évolution d'application internet |

jeudi 03 novembre 2011 | Anca Muscholl (LaBRI) | Controlling distributed systems |

jeudi 13 octobre 2011 | Benjamin Monmege (LSV, ENS Cachan) | Weighted Expressions and Pebble Automata over Nested Words |

jeudi 06 octobre 2011 | Lukasz Kaiser (LIAFA, CNRS) | Model Checking the Quantitative mu-Calculus on Infinite Transition Systems |

jeudi 29 septembre 2011 | Barbara Jobstmann (Verimag) | Quantitative Verification and Synthesis |

jeudi 22 septembre 2011 | Marc Zeitoun (LaBRI) | Model checking vector addition systems with one zero-test |

jeudi 30 juin 2011 | Amélie Stainer (INRIA Rennes) | A game approach to determinize timed automata |

jeudi 23 juin 2011 | Gérald Point (LaBRI) | Génération de séquences de pannes de modèles AltaRica |

jeudi 09 juin 2011 | David Janin (LaBRI) | Vers un modèle de contrôle temps-réels, hiérarchique, concurrent et réactifs |

jeudi 19 mai 2011 | Rohit Chadha (LSV) | Power of Randomization in Finite State Monitoring |

jeudi 12 mai 2011 | Renaud Tabary (LaBRI) | Hybrid syntactic/semantic computer virus detection scheme |

jeudi 05 mai 2011 | Youssouf Oualhadj (LaBRI) | Computing Optimal Strategies for Markov Decision Processes with Parity and Positive-Average Conditions |

jeudi 28 avril 2011 | Srivathsan Balaguru (LaBRI) | A lazy reachability algorithm for timed automata |

jeudi 07 avril 2011 | Régis Gascon (INRIA Sophia Antipolis) | Contraintes sur le temps logique dans la conception de systemes embarques |

jeudi 17 février 2011 | Stefan Schwoon (LSV, Cachan) | Unfoldings of contextual Petri nets |

jeudi 03 février 2011 | Mohamed Faouzi Atig (LIAFA, PARIS) | Global Model Checking of Ordered Multi-Pushdown Systems |

jeudi 16 décembre 2010 | Laurent Doyen (LSV, Cachan) | Energy and Mean-Payoff Games |

jeudi 09 décembre 2010 | Ylies Falcone (projet VERTECS/INRIA, Rennes) | What Can You Verify and Enforce at Runtime ? |

jeudi 02 décembre 2010 | Frédéric Herbreteau (LaBRI) | Efficient Emptiness Check for Timed Büchi Automata |

jeudi 21 octobre 2010 | Michael Ummels (RWTH Aachen) | The complexity of Nash Equilibria in Reward Games |

jeudi 14 octobre 2010 | Ashutosh Trivedi (The University of Warwick, UK) | Expected Reachability-Time Games |

jeudi 07 octobre 2010 | Arshia Cont (IRCAM, centre Pompidou) | Traitement et programmation synchrone des flux musicaux |

jeudi 30 septembre 2010 | Jérôme Leroux (LaBRI) | The Vector Addition System Reachability Problem |

jeudi 16 septembre 2010 | Benedikt Bollig (LSV, Cachan) | Distributed Timed Automata with Independently Evolving Clocks |

- MVTsi 2009-2010.
- MVTsi 2008-2009.
- MVTsi 2007-2008.
- MVTsi 2006-2007.
- MVTsi 2005-2006.
- MVTsi 2004-2005.
- MVTsi 2003-2004.
- MVTsi 2002-2003.
- MVTsi 2001-2002.
- MVTsi 2000-2001.
- MVTsi 1999-2000.
- MVTsi 1998-1999.
- MVTsi 1997-1998.
- MVTsi 1996-1997.
- MVTsi 1995-1996.
- Sémantique du parallélisme 1994-1995.
- Sémantique du parallélisme 1993-1994.
- Sémantique du parallélisme 1992-1993.