~~NOCACHE~~ ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 693 date: lundi 10 décembre 2018 heure: 11h10 salle: Salle 1007 nom: Mahsa Shirmohammadi affiliation: LIS - CNRS & Université Aix-Marseille titre: On the Complexity of Value Iteration ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 685 date: lundi 03 décembre 2018 heure: 11h10 salle: Salle 1007 nom: Vincent Rahli affiliation: SnT - University of Luxembourg titre: Building Reliable Systems on Reliable Foundations ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 692 date: lundi 26 novembre 2018 heure: 11h10 salle: Salle 1007 nom: Matthias Függer affiliation: LSV - CNRS & ENS de Cachan titre: Fast Asymptotic and Approximate Consensus in Highly Dynamic Networks ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 666 date: lundi 12 novembre 2018 heure: 11h10 salle: Salle 1007 nom: Arvid Jakobsson affiliation: Huawei Research & LIFO -Université d'Orléans titre: Replicated Synchronization of BSPlib Programs ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 697 date: lundi 05 novembre 2018 heure: 11h10 salle: Salle 1007 nom: Adrien Guatto affiliation: IRIF titre: Hierarchical Memory Management for Mutable State ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 684 date: lundi 29 octobre 2018 heure: 11h10 salle: Salle 1007 nom: Éric Tanter affiliation: PLEIAD - Universidad de Chile & INRIA Paris titre: The Essence of Gradual Typing ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 663 date: lundi 22 octobre 2018 heure: 11h10 salle: Salle 1007 nom: Marie Fortin affiliation: LSV - ENS Paris-Saclay titre: It Is Easy to Be Wise After the Event: Communicating Finite-State Machines Capture First-Order Logic with "Happened Before" ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 652 date: lundi 01 octobre 2018 heure: 11h10 salle: Salle 1007 nom: Mahsa Shirmohammadi affiliation: LIS - CNRS & Université Aix-Marseille titre: On Rationality of Nonnegative Matrix Factorization ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 634 date: lundi 24 septembre 2018 heure: 11h10 salle: Salle 1007 nom: Adam Shimi affiliation: IRIT - ENSEEIHT titre: Characterizing Asynchronous Message-Passing Models Through Rounds ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 639 date: lundi 17 septembre 2018 heure: 11h00 salle: Salle 1007 nom: Franz Mayr affiliation: Universidad ORT, Uruguay titre: Regular inference on artificial neural networks ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 626 date: vendredi 29 juin 2018 heure: 11h00 salle: Salle 3052 nom: Mahsa Shirmohammadi affiliation: LIS, CNRS - Univ. Aix-Marseille titre: Costs and Rewards in Priced Timed Automata ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 610 date: lundi 25 juin 2018 heure: 11h00 salle: Salle 3052 nom: Nicolas Jeannerod affiliation: IRIF titre: Deciding the First-Order Theory of an Algebra of Feature Trees with Updates ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 601 date: lundi 18 juin 2018 heure: 11h00 salle: Salle 3052 nom: Eugène Asarin affiliation: IRIF titre: Distance on timed words and applications ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 618 date: mercredi 13 juin 2018 heure: 15h00 salle: Salle 3052 nom: Joël Ouaknine affiliation: MPI-SWS titre: Program Invariants ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 579 date: lundi 11 juin 2018 heure: 11h00 salle: Salle 3052 nom: François Pottier affiliation: INRIA Paris titre: Verifying a Hash Table and Its Iterators in Higher-Order Separation Logic ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 573 date: vendredi 01 juin 2018 heure: 10h30 salle: 3052 nom: Derek Dreyer affiliation: Max Planck Institute for Software Systems (MPI-SWS) titre: RustBelt: Logical Foundations for the Future of Safe Systems Programming ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 451 date: lundi 28 mai 2018 heure: 11h00 salle: Salle 1007 nom: Ana Sokolova affiliation: Universität Salzburg, Austria titre: Linearizability of Concurrent Data Structures via Order Extension Theorems ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 572 date: lundi 14 mai 2018 heure: 11h00 salle: Salle 1007 nom: Raphaël Cauderlier affiliation: IRIF - Université Paris Diderot titre: A Verified Implementation of the Bounded List Container ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 584 date: lundi 07 mai 2018 heure: 11h00 salle: Salle 1007 nom: Adrien Pommellet affiliation: IRIF titre: Static Analysis of Multithreaded Recursive Programs Communicating via Rendez-vous ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 449 date: lundi 09 avril 2018 heure: 11h00 salle: Salle 1007 nom: Ilya Sergey affiliation: University College London, UK titre: Programming and Proving with Distributed Protocols ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 538 date: lundi 26 mars 2018 heure: 11h00 salle: Salle 1007 nom: Ivan Gazeau affiliation: LORIA & INRIA Nancy - Grand Est titre: Automated Verification of Privacy-type Properties for Security Protocols ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 554 date: vendredi 23 mars 2018 heure: 14h30 salle: Salle 3052 nom: Javier Esparza affiliation: Tecnhische Universität München titre: One Theorem to Rule Them All: A Unified Translation of LTL into omega-Automata ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 450 date: lundi 19 mars 2018 heure: 11h00 salle: Salle 1007 nom: Rupak Majumdar affiliation: Max Planck Institute for Software Systems (MPI-SWS) titre: Effective Random Testing for Concurrent and Distributed Programs ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 534 date: lundi 12 mars 2018 heure: 11h00 salle: Salle 1007 nom: Thomas Colcombet affiliation: IRIF & CNRS titre: Automata and Program Analysis ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 521 date: lundi 26 février 2018 heure: 11h00 salle: Salle 1007 nom: Cătălin Hriţcu affiliation: INRIA Paris titre: When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 504 date: lundi 19 février 2018 heure: 11h00 salle: Salle 3052 nom: Adrien Boiret affiliation: University of Warsaw titre: The "Hilbert Method" for Solving Transducer Equivalence Problems. ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 452 date: jeudi 08 février 2018 heure: 10h30 salle: Salle 3052 nom: Vincent Laporte affiliation: IMDEA Software titre: Provably secure compilation of side-channel countermeasures: the case of cryptographic “constant-time” ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 421 date: lundi 29 janvier 2018 heure: 11h00 salle: Salle 1007 nom: Engel Lefaucheaux affiliation: ENS Cachan / IRISA Rennes titre: Probabilistic Disclosure: Maximisation vs. Minimisation ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 420 date: lundi 22 janvier 2018 heure: 11h00 salle: Salle 1007 nom: Josef Widder affiliation: TU Wien titre: Synthesis of Distributed Algorithms with Parameterized Thresholds Guards ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 340 date: lundi 15 janvier 2018 heure: 11h00 salle: Salle 1007 nom: Chao Wang affiliation: IRIF titre: Checking Linearizability of Concurrent Priority Queues ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 367 date: lundi 08 janvier 2018 heure: 11h00 salle: Salle 1007 nom: Jean-Jacques Lévy affiliation: IRIF & INRIA titre: Proofs of graph algorithms with automation and their readability ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 347 date: lundi 11 décembre 2017 heure: 11h00 salle: Salle 1007 nom: Irène Guessarian affiliation: IRIF - Unviersité Paris Diderot titre: Congruence Preservation, Lattices and Recognizability ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 366 date: jeudi 07 décembre 2017 heure: 16h00 salle: Salle 1007 nom: Luke Ong affiliation: University of Oxford titre: Constrained Horn clauses for automatic program verification: the higher-order case ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 365 date: mardi 28 novembre 2017 heure: 13h30 salle: Salle 3052 nom: Léon Gondelman affiliation: Radboud University, The Netherlands titre: The Spirit of Ghost Code ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 339 date: lundi 20 novembre 2017 heure: 11h00 salle: Salle 1007 nom: Laurent Fribourg affiliation: LSV, CNRS & ENS de Cachan titre: Euler’s Method Applied to the Control of Switched Systems ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 335 date: lundi 13 novembre 2017 heure: 11h00 salle: Salle 1007 nom: Viktor Vafeiadis affiliation: Max Planck Institute for Software Systems (MPI-SWS) titre: Effective Stateless Model Checking for C/C++ Concurrency ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 307 date: lundi 30 octobre 2017 heure: 11h00 salle: Salle 1007 nom: Suha Mutluergil affiliation: Koç University titre: Proving linearizability using forward simulations ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 321 date: lundi 23 octobre 2017 heure: 11h00 salle: Salle 1007 nom: Raphaël Cauderlier affiliation: IRIF - Université Paris Diderot titre: FocaLiZe and Dedukti to the Rescue for Proof Interoperability ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 320 date: lundi 16 octobre 2017 heure: 11h00 salle: Salle 1007 nom: Noam Rineztky affiliation: Tel-Aviv University titre: Verifying Equivalence of Spark Programs ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 306 date: lundi 09 octobre 2017 heure: 11h00 salle: Salle 1007 nom: Javier Esparza affiliation: Technische Universität München titre: Polynomial Analysis Algorithms for Free-Choice Workflow Nets ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 305 date: lundi 02 octobre 2017 heure: 11h00 salle: Salle 1007 nom: Ahmed Bouajjani affiliation: IRIF - Université Paris Diderot titre: Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 281 date: mercredi 28 juin 2017 heure: 14h00 salle: Salle 3052 nom: Giuliano Losa affiliation: UCLA titre: Paxos Made EPR --- Decidable Reasoning about Distributed Consensus ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 279 date: jeudi 22 juin 2017 heure: 11h00 salle: Salle 3052 nom: Ruzica Piskac affiliation: Yale University titre: New Applications of Software Synthesis: Verification of Configuration Files and Firewalls Repair ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 273 date: lundi 12 juin 2017 heure: 14h00 salle: Salle 3052 nom: Thomas Wies affiliation: New York University titre: A Simple Framework for Verifying Concurrent Search Structures ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 264 date: mardi 06 juin 2017 heure: 11h00 salle: Salle 3052 nom: Sergio Rajsbaum affiliation: UNAM Mexico titre: Tasks, objects, and the notion of a distributed problem ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 263 date: jeudi 01 juin 2017 heure: 11h00 salle: Salle 3052 nom: Orna Grumberg affiliation: Technion, Israel titre: Sound and Complete Mutation-Based Program Repair ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 262 date: mardi 23 mai 2017 heure: 15h30 salle: Salle 3052 nom: Florian Zuleger affiliation: TU Wien titre: Inductive Termination Proofs by Transition Predicate Abstraction and their relationship to the Size-Change Abstraction ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 258 date: lundi 22 mai 2017 heure: 11h00 salle: Salle 1007 nom: Alain Finkel affiliation: LSV, ENS Cachan titre: The Erdös & Tarski theorem. A new class of WSTS without WQO. ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 230 date: lundi 27 mars 2017 heure: 11h00 salle: Salle 1007 nom: Mohamed Faouzi Atig affiliation: Uppsala University titre: Lossy Channel Systems with Data. ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 227 date: lundi 20 mars 2017 heure: 11h00 salle: Salle 1007 nom: Andreas Podelski affiliation: University of Freiburg titre: Proving Liveness of Parameterized Programs ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 212 date: lundi 13 mars 2017 heure: 11h00 salle: Salle 1007 nom: Ori Lahav affiliation: MPI Kaiserslautern titre: A Promising Semantics for Relaxed-Memory Concurrency ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 211 date: lundi 06 mars 2017 heure: 11h00 salle: Salle 1007 nom: Germán Andrés Delbianco affiliation: IMDEA Madrid titre: Concurrent Data Structures Linked in Time ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 205 date: lundi 27 février 2017 heure: 11h00 salle: Salle 1007 nom: Oded Maler affiliation: CNRS and University of Grenoble-Alpes titre: Monitoring: Qualitative and Quantitative, Real and Virtual, Online and Offline ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 202 date: lundi 20 février 2017 heure: 11h00 salle: Salle 1007 nom: Loig Jezequel affiliation: L2SN - Nantes titre: Lazy Reachability Analysis in Distributed Systems ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 186 date: lundi 23 janvier 2017 heure: 11h00 salle: Salle 1007 nom: Andrea Cerone affiliation: Imperial College London titre: Analysing Snapshot Isolation ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 167 date: lundi 12 décembre 2016 heure: 11h00 salle: Salle 1007 nom: Bin Fang affiliation: IRIF(Paris), ECNU (China) titre: Hierarchical Shape Abstraction for Analysis of Free-List Memory Allocators (a logic-based approach) ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 162 date: vendredi 09 décembre 2016 heure: 11h00 salle: Salle 3052 nom: Alastair Donaldson affiliation: Imperial College London titre: Exposing Errors Related to Weak Memory in GPU Applications ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 157 date: lundi 05 décembre 2016 heure: 11h00 salle: Salle 1007 nom: Guilhem Jaber affiliation: IRIF titre: SyTeCi: Symbolic, Temporal and Circular reasoning for automatic proofs of contextual equivalence ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 155 date: lundi 28 novembre 2016 heure: 11h00 salle: Salle 1007 nom: Georg Zetzsche affiliation: LSV, ENS Cachan titre: First-order logic with reachability for infinite-state systems ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 154 date: jeudi 24 novembre 2016 heure: 15h00 salle: Salle 3052 nom: Gennaro Parlato affiliation: University of Southampton titre: A Pragmatic Bug-finding Approach for Concurrent Programs ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 142 date: lundi 14 novembre 2016 heure: 11h00 salle: Salle 1007 nom: Philipp Rümmer affiliation: University of Uppsala titre: Liveness of Randomised Parameterised Systems under Arbitrary Schedulers ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 120 date: lundi 24 octobre 2016 heure: 11h00 salle: Salle 1007 nom: Sylvain Schmitz affiliation: LSV - ENS Cachan titre: Ideal Decompositions for Vector Addition Systems ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 108 date: lundi 10 octobre 2016 heure: 11h00 salle: Salle 1007 nom: Steven de Oliveira affiliation: CEA titre: Polynomial invariants by linear algebra ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 110 date: lundi 03 octobre 2016 heure: 11h00 salle: Salle 1007 nom: Giovanni Bernardi affiliation: IRIF titre: Robustness against Consistency Models with Atomic Visibility ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 109 date: lundi 26 septembre 2016 heure: 11h00 salle: Salle 1007 nom: Arnaud Sangnier affiliation: IRIF titre: Fixpoints in VASS: Results and Applications ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 106 date: lundi 19 septembre 2016 heure: 11h00 salle: Salle 1007 nom: Francesco Belardinelli affiliation: Université d'Evry titre: Abstraction-based Verification of Infinite-state Data-aware Systems ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 78 date: lundi 30 mai 2016 heure: 11h00 salle: Salle 1007 nom: Thibaut Balabonski affiliation: LRI titre: Low-level C code optimisations: are they valid? ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 399 date: lundi 14 mars 2016 heure: 11h00 salle: Salle 1007 nom: Paul Gastin affiliation: LSV titre: Formal methods for the verification of distributed algorithms ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 398 date: lundi 07 mars 2016 heure: 11h00 salle: Salle 1007 nom: Julien Signoles affiliation: CEA-LIST titre: Frama-C, a collaborative and extensible framework for C code analysis ---- ---- datatemplateentry ---- template: templates:seance classe: seance type: Verification seminaire: verif id: 397 date: lundi 29 février 2016 heure: 11h00 salle: Salle 1007 nom: Pierre Fraigniaud affiliation: IRIF titre: Fault-Tolerant Decentralized Runtime Monitoring ----