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

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

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

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

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

Thursday 11 June 2015 | Marek Trtik (VERIMAG) | Abstracting Path Conditions |

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

Thursday 28 May 2015 | Alessia Milani (LaBRI) | An Introduction to Software Transactional Memory |

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

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

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

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

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

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

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

Thursday 18 December 2014 | Denis Kuperberg (IRIT/ONERA) | Cost functions and Value 1 problem in practice |

Thursday 04 December 2014 | Sylvain Schmitz (LSV) | Alternating Vector Addition Systems with States |

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

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

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

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

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

Thursday 19 June 2014 | Thème MV (LaBRI) | Réunion de Thème |

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

Monday 02 June 2014 | Chris Newcombe (Amazon.com) | Why Amazon Chose TLA+ |

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

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

Thursday 13 March 2014 | Sylvain Schmitz (LSV) | The Power of Priority Channel Systems |

Thursday 20 February 2014 | Valentin Perrelle (IRT SystemX) | Static analysis of programs manipulating arrays |

Thursday 13 February 2014 | Emmanuel Fleury (LaBRI) | Binary Analysis: Theory and Practice |

Thursday 06 February 2014 | Philippe Schnoebelen (LSV) | The Power of Well-Structured Systems |

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

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

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

Thursday 12 December 2013 | Ahmed Bouajjani (LIAFA) | Verification of Concurrent Programs: Decidability, Complexity, Reductions |

Thursday 05 December 2013 | Jean-Marie Lagniez (CRIL) | Knowledge Compilation for Model Counting: Afﬁne Decision Trees |

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

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

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

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

Thursday 24 October 2013 | Alain Griffault et Gérald Point (LaBRI) | AltaRica |

Thursday 17 October 2013 | Laurent Simon (LaBRI) | SAT Solvers and Model Checking |

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

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

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

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

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

Thursday 16 May 2013 | Hugues Cassé (IRIT) | Path Analysis in OTAWA Framework |

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

Thursday 04 April 2013 | Aymeric Vincent (LaBRI) | The Insight binary analysis framework |

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

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

Thursday 21 February 2013 | Stefan Göller (Univ. Bremen) | Equivalence Checking of Pushdown Automata and One-Counter Automata |

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

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

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

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

Thursday 20 December 2012 | Antoine Rollet (LaBRI) | Runtime Enforcement of Timed Properties |

Thursday 06 December 2012 | Javier Esparza (TUM, Germany) | A perfect model for bounded verification |

Thursday 06 December 2012 | Jean-Francois Raskin (ULB, Belgium) | Multi-dimension Quantitative Games: Complexity and Strategy Synthesis |

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

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

Thursday 04 October 2012 | Lorenzo Clemente (LaBRI) | Reachability of Communicating Timed Processes |

Thursday 27 September 2012 | Sven Schewe (Liverpool University) | Strategy Synthesis (From Specification to Implementation) |

Thursday 07 June 2012 | M Praveen (LSV) | Parameterized Complexity of some Petri Net Problems |

Thursday 24 May 2012 | Pierre Bourhis () | Querying Schemas With Access Restrictions |

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

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

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

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

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

Thursday 22 March 2012 | Emmanuel Filiot (ULB) | Exploiting Structure in LTL Synthesis |

Thursday 15 March 2012 | Benoît Delahaye () | Compositional Specification Theories for Stochastic Systems |

Thursday 08 March 2012 | Gabriele Puppis (LaBRI) | The Cost of Repairing Regular Specifications |

Thursday 16 February 2012 | Lorenzo Clemente (LaBRI) | Fixed-word simulations and ranks |

Thursday 09 February 2012 | Cezara Dragoi (IST Austria ) | Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data |

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

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

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

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

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

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

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

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

Thursday 03 November 2011 | Anca Muscholl (LaBRI) | Controlling distributed systems |

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

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

Thursday 29 September 2011 | Barbara Jobstmann (Verimag) | Quantitative Verification and Synthesis |

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

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

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

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

Thursday 19 May 2011 | Rohit Chadha (LSV) | Power of Randomization in Finite State Monitoring |

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

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

Thursday 28 April 2011 | Srivathsan Balaguru (LaBRI) | A lazy reachability algorithm for timed automata |

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

Thursday 17 February 2011 | Stefan Schwoon (LSV, Cachan) | Unfoldings of contextual Petri nets |

Thursday 03 February 2011 | Mohamed Faouzi Atig (LIAFA, PARIS) | Global Model Checking of Ordered Multi-Pushdown Systems |

Thursday 16 December 2010 | Laurent Doyen (LSV, Cachan) | Energy and Mean-Payoff Games |

Thursday 09 December 2010 | Ylies Falcone (projet VERTECS/INRIA, Rennes) | What Can You Verify and Enforce at Runtime ? |

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

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

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

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

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

Thursday 16 September 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.