Verimag Seminars

If you would like to be informed by email when a VERIMAG seminar is being held, please send an email to Sylvain Boulmé.

To schedule a seminar, Verimag member should fill the online form. Otherwise, please contact Sylvain Boulmé.

 /  ICAL

Upcoming Seminars

• 14 November 2024 - 14h00: Room 206 (2nd floor, badged access)
  by Lisa Maile de TU Braunschweig (Germany) : Real-Time Communication with Dynamic Network Traffic using Time-Sensitive Networking
  
• 21 November 2024 - 14h00: Room 206 (2nd floor, badged access)
  by Chao Huang de School of Electronics & Computer Science Universi : Safe Reinforcement Learning with Verification in the Loss
  
• 28 November 2024 - 14h00: Room 206 (2nd floor, badged access)
  by Grégoire BUSSONE de ENS, équipe Parkas (Inria-ENS) : TBA (Synchronous Language Compilers: Translation Validation and Optimizations)
  
• 2 December 2024 - 14h00: Amphitéatre MJK
  by Thomas Vigouroux de Verimag : Quantitative analysis for adaptive attackers (Thesis)
  
• 12 December 2024 - 14h00: Room 206 (2nd floor, badged access)
  by Lucas Bueri de Verimag : tba (Thesis)
  

Past Seminars

• 7 November 2024 - by Aurèle Barrière de EPFL : Formal Verification Beyond Traditional Compilation
• 27 June 2024 - by Nicolas Chappe de ENS-Lyon, LIP, CASH : Executable semantics based on Choice Trees for a concurrent subset of LLVM IR
• 19 June 2024 - by Jean-François MONIN de Verimag, Polytech Grenoble. : Recent advances on the Braga method
• 18 June 2024 - by Matthieu Sozeau de Inria (Galinette), Université de Nantes : Verified Extraction from Coq to OCaml
• 17 June 2024 - by Sylvain BOULME de Verimag, Grenoble-INP Ensimag : Toward a FFI (Foreign Function Interface) for embedding untrusted imperative OCaml into Coq-verified computations.
• 17 June 2024 - by Basile GROS de Verimag, UGA : Small Inversions in Coq
• 30 May 2024 - by Mohamed Maghenem de CNRS, GIPSA-lab, Grenoble : A Hybrid-Systems Framework for Distributed Gradient-Based Estimation
• 16 May 2024 - by Gaiyun Liu de GREAH : Modeling, analysis, and supervisory control of networked discrete event systems
• 2 May 2024 - by Matthieu Moy de Univ. Lyon 1 - LIP (CASH) : How to Build a Broken System?
• 18 April 2024 - by Akram Idani de LIG (Vasco), Ensimag : Formal Model-Driven Engineering
• 15 April 2024 - by Subhajit Roy de Indian Institute of Technology Kanpur : Satisfiability modulo fuzzing: a synergistic combination of SMT solving and fuzzing
• 11 April 2024 - by Andrei Paskevich de Univ. Paris-Saclay (LMF) - Inria Saclay (Toccata) : Coma: an intermediate verification language with explicit abstraction barriers
• 4 April 2024 - by Sébastien Michelland de LCIS (UGA) : Abstract Interpreters: a Monadic Approach to Modular Verification
• 14 March 2024 - by Adel NOUREDDINE de University of Pau, laboratoire LIUPPA : Observing energy consumption: from hardware to software source code
• 13 March 2024 - by Inigo Incer de CalTech and UC Berkley : Towards Provably Safe and Secure Systems with Contract-Based Design
• 7 March 2024 - by Sylvain Boulmé de Verimag, Grenoble-INP Ensimag : Développement logiciel formellement vérifié: pourquoi et comment ?
• 22 February 2024 - by Paolo Ballarini de CentraleSupélec - MCIS : Hybrid-Automata Specification Language: from expressive stochastic model checking to parametric stochastic model checking
• 12 February 2024 - by Aina Rasoldier de Inria : Comment évaluer le potentiel d'une solution numérique face à l'urgence écologique ? Application aux plateformes de covoiturage régulier à l'échelle locale (Thesis)
• 8 February 2024 - by Sophie Morel de CNRS - ENS-Lyon : Formalisation d'un objet geometrique dans l'assistant de preuve Lean: le cas des grassmanniennes.
• 14 December 2023 - by Alessandro De Palma de INRIA : From Neural Network Verification to Efficient Robust Training
• 12 December 2023 - by Leo Gourdin de VERIMAG : Formal Validation of Intra-Procedural Transformations by Defensive Symbolic Simulation (Thesis)
• 30 November 2023 - by Yutaka Nagashima de Huawei Technologies R&D (UK) : AI-Enhanced Theorem Proving: Tactical Approaches for Induction Problems
• 17 November 2023 - by Thomas Mari de VERIMAG (MOHYTOS), INRIA (SPADES) : Causal explanations for reactive real-time systems (Thesis)
• 9 November 2023 - by Gidon Ernst de Ludwig-Maximilians-University of Munich : Automating software verification with respect to strong specifications
• 19 October 2023 - by Michael Foster de University of Sheffield : Active Inference of Extended Finite State Machines Without Reset
• 12 October 2023 - by Nicola Gigante de Free University of Bozen-Bolzano, Italy : Temporal Logics Modulo Theories for Infinite-State Verification
• 12 July 2023 - by Dejan Nickovic de AIT, Vienna : Attribute Repair for Threat Prevention
• 7 July 2023 - by Akshay Mambakam de VERIMAG, Université Grenoble Alpes : Parametric timed formalisms for specification and monitoring (PhD defense) (Thesis)
• 6 July 2023 - by Nicola Paoletti de King's College London : Causal Temporal Reasoning for Markov Decision Processes
• 30 June 2023 - by Sayan Mitra de University of Illinois Urbana-Champaign : Assuring Safety of Learning-Enabled Systems with Perception Contracts.
• 9 June 2023 - by Jean-Luc Scharbarg de IRIT : Trends in real-time embedded networks: towards TSN
• 9 June 2023 - by claire maiza de GrenobleINP/ Ensimag, Verimag : Hardware and software analyses for precise and efficient timing analysis (HDR)
• 8 June 2023 - by Basile Pesin de Inria PARKAS - ENS-Ulm : Verifying a compiler for a synchronous dataflow language with state machines in Coq
• 25 May 2023 - by Henri-Pierre Charles de CEA, Grenoble : Spécialisation de code binaire au run-time : pour gagner du temps et de l'énergie, il faut rouler à l'HybroGen
• 4 May 2023 - by Joseph Sifakis de VERIMAG : Artificial Intelligence and autonomous systems
• 28 April 2023 - by Thomas Jensen de INRIA : An information flow logic based on partial equivalence relations
• 28 April 2023 - by Etienne Boespflug de Vérimag : Outils pour l’analyse de code et de contre-mesures pour l'injection de fautes multiples (Thesis)
• 9 March 2023 - by Clementine Gritti de University of Canterbury -- New Zealand : Internet of Things: From modern cryptography to post-quantum cryptography
• 6 March 2023 - by Frederic Fort de IRT Saint Exupery : Programing adaptive real-time systems
• 2 March 2023 - by Arthur Perais de TIMA : Exploring Instruction Fusion Opportunities in General Purpose Processors
• 23 February 2023 - by Léo Robert de LIMOS (Université Clermont Auvergne) : How fast do you heal? A taxonomy for post-compromise security in secure-channel establishment.
• 23 February 2023 - by Imen Sayar de IRIT-SM@RT : Collaborative development of safe and secure cyber-physical systems
• 20 February 2023 - by anais durand de univ. clermont auvergne : Exploration of 3D environments by swarms of luminous autonomous robots.
• 6 February 2023 - by Bruno FERRES de LIP (equipe CASH) : Using Model Checking for Electrical Rule Checking of Integrated Circuits at Transistor Level
• 2 February 2023 - by Charlie Jacomme de Team Prosecco of Inria Paris : A comprehensive, formal and automated analysis of the EDHOC protocol.
• 26 January 2023 - by Son Ho de Team Prosecco of Inria Paris : Aeneas: Rust Verification by Functional Translation
• 16 December 2022 - by Vincent Morice de STMicroelectronics : Modèle haut niveau de microcontrôleurs basé sur les dépendances pour le développement de logiciel embarqué (Thesis)
• 13 December 2022 - by Ezio Bertocci de TU Wien : Automatic Invariant Generations for Probabilistic Loops
• 8 December 2022 - by Kohei SUENAGA de Kyoto University : Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption
• 24 November 2022 - by Xavier Denis de LRI : Deductive Verification of Higher-Order Rust Programs
• 24 November 2022 - by Jean-François Monin de VERIMAG : Recursive Programming in Coq and Intensionality : oh happy case !
• 17 November 2022 - by Arnaud Sangnier de IRIF : Parameterized verification of Networks with selective broadcast
• 10 November 2022 - by Stephan Plassart de LCA2 EPFL : Equivalent Versions of Total Flow Analysis
• 27 October 2022 - by Hugo Gimbert de CNRS (LaBRI) : Les algorithmes de ParcourSup
• 29 September 2022 - by Merigoux Denis de INRIA Prosecco : Rules, Computation and Politics: Scrutinizing Unnoticed Programming Choices in French Housing Benefits
• 9 September 2022 - by Lucas Bueri de Verimag : On an Invariance Problem for Parameterized Concurrent Systems
• 12 July 2022 - by Dejan Nickovic de AIT Vienna : Information-flow Interfaces
• 7 July 2022 - by Franz Meyer de Universidad ORT Uruguay : Towards Efficient Active Learning of PDFA
• 21 June 2022 - by Joel Goossens de ULB, Brussels : Real-Time Computing, Multiprocessor scheduling problems
• 16 June 2022 - by Joel Goossens de ULB, Brussels : Periodicity of real-time priority driven schedulers with preemption delay on uniprocessor
• 14 June 2022 - by Joel Goossens de ULB, Brussels : Real-Time Computing, foundation
• 3 June 2022 - by CAPITAL Workshop de sCalable And PrecIse Timing AnaLysis for multicore : Workshop CAPITAL 2022 : sCalable And PrecIse Timing AnaLysis for multicore platforms
• 31 May 2022 - by Matheus Schuh de Verimag / Kalray : Safe Implementation of Hard Real-Time Applications on Many-Core Platforms (Thesis)
• 5 May 2022 - by Nathalie Bertrand de INRIA Rennes : Reconfigurable Parameterized Broadcast Networks: Minimal Size and Execution Length for Coverability
• 7 April 2022 - by Benedikt Bollig de LSV, ENS Saclay : Identifiers in Registers - Describing Network Algorithms with Logic
• 24 March 2022 - by David Monniaux de VERIMAG : The trusted computing base of the CompCert verified compiler
• 10 March 2022 - by Paolo Torrini de Inria Sardes : A CompCert Backend with Symbolic Encryption
• 3 March 2022 - by Xiaowei Huang de University of Liverpool : Machine Learning Safety
• 13 January 2022 - by Benjamin BLANC de Prover Tech : Formal Methods in Practice: Model Checking in the Railway Industry
• 13 December 2021 - by Joseph Sifakis de VERIMAG : Specification and Validation of Autonomous Driving Systems: A Multilevel Semantic Framework
• 7 December 2021 - by Alessio Mansutti de University of Oxford : Efficient complementation of semilinear sets and the VC dimension of Presburger arithmetic
• 3 December 2021 - by Miriam Garci­a de Institute of Science and Technology (IST) of Austr : Design, Verification and Synthesis of Hybrid Systems.
• 2 December 2021 - by Leo Exibard de Reykjavik University : Reactive Synthesis over Infinite Data Domains with Machines with Registers
• 29 November 2021 - by Nicolas Basset de VERIMAG : Uniform Sampling for Networks of Automata
• 23 November 2021 - by PIERRE-LEO BEGAY de Orange Labs & Verimag : Design, Development and certification in Coq/MathComp of Datalog optimizations for network verification (Thesis)
• 4 October 2021 - by Hadi DAYEKH de VERIMAG, UGA : Learning Automata over Large Alphabets as an Alternative to Recurrent Neural Networks
• 27 September 2021 - by Sylvain Boulmé de Verimag : Formally Verified Defensive Programming (efficient Coq-verified computations from untrusted ML oracles) (HDR)
• 20 September 2021 - by Lucas Bueri de VERIMAG : Décidabilité de la rationalité des VAS
• 30 August 2021 - by Yannick Zakowski de LIP : Vellvm semantics
• 13 July 2021 - by Cyril Six de Kalray & Verimag : Optimized and formally-verified compilation for a VLIW processor (Thesis)
• 17 June 2021 - by Pierre Courtieu de CNAM-CEDRIC : [FormalProofs] Dealing with ugly proof environment.
• 10 June 2021 - by Jean-François Monin de Verimag : [FormalProofs] Small inversions and unleashed recursion in Coq, the Braga method
• 23 April 2021 - by Schoitsch Erwin de AIT Austrian Institute of Technology : Ethical aspects and recommendations for trustworthy highly automated/autonomous systems
• 1 April 2021 - by Lionel Rieg de VERIMAG / IIM Grenoble INP : [FormalProofs] A formally-verified compiler from Esterel to circuits
• 11 March 2021 - by David Monniaux de Verimag : [SharedResources] CompCert for Risc-V on FPGA
• 26 February 2021 - by Emma AHRENS de Verimag, Mohytos : Local Reasoning for Reconfigurable Distributed Systems
• 25 February 2021 - by Cyril SIX de Kalray / Verimag : Certified Superblock Scheduling for the CompCert Compiler
• 11 February 2021 - by Franck POMMEREAU de University of Évry : Formal Modelling and Symbolic Analysis of Ecosystems
• 28 January 2021 - by Etienne André de Université de Lorraine : Symbolic Monitoring against Specifications Parametric in Time and Data
• 21 January 2021 - by Etienne Andre de Université de Lorraine : Symbolic Monitoring against Specifications Parametric in Time and Data
• 14 January 2021 - by Olivier RIDOUX de IRISA, Université de Rennes I : Landauer limit and reversible calculus: an introduction
• 18 December 2020 - by Guo Xiaojie de INRIA/VERIMAG : Certified Tools for Schedulability Analyses (Thesis)
• 17 December 2020 - by Stéphane Devismes de UGA/VERIMAG : Versatility and Efficiency in Self-Stabilizing Distributed Systems (HDR)
• 11 December 2020 - by Marius Bozga de VERIMAG : Compositional Generation of Invariants for Timed Systems
• 3 December 2020 - by Jacques Combaz de CNRS / VERIMAG / ETiCS : Introduction aux effets rebond [lien visio: https://veri-bbb.imag.fr/b/jac-lxa-inn-hnq]
• 20 November 2020 - by Radu Iosif de VERIMAG/CNRS : Structural Invariants for the Verification of Systems with (Recursively Defined) Parameterized Architectures
• 19 November 2020 - by Aina Rasoldier de INRIA / Spades - VERIMAG / ETiCS : Les méthodologies d'évaluation des impacts environnementaux des technologies de l'information et de la communication (TIC) à l'échelle mondiale
• 17 November 2020 - by Schuh Matheus de Kalray/Verimag : A study of predictable execution models implementation for industrial data-flow applicationson a multi-core platform with shared banked memory
• 6 November 2020 - by Akshay Mambakam de VERIMAG : Learning Specifications for Labelled Patterns
• 22 October 2020 - by Cyril Six de Kalray - Verimag : Certified and Efficient Instruction Scheduling. Application to Interlocked VLIW Processors.
• 30 June 2020 - by Sébastien Michelland de ENS de Lyon : A Decision Procedure for Equivalence Relations
• 12 March 2020 - by Mathias RAMPARISON de University of Luxemburg : Updatable Parametric Timed Automata: Decidability, Algorithms, and Application to Security
• 9 March 2020 - by Rémy Boutonnet de VERIMAG : Modular Analysis of Numerical Properties by Abstract Interpretation (Thesis)
• 21 February 2020 - by Michael Marcozzi de Imperial College (London) : Compiler Fuzzing: How Much Does It Matter?
• 13 February 2020 - by Jonathan Salwan de Quarkslab : L'exécution symbolique pour l'aide à la rétro-ingénierie dans un cadre industriel (Thesis)
• 12 February 2020 - by Sébastien Bardin de CEA-LIST : From Safety to Security: The Case of Binary-level Code Analysis
• 6 February 2020 - by Jules Chouquet de IRIF : Lower bounds for probabilistic k-set agreement through combinatorial topology
• 3 February 2020 - by Matthieu Jan and Asavoae Mihail de CEA : Towards Automatic Extraction of Timing models from HDL designs (Mihail Asavoae) - Tracking timing anomalies (Matthieu Jan)
• 27 January 2020 - by Xiao XU de VERIMAG : Thesis Defence - Xiao XU - Generalisation of Alternating Automata over Infinite Alphabets (Thesis)
• 27 January 2020 - by Margus Veanes de Microsoft Research Lab : Symbolic Regexes & Matching
• 19 December 2019 - by Yannick Zakowski de University of Pennsylvania : From representing recursive and impure programs in Coq to a modular formal semantics of LLVM IR
• 19 December 2019 - by Hang Yu de VERIMAG : Towards an Efficient Parallel Parametric Linear Programming Solver (Thesis)
• 25 November 2019 - by Moshe Vardi de Rice University : Technology is Driving the Future, But Who Is Steering?
• 21 November 2019 - by Sophie Tourret de Max-Planck-Institut für Informatik, Saarbrücken : Stronger Higher-order Automation
• 10 October 2019 - by Jan Reineke de Universität des Saarlandes : Spectector: Principled detection of speculative information flows
• 8 October 2019 - by Valentin TOUZEAU de Verimag : Static Analysis of Least Recently Used Caches: Complexity, Optimal Analysis, and Applications to Worst-Case Execution Time and Security (Thesis)
• 26 September 2019 - by Pierre-Jean Meyer de University of California, Berkeley : Reachability analysis and decompositions for abstraction-based control synthesis
• 20 September 2019 - by -- Oded Maler Memorial Day de Organized by VERIMAG : Oded Maler Memorial Day
• 19 September 2019 - by Martin Franzle de Carl von Ossietzky Universitat Oldenburg, Germany : What’s to Come is Still Unsure: Automatically Synthesizing and Verifying Controllers Resilient to Delayed Interaction
• 11 July 2019 - by Eric Gascard de SCOP, Polytech Grenoble : Quantitative Analysis of Dynamic Fault Trees by means of Monte Carlo Simulations: Event-Driven Simulation Approach
• 9 July 2019 - by Lionel Rieg de VERIMAG : Integrating Formal Schedulability Analysis into a Verifed OS Kernel
• 4 July 2019 - by Radu IOSIF de VERIMAG : Alternating Automata Modulo First Order Theories
• 2 July 2019 - by Indranil Saha de IIT Kanpur, India : Developing Autonomous Multi-Robot Systems for Complex Missions
• 28 June 2019 - by Braham Lotfi Mediouni de Verimag (RSD) : Modeling and Analysis of Stochastic Real-Time Systems (Thesis)
• 26 June 2019 - by Rany Kahil de Verimag, Université Grenoble Alpes : Schedulability in Mixed- criticality Systems (Thesis)
• 25 June 2019 - by Hernan Ponce de Leon de Fortiss, Munich, Germany : BMC with Weak Memory Models
• 14 June 2019 - by Benoit Barbot de LACL, Universite Paris Est, Creteil : Cosmos a quantitative verification tool for large stochastic systems
• 13 June 2019 - by Simon IOSTI de Verimag : Using neural networks to improve performances of correct-by-construction controllers
• 9 May 2019 - by Saddek Bensalem de Verimag : Engineering Trustworthy Learning-Enabled Autonomous Systems
• 2 May 2019 - by Michael PERIN de Verimag / UGA : Découvrir AMC en 45 Questions a Choix Multiples
• 29 April 2019 - by Invited Speakers de Onera, Kalray, INRIA, Verimag ... : Journée thématique Verimag : Many-core Kalray MPPA, implementation and verification
• 5 April 2019 - by Radu IOSIF de VERIMAG : On the Expressive Completeness and Complexity of Prenex Separation Logic
• 4 April 2019 - by Radu IOSIF de VERIMAG : Checking Deadlock-Freedom of Parametric Component-Based Systems
• 1 April 2019 - by Edward A. Lee de UC Berkeley : Living Digital Beings
• 28 March 2019 - by Olivier VIDAL de ISTerre, Universite Grenoble-Alpes : Matières premières et énergie à l’échelle mondiale dans le contexte de la transition énergétique
• 20 March 2019 - by Rim El Ballouli de Universite Grenoble Alpes : Modeling Self-configuration in Architecture-based Self-adaptive systems (Thesis)
• 8 March 2019 - by Mathias Bourgoin de Nomadic Labs : An overview of the Tezos blockchain
• 22 February 2019 - by Moustapha Lo de Verimag : Implementing a Real-time Avionic application on a Manycore Processor (Thesis)
• 18 February 2019 - by Guillaume Baudart de IBM T. J. Watson Research Center, Yorktown Heights : Probabilistic Reactive Programming
• 14 February 2019 - by Nikos Gorogiannis de Facebook : Concurrency bug detection at scale with Infer
• 7 February 2019 - by Jacques COMBAZ de CNRS, Verimag : Assembling Components in BIP
• 25 January 2019 - by Tom Yamaguchi de TOYOTA : Application of Abstract Interpretation to the Automotive Electronic Control System
• 24 January 2019 - by Maiza Claire de VERIMAG : WCET and interference analysis for multicore systems
• 22 January 2019 - by Georg Struth de University of Sheffield : Verifying Hybrid Systems with Modal Kleene Algebra
• 21 January 2019 - by Sergio Yovine de Universidad ORT Uruguay : Formal specification and implementation of an automated pattern-based parallel-code generation framework
• 18 January 2019 - by Chi-Hong Cheng de Fortiss : When neural networks meet dependability
• 17 January 2019 - by Paolo Torrini de Verimag / PACSS : Reifying and translating a monadic fragment of Gallina
• 8 January 2019 - by Michal Valko de SequeL, Inria Lille - Nord Europe : The power of graphs in speeding up online learning and decision making
• 7 January 2019 - by Michal Valko de SequeL, Inria Lille - Nord Europe : A simple parameter-free and adaptive approach to optimization under a minimal local smoothness assumption
• 19 December 2018 - by Khalil Ghorbal de INRIA : Simulating and Verifying Cyber-Physical Systems: Current Challenges and Novel Research Directions
• 17 December 2018 - by NIKOLAOS KEKATOS de Verimag Laboratory, University of Grenoble Alpes : Formal Verification of Cyber-Physical Systems in the Industrial Model-Based Design Process (Thesis)
• 11 December 2018 - by Bibek Kabi de LIX : Combining Zonotope Abstraction and Constraint Programming for Synthesizing Inductive Invariants
• 6 December 2018 - by Joseph Sifakis de Verimag : On the Nature of Autonomy: A Rigorous Architectural Characterization
• 29 November 2018 - by Sylvain Boulmé de Verimag : Importation d'oracles ML impératifs dans du code Coq vérifié
• 22 November 2018 - by analyse et verif. legeres Une journee de reflexion de 5 exposes 10h - 16h30 : Lightweight analysis and verification techniques
• 16 November 2018 - by Amaury Graillat de VERIMAG/KALRAY : Parallel Code Generation of Synchronous Programs for a Many-core Architecture (Thesis)
• 31 October 2018 - by Mahieddine DELLABANI de Verimag : Formal Methods for Distributed Real-Time Systems (Thesis)
• 23 October 2018 - by Thusitha Asela Bandara de Verimag : An Adaptive Charge Protocol for Lithium-lon Batteries
• 11 October 2018 - by Florent Chevrou de IRIT : Formalisation of Asynchronous Interactions
• 4 October 2018 - by Erwan Jahier de verimag : [Technical Seminar] A gentle introduction to Gitlab-CI and docker
• 20 September 2018 - by Cyril Six de Kalray & Verimag : Extending the CompCert certified compiler for a VLIW processor of Kalray
• 13 September 2018 - by Franz Mayr de Universidad ORT Uruguay : Regular inference on artificial neural networks
• 25 June 2018 - by Stefano Berardi de University of Torino : Martin-Lof's Inductive Definitions Are Not Equivalent to Cyclic Proofs
• 22 June 2018 - by Pallab Dasgupta de IIT Kharagpur : Verification challenges in the Power Management fabric of Integrated Circuits
• 31 May 2018 - by Cristina Serban de VERIMAG, Université Grenoble Alpes : Automated Reasoning in Separation Logic with Inductive Definitions (Thesis)
• 17 May 2018 - by Michael PERIN de VERIMAG / Université Grenoble-Alpes : Automatic Grading: take a CEGAR and let the machine do your work
• 16 May 2018 - by Arvind Adimoolam de VERIMAG : A Calculus of Complex Zonotopes for Computing Invariants of Affine Hybrid Systems (Thesis)
• 15 May 2018 - by Luc Jaulin de Lab-STICC, ENSTA-Bretagne : Computing inner and outer approximations of forward reach sets of a nonlinear dynamical system
• 7 May 2018 - by Alexandre Rocca de Verimag : Formal methods for modelling and validation of biological models (Thesis)
• 17 April 2018 - by Jim Kapinski de TEMA Toyota, USA : Verification of Learning-Enabled, Cyber-Physical Systems
• 12 April 2018 - by Maria Méndez Real de ATER IETR Nantes - équipe SYSCOM : Cache-based attacks and spatial isolation countermeasure on multi and many-core architectures
• 22 March 2018 - by Guilhem Jaber de ENS Lyon/LIP Plume : Model-checking contextual equivalence of higher-order programs with references (candidat poste MCF)
• 22 March 2018 - by Anastasia Volkova de LIP, ENS de Lyon : Towards reliable implementation of digital filters. How digital signal processing and computer arithmetic meet (candidate poste MCF)
• 19 March 2018 - by Benjamin Farinier de CEA_LIST-SaClay : Model Generation for Quantified Formulas: A Taint-Based Approach
• 15 March 2018 - by Ayoub Nouri de VERIMAG : ASTROLABE: A Rigorous Approach for System-Level Performance Modeling and Analysis (candidat poste MCF)
• 15 March 2018 - by Lionel Rieg de Yale University : Extending a verified OS kernel for real-time
• 8 March 2018 - by Ivan Gazeau de LORIA, Nancy : Automated verification of privacy-type properties for security protocols (MCF Candidate)
• 15 February 2018 - by Gheorghe Stefanescu de University of Bucharest : Adaptive systems made by self-assembling heterogeneous components within regular 2D patterns
• 5 February 2018 - by Maxime Puys de Verimag : Cybersecurity of Industrial Systems: Applicative Filtering and Generation of Attack Scenarios (Thesis)
• 18 January 2018 - by David Monniaux de CNRS / VERIMAG : SPECTRE + MELTDOWN
• 15 January 2018 - by Dogan Ulus de Verimag / UGA : Pattern Matching with Time: Theory and Applications (Thesis)
• 21 December 2017 - by Mirco Giacobbe de IST Austria : Counterexample-guided Refinement of Template Polyhedra
• 11 December 2017 - by Denis Becker de Verimag / STMicroelectronics : Parallel SystemC/TLM Simulation of Hardware Components Described for High-Level Synthesis (Thesis)
• 11 December 2017 - by Alexandre Maréchal de Verimag : New Algorithmics for Polyhedral Calculus via Parametric Linear Programming (Thesis)
• 7 December 2017 - by De Oliviera Steven de CEA-List/Verimag : Synthesizing Invariants by Solving Solvable Loops
• 1 December 2017 - by Reineke Jan de Saarland University : On the Smoothness of Paging Algorithms
• 1 December 2017 - by Hamza RIHANI de Univ. Grenoble Alpes / Verimag : Many-Core Timing Analysis of Real-Time Systems and its Application to an Industrial Processor (Thesis)
• 23 November 2017 - by Joseph Sifakis de VERIMAG : How Much Hard is System Design?
• 20 October 2017 - by Franck De Goer de LIG/VASCO et VERIMAG/PACSS : Reverse Engineering binary code in one execution - A lightweight function based dynamic execution. (Thesis)
• 19 October 2017 - by de : COQ en STOCK
• 10 October 2017 - by Irini Eleftheria Mens de Verimag, Université Grenoble Alpes : Learning Regular Languages over Large Alphabets (Thesis)
• 10 October 2017 - by Frits Vaandrager de Radboud University, Netherlands : Learning Mealy Machines with Timers
• 28 September 2017 - by Adrien Guatto de Inria : A Functional Language with Time Warps
• 14 September 2017 - by Joël Goossens de Université libre de Bruxelles : Feasibility & Simulation Intervals of Schedules for Recurrent Real-Time Tasks
• 1 September 2017 - by Anaïs Durand de Verimag : Efficient Distributed Algorithms Suited for Uncertain Context (Thesis)
• 31 August 2017 - by : Workshop ESTATE/VERIMAG Distributed Algorithms
• 12 July 2017 - by Manuel Barragan de TIMA : Feature selection and design for machine learning-based test of analog, mixed-signal and RF circuits
• 26 June 2017 - by Hosein Nazarpour de Verimag : Monitoring Multi-Threaded and Distributed (Component-Based) Systems (Thesis)
• 8 June 2017 - by Assalé ADJE de Université de Perpignan : Itérations sur les politiques pour la vérification de systèmes dynamiques en temps discret.
• 6 June 2017 - by Laurent Lemke de UGA : Modèles partagés et infrastructure ouverte pour l’internet des objets de la ville intelligente (Thesis)
• 10 May 2017 - by Yuliia Romenska de Univ. Grenoble Alpes : High-Level Component-Based Models for Functional Verification of Systems-on-a-Chip (Thesis)
• 20 April 2017 - by Vincent Penelle de Universite de Varsovie : On the context-freeness problem for vector addition systems. (candidat MCF)
• 19 April 2017 - by Liliana Andrade de Verimag : High Level Modeling and Simulation of Heterogeneous Systems: A focus on the SystemC-AMS Synchronization Problem
• 11 April 2017 - by Iulia Dragomir de Verimag : Compositional Design and Analysis of Embedded Systems
• 30 March 2017 - by Helmut Seidl de Technische Universitaet Muenchen : Enforcing Termination of Interprocedural Analysis
• 30 March 2017 - by Dirk Beyer de Ludwig-Maximilians-Universitaet Muenchen : Correctness Witnesses: Exchanging Verification Results between Verifiers
• 29 March 2017 - by Josselin FEIST de VERIMAG / PACSS : Finding the Needle in the Heap: Combining Binary Analysis Techniques to Trigger Use-After-Free (Thesis)
• 29 March 2017 - by Egor Karpenkov de VERIMAG : Finding Inductive Invariants using SMT Solving and Convex Optimization (Thesis)
• 28 March 2017 - by Nikolaj Bjorner de Microsoft Research : Network Verification for Microsoft Azure
• 23 March 2017 - by Romaric Ludinard de ENSAI : Bitcoin, its blockchain and the double spending problem : Bitcoin in a nutshell and safety analysis of recent improvement proposals
• 23 March 2017 - by Hugues Evrard de Imperial College, London : Automated generation of a distributed implementation from a formal model of concurrent processes interacting via multiway rendezvous.
• 16 March 2017 - by Manuel Selva de Inria : Efficient execution on multi-core systems
• 9 March 2017 - by Arthur Milchior de Université Paris Diderot IRIF : Deterministic Automaton and logically definable sets of numbers.
• 9 March 2017 - by Lionel Rieg de Yale university, Flint group : Formal Proofs of Safety in Coq: Mobile Robot Networks and Lustre Compilation
• 2 March 2017 - by Loïc Correnson de CEA - Equipe LIST : « From Frama-C to Lustre »
• 2 March 2017 - by Nicolas Basset de Université Libre de Bruxelles : Uniform Sampling for Timed Automata with Application to Language Inclusion Measurement
• 2 March 2017 - by Paulin Fournier de LABRI, Bordeaux : Verification of infinite probabilistic systems
• 16 February 2017 - by Mastrolilli Monaldo de IDSIA Lugano : High Degree Sum of Squares Proofs/Hierarchy for 0/1 Problems
• 16 February 2017 - by Naor Seffi de Technion Haifa : Multi-label Classification with Pairwise Relations
• 16 February 2017 - by Abhinav Srivastav de Verimag : Trade-offs in Resource Allocation Problems (Thesis)
• 9 February 2017 - by de : Second Year PhD Students Seminars - week 2/2
• 2 February 2017 - by de : Second Year PhD Students Seminars - week 1/2
• 5 December 2016 - by Paul FEAUTRIER de LIP, Ecole Normale Supérieure de Lyon : New Architectures, New Compilation Problems
• 17 November 2016 - by Robin David de CEA LIST : Formal Approaches for Automatic Deobfuscation and Reverse-engineering of Protected Codes
• 7 November 2016 - by Najah BEN SAID de Verimag, Grenoble Alpes University : Information Flow Security in Component Based Models: From Verification to Implementation (Thesis)
• 4 November 2016 - by Souha Ben Rayana de Verimag, Grenoble Alpes University : Compositional Verification of Component-Based Real-time Systems and Applications. (Thesis)
• 2 November 2016 - by Nikos Gorogiannis de University of Middlesex : Biabduction (and Related Problems) in Array Separation Logic
• 28 October 2016 - by J. Esparza, A. Bouajjani, and D. Nickovic de TU Munich, IRIF, Austrian IT : Verification: Theory and Practice
• 28 October 2016 - by Thomas FERRERE de Verimag : Assertion and Measurements for Mixed-Signal Simulation (Thesis)
• 27 October 2016 - by Joseph Sifakis de VERIMAG : Modeling architectures and their properties in BIP
• 13 October 2016 - by Ismail Oukid de SAP : Storage Class Memory (aka NVRAM): Challenges and Opportunities
• 12 October 2016 - by Louis Dureuil de Vérimag-CEA : Analyse de code et processus d’évaluation des composants sécurisés contre l’injection de faute (Thesis)
• 6 October 2016 - by Cristina SERBAN de VERIMAG : A Decision Procedure for Separation Logic in SMT
• 29 September 2016 - by Andreas Podelski de University of Freiburg : Thread Modularity on the Next Level
• 29 September 2016 - by Joel Ouaknine de Max Planck Institute and Oxford University : Decision Problems for Linear Dynamical Systems
• 29 September 2016 - by Parosh Abdulla de Uppsala University : Automatic Verification of Linearization Policies
• 29 September 2016 - by Radu Iosif de VERIMAG : Automata and Logics for Program Verification (HDR)
• 5 July 2016 - by Rahul Mangaram de University of Pennsylvania : Challenges with Medical Cyber-Physical Systems
• 5 July 2016 - by Jyo Deshmukh de TEMA Toyota, Los Angeles : Recent progress on formal methods for CPS
• 30 June 2016 - by Sergiy Bogomolov de IST Austria : Scalable Static Hybridization Methods for Analysis of Nonlinear Systems
• 22 June 2016 - by Heiko FALK de Hamburg University of Technology (TUHH) : WCET-Aware Compilation and Optimization for Real-Time Systems
• 16 June 2016 - by Jan Lanik de VERIMAG : Power reduction in sequential circuits (Thesis)
• 26 May 2016 - by Frehse Goran de VERIMAG : Scalable Verification of Hybrid Systems (HDR)
• 12 May 2016 - by Bruno Grenet de LIRMM, Université de Montpellier : Factorisation de polynômes lacunaires
• 28 April 2016 - by Camille Coti de Université Paris XIII / LIPN : Parallel, distributed behavioral cartography of parametric timed automata
• 24 March 2016 - by Amaury Pouly de Oxford University, Dept. of Computer Science : Solvability of Matrix-Exponential Equations
• 9 March 2016 - by Dario Socci de Verimag : Scheduling of Certifiable Mixed-Criticality Systems (Thesis)
• 9 March 2016 - by Luca Santinelli de ONERA (French Aerospace Lab) : Mixed-Criticalities and Probabilities
• 9 March 2016 - by Sanjoy Baruah de University of North Carolina at Chapel Hill. : Mixed-criticality Scheduling on Multiprocessors
• 9 March 2016 - by Alan Burns de University of York : Mixed Criticality - A Personal View
• 2 March 2016 - by Alexey Bakhirkin de University of Leicester : Towards finding non-terminating behaviours in programs
• 1 March 2016 - by Arnaud Sangnier de LIAFA PARIS 7 : On the Complexity of Verifying Regular Properties on Flat Counter Systems
• 4 February 2016 - by de Verimag : PhD Seminars
• 29 January 2016 - by Mathilde Duclos de Université Grenoble-Alpes : Methods for cryptographic protocol verification in the computational model (Thesis)
• 28 January 2016 - by de Verimag : PhD Seminars
• 7 January 2016 - by de Verimag : Phd Seminars
• 10 December 2015 - by Alexios Lekidis de Verimag/DCS : Design flow for the rigorous development of networked embedded systems (Thesis)
• 10 December 2015 - by PEKTAŞ Abdurrahman de TUBITAK : Behavior based malware classification using online machine learning (Thesis)
• 16 October 2015 - by Enea Zaffanella de Università degli Studi di Parma : A Few Notes on the Implementation of Convex Polyhedra Using the Double Description Framework
• 15 October 2015 - by Alexis Fouilhe de Verimag : Revisiting the abstract domain of polyhedra: constraints-only representation and formal proof (Thesis)
• 15 October 2015 - by Andy King de University of Kent : The Ying and the Yang of Binary Reversing
• 14 October 2015 - by Chantal Keller de Université Paris Sud : F*: Higher-Order Effectful Program Verification
• 18 September 2015 - by Ali Kassem de Verimag : Automated Verification of Exam, Cash, Reputation, and Routing Protocols (Thesis)
• 10 September 2015 - by Julien Signoles Nikolai Kosmatov de CEA6LIST : Combinations of Static and Dynamic Analyses in Frama-C: An Overview
• 3 September 2015 - by Amaury Pouly de LIX (Polytechnique) : On the complexity of some continuous space reachability problems
• 2 July 2015 - by Christos H. Papadimitriou de UC Berkeley : Life under the Lens
• 25 June 2015 - by Pablo Buiras de Chalmers University of Technology (Sweden) : Mixing Static and Dynamic Typing for Information-Flow Control in Haskell
• 11 June 2015 - by Chris Myers de University of Utah : LEMA: A Tool for the Formal Verification of Digitally-Intensive Analog/Mixed-Signal Circuits
• 9 June 2015 - by Ahlem TRIKI de Verimag : Implémentations Distributés des Systems Temps-réel à base de Composants (Thesis)
• 28 May 2015 - by Andrew Reynolds de EPFL Lausanne : Using CVC4 for Proofs by Induction in SMT
• 8 April 2015 - by Ayoub Nouri de Verimag : Rigorous System-level Modeling and Performance Evaluation for Embedded System Design (Thesis)
• 3 April 2015 - by Damien Pous de ENS de Lyon : Algorithms for language equivalence of finite automata
• 19 February 2015 - by Seminaires doctorants 3 de Verimag : Verimag PhD seminars 3
• 12 February 2015 - by Seminaires doctorants 2 de Verimag : Verimag PhD seminars 2
• 5 February 2015 - by Seminaires doctorants 1 de Verimag : Verimag PhD seminars 1
• 29 January 2015 - by Jim Kapinski de TEMA Toyota Technical Center in Los Angeles : Applying V&V technologies to automotive engine control: challenges and directions
• 15 January 2015 - by Alexandre Marechal de Verimag PhD student : A new Linearization Technique for Multivariate Polynomials Using Convex Polyhedra Based on Handelman-Krivine's Theorem
• 10 December 2014 - by Cristina Serban de VERIMAG : An Introduction to Separation Logic
• 21 November 2014 - by Chih-Hong Cheng de ABB Germany : G4LTL-ST - Automatic Generation of PLC programs
• 13 November 2014 - by Victor Magron de Imperial College : New applications of moment-SOS hierarchies
• 7 November 2014 - by Jean-Baptiste Jeannin de Carnegie Mellon University : Differential Temporal Dynamic Logic for Hybrid Systems and Airplane Collision Avoidance
• 15 October 2014 - by Andreas Podelski de University of Freiburg : Proof Spaces for Unbounded Parallelism
• 14 October 2014 - by Andreas Podelski de University of Freiburg : Static Analysis Modulo Theory
• 13 October 2014 - by Julien Henry de Université de Grenoble : Static Analysis by Abstract Interpretation and Decision Procedures (Thesis)
• 13 October 2014 - by Pranav TENDULKAR de Verimag : Mapping and Scheduling on Multi-core Processors using SMT Solvers (Thesis)
• 9 October 2014 - by Kim Quyên Lý de LIAMA, VERIMAG : Automated verification of termination certificates (Thesis)
• 3 October 2014 - by Raphaël Jamet de Verimag : Protocols and Models for the Security of Wireless Ad Hoc Networks (Thesis)
• 12 September 2014 - by Jean-Marc Vincent de LIG : A Spatiotemporal Data Aggregation Technique for the Macroscopic Analysis of Large-scale Systems
• 28 May 2014 - by Dejan Nickovic de Austrian Institute of Technology : Require, Test and Trace It
• 28 April 2014 - by Christian VON ESSEN de Verimag/UJF : Quantitative verification and synthesis (Thesis)
• 14 April 2014 - by Kees Goossens de TUE : CompSOC: A Mixed-Criticality Platform, Formalism, and Design Flow
• 3 April 2014 - by Florian Brandner de ENSTA-ParisTech : Refinement of Worst-Case Execution Time Bounds by Graph Pruning
• 3 April 2014 - by Jan Reineke de Universität des Saarlandes : PRET DRAM controller: bank privatization for predictability and temporal isolation
• 13 March 2014 - by Matthieu Moy de Verimag : High-level Models for Embedded Systems (HDR)
• 27 February 2014 - by Eugene Asarin de LIAFA : Toward a Timed Theory of Channel Coding
• 14 February 2014 - by Franck Cassez de NICTA, Sydney, Australie : A compositional approach to inter-procedural analysis
• 7 February 2014 - by Victor Magron de LAAS : Formal Certificates for Nonlinear Inequalities
• 6 February 2014 - by Najah Ben Said de Verimag : Information Flow Security in Component-Based Systems.
• 6 February 2014 - by Ali Kassem de Verimag : Formal Security Analysis for Routing Protocols and E-exams
• 30 January 2014 - by Abhinav Srivastav de Verimag : Multi-objective scheduling for multi-core systems
• 23 January 2014 - by Alexios Lekidis de Verimag : Model-based design in sensor network systems
• 23 January 2014 - by Souha Ben Rayana de Verimag : Compositional Verification of Component- Based Real-time Systems and Applications
• 23 January 2014 - by Alexis Fouilhe de Verimag : Verifying numerical static analysis results with a proof assistant
• 16 January 2014 - by Ozgun Pinarer de Verimag : Estimation of energy consumption of embedded system network
• 16 January 2014 - by Irini-Eleftheria Mens de Verimag : Learning Regular Languages over Large Alphabets
• 16 January 2014 - by Jan Lanik de Verimag : Switching reduction in sequential circuits
• 7 January 2014 - by Corneliu Popeea de Technische Universitaet Muenchen : Automated verification of multi-threaded programs
• 12 December 2013 - by Yvan Rivierre de VERIMAG : Self-Stabilizing Algorithms for Constructing Distributed Spanning Structures (Thesis)
• 9 December 2013 - by Giuseppe Lipari de LSV et Scuola Superiore Sant'Anna, Pisa : Hierarchical scheduling and component-based analysis of real-time systems
• 25 November 2013 - by Jannik Dreier de VERIMAG : Formal Verification of Voting and Auction Protocols: From Privacy to Fairness and Verifiability (Thesis)
• 25 November 2013 - by Mahfuza Farooque de École polytechnique : A Bisimulation between DPLL(T) and a Proof-Search Strategy for the Focused Sequent Calculus
• 31 October 2013 - by Mirko Fiacchini de GIPSA-lab, Grenoble : Set-theory and invariance for complex systems
• 26 September 2013 - by Garnacho Manuel de IRIT : A Mechanized Semantic Framework for Real-Time Systems
• 16 September 2013 - by Jean Quilbeuf de Verimag : Distributed Implementations of Component-based Systems with Prioritized Multiparty Interactions. Application to the BIP Framework. (Thesis)
• 18 July 2013 - by Gaël Thomas de Paris VI / LIP6 : A Study of the Scalability of Stop-the-world Garbage Collectors on Multicores
• 11 July 2013 - by Sriram Sankaranarayanan de University of Colorado at Boulder : Invariance and Termination for Probabilistic Programs using Martingales.
• 10 July 2013 - by Xiaomu Shi de VERIMAG UJF : Certification of an Instruction Set Simulator (Thesis)
• 27 June 2013 - by Klaus Draeger de University of Oxford : Synchronization Invariants
• 19 June 2013 - by Jessy Clédière de CEA-Grenoble LETI DSIS STCS CESTI : Treize années au Centre d'Evaluation de la Sécurité des Technologies de l'Information du CEA-Grenoble (CESTI-Léti) (HDR)
• 11 June 2013 - by Christian von Essen de Verimag : Of Markov Decision Processes and Airborne Collisions
• 30 May 2013 - by Chantal Keller de Laboratoire d'informatique de l'X : A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• 23 May 2013 - by Adam Halasz de West Virginia University : Challenges and possible strategies in the modeling of signal initiation by membrane bound receptors
• 6 May 2013 - by Emmanuel Sifakis de Verimag/UJF : Towards efficient and secure shared memory applications (Thesis)
• 26 April 2013 - by Zhoulai Fu de IMDEA Madrid : Picking up your targets --- aggressive strong update beyond common sense
• 25 April 2013 - by Deshmukh Jyotirmoy de Toyota : Mining Temporal Requirements of an Industrial-Scale Control System
• 12 April 2013 - by Florent Garnier de VERIMAG : Verifying C-Programs memory faults freedom by mean of Abstract Interpretation and a-posteriori model verification
• 9 April 2013 - by Paraskevas Bourgos de Verimag / UJF : Rigorous Design Flow for Programming Manycore Platforms (Thesis)
• 22 March 2013 - by Karem Sakalla de University of Michigan Ann Arbor : Saucy3: Fast Symmetry Discovery in Graphs
• 19 March 2013 - by Sanjit Seshia de University of California, Berkeley : Integrating Induction and Deduction for Verification and Synthesis
• 18 March 2013 - by Wang Yi de Uppsala University : Scheduling and Analysis of Cyclic Mode-Switches
• 18 March 2013 - by Rolf Ernst de TU Braunschweig : Mixed critical system design and analysis
• 18 March 2013 - by Wang Yi de Uppsala University : Scheduling and Analysis of Cyclic Mode-Switches
• 6 March 2013 - by Marc Pouzet de UPMC / ENS : Zélus: A Synchronous Language with ODEs
• 21 February 2013 - by Valentin Perrelle de UJF / Verimag : Static Analysis of Programs Manipulating Arrays (Thesis)
• 31 January 2013 - by Ahlem Triki de Verimag : Seminaire doctorant
• 31 January 2013 - by Dario Socci de Verimag : Seminaire doctorant
• 24 January 2013 - by Raphael Jamet de Verimag : Seminaire doctorant
• 24 January 2013 - by Julien Henry de Verimag : Seminaire doctorant
• 24 January 2013 - by Ayoub Nouri de Verimag : Seminaire doctorant
• 16 January 2013 - by Prabhakar Pavithra de IMDEA, Spain : Approximation based Verification of Hybrid Systems
• 7 December 2012 - by Romain Testylier de UJF : Reachability analysis of nonlinear dynamical systems (Thesis)
• 6 December 2012 - by Irina Asavoae de University Alexandru Ioan Cuza, Iasi, Romania : Bounded Model Checking of Recursive Programs with Pointers in K Abstract
• 6 December 2012 - by Mihail Asavoae de University Alexandru Ioan Cuza, Iasi, Romania : Semantics-Based WCET Analysis
• 9 November 2012 - by Damien Massé de Université de Bretagne Occidentale (Brest) : Inférences de propriétés de terminaison par itération de stratégies
• 6 November 2012 - by Pascal Lafourcade de Verimag : Computer Aided Security for Cryptographic Primitives, Voting protocols, and Wireless Sensor Networks (HDR)
• 29 October 2012 - by Jean-François KEMPF de VERIMAG : On Computer-Aided Design-Space Exploration for Multi-Cores (Thesis)
• 24 October 2012 - by Selma Saidi de VERIMAG : Optimizing DMA Data Transfers for Embedded Multi-Cores (Thesis)
• 16 October 2012 - by Guillaume Brat de NASA Ames : An overview of formal methods for Aeronautics at NASA
• 2 October 2012 - by Artur Pietrek de VERIMAG : TIREX: a textual target-level intermediate representation for virtual execution environment, compiler information exchange and program analysis (Thesis)
• 14 September 2012 - by Rance Delong de SRI International : MILS and DMILS project
• 13 September 2012 - by Corneliu Popeea de Technical University of Munich : Synthesizing Software Verifiers from Proof Rules
• 12 July 2012 - by Roberto Bruttomesso de ATRENTA : Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms
• 5 July 2012 - by Pascal Cuoq de CEA : Collaboration d'analyses dans Frama-C
• 26 June 2012 - by Gerardo Schneider de Chalmers | University of Gothenburg : Towards a Framework for Conflict Analysis of Normative Texts Written in Controlled Natural Language
• 26 June 2012 - by Eduardo Mazza de Verimag : A Formal Framework for Specifying and Analyzing Liabilities Using Log as Digital Evidence (Thesis)
• 21 June 2012 - by Jean-Christophe Filliâtre de CNRS / LRI : Combining Interactive and Automated Theorem Proving in Why3
• 7 June 2012 - by Gilles Muller de LIP6 : Remote Core Locking: Migrating Critical-Section Execution to Improve the Performance of Multithreaded Applications
• 5 June 2012 - by Tesnim Abdellatif de Verimag : Rigorous Implementation of Real-time Systems (Thesis)
• 1 June 2012 - by Ian Mitchell de VERIMAG : Scalable approximation of the viability kernel and safe control synthesis for LTI systems using maximal reachability
• 31 May 2012 - by Pavol Cerny de IST Austria : Quantitative Abstraction Refinement
• 29 May 2012 - by Rajarshi RAY de Verimag : Reachability Analysis of Hybrid Systems Using Support Functions (Thesis)
• 25 May 2012 - by Johannes Reich de SPA : A System Perspective on Processes and Their Interactions.
• 11 May 2012 - by Xavier Urbain de ENSIIE : Démonstration automatique : techniques, outils et certification.
• 9 May 2012 - by Pierre Ganty de IMDEA (Madrid) : A Perfect Model for Bounded Verification
• 5 April 2012 - by Laura Kovacs de Technical University of Vienna : Playing in the Grey Area of Proofs
• 22 March 2012 - by Oded Maler de VERIMAG : Performance Evaluation of Schedulers in a Probabilistic Setting
• 12 March 2012 - by Nicolas Berthier de Université de Grenoble : Synchronous Programming of Device Drivers for Global Resource Control in Embedded Systems (Thesis)
• 8 March 2012 - by Goran Frehse de Verimag : Safety Analysis of Hybrid Systems with SpaceEx
• 5 March 2012 - by Sriram Rajamani de Microsoft Research : Program Analysis and Machine Learning: A Win-Win Deal
• 1 March 2012 - by Jerôme Leroux de LABRI : Vector Addition System Reachability Problem
• 23 February 2012 - by Franck Petit de LIP6 : Strength of Stabilization vs. Amount of Resources
• 10 February 2012 - by Laurent George de INRIA Rocquencourt / AOSTE Team INRIA : Robustesse temporelle dans les systèmes embarqués mono et multiprocesseur
• 9 February 2012 - by Jan Olaf Blech de Fortiss : Proof Assistant Based Certification for Modeling Languages and its Application to PLC Development
• 26 January 2012 - by Tom Henzinger de IST-Austria : Quantitative Reactive Modeling
• 19 January 2012 - by Christian von Essen de Verimag : Synthesizing Efficient Controllers
• 12 January 2012 - by Marion DAUBIGNARD de VERIMAG : Formal Methods for Concrete Security Proofs (Thesis)
• 18 November 2011 - by Giovanni Funchal de Verimag/STMicroelectronics : Contributions to Transaction-Level Modeling of Systems-on-a-Chip (Thesis)
• 14 November 2011 - by Philippe Suter de EPFL : Sets with Cardinality Constraints in Satisfiability Modulo Theories
• 4 October 2011 - by Julien Legriel de VERIMAG : Multi-Criteria Optimization and its Application to Multi-Processor Embedded Systems (Thesis)
• 15 September 2011 - by Balaji Raman de DCS, Verimag : On Buffering with Stochastic Guarantees in Resource-Constrained Media Players
• 21 July 2011 - by Pierre Ganty de IMDEA : Pattern-based Verification for Multithreaded Programs
• 30 June 2011 - by Nathalie Bertrand de IRISA : Determinizing timed automata.
• 28 June 2011 - by Francesco Logozzo de Microsoft Research : Practical program verification for the working programmer with CodeContracts and Abstract Interpretation
• 21 June 2011 - by VASSILIKI SFYRLA de VERIMAG/UJF : Modeling Synchronous Systems in BIP (Thesis)
• 26 May 2011 - by Jannik Dreier de VERIMAG : Privacy Properties for Voting Protocols: The completed picture
• 19 May 2011 - by Viktor Kuncak de EPFL : Towards Implicit Programming
• 18 May 2011 - by Jinyun XUE de Institute of Software, Chinese Academy of Science, : PAR Method and PAR Platform for Developing Reliable Software and Its New Development
• 16 March 2011 - by Fabio Somenzi de University of Colorado in Boulder : Clause Manipulation for Faster Satisfiability
• 3 March 2011 - by Hubert Garavel de INRIA : CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processe
• 3 February 2011 - by IMENE BEN HAFAIEDH de VERIMAG-UJF : Component-based Systems: from Design to Implementation (Thesis)
• 21 January 2011 - by Sophie Quinton de Verimag / UJF : Design, verification and implementation of systems of components (Thesis)
• 20 December 2010 - by John Plaice de University of New South Wales : Cartesian Programming (HDR defence) (HDR)
• 18 November 2010 - by Antoine GERBAUD de Synchrone/Asynchrone : Walker model for complex networks
• 5 November 2010 - by Moshe Vardi de Rice University : From Philosophical to Industrial Logics
• 28 October 2010 - by Mohamad Jaber de VERIMAG : Centralized and Distributed Implementations of Correct-by-construction Component-based Systems by using Source-to-source Transformations in BIP (Thesis)
• 22 September 2010 - by Mathias Péron de UJF / VERIMAG : Contributions to the Static Analysis of Programs Handling Arrays (Thesis)
• 15 September 2010 - by Tayeb BOUHADIBA de Verimag : 42, A Component-Based Approach to Virtual Prototyping of Heterogeneous Embedded Systems (Thesis)
• 27 August 2010 - by Manuel Garnacho de VERIMAG - DCS : Automatic and formal certification of critical systems by instrumentation of abstract interpreters (Thesis)
• 26 August 2010 - by Sébastien Bourdeauducq de Sharism at Work : Milkymist : un System-on-Chip libre et orienté video temps réel
• 8 July 2010 - by Sophie Quinton de Verimag : Achieving distributed control through model checking
• 1 July 2010 - by Jocelyne Troccaz de CNRS/TIMC : TBA
• 18 June 2010 - by Arshia Cont de IRCAM : Antescofo : A performance-synchronous language for computer music
• 17 June 2010 - by Karel Heurtefeux de Synchrone : Qualitative localization applied to routing and MAC layer in Wireless Sensor Networks
• 27 May 2010 - by Thanh Hung NGUYEN de Verimag : Constructive Verification for Component-based Systems (Thesis)
• 10 May 2010 - by Christophe JOUBERT de Technical University of Valencia, Spain : Datalog-based Program Analysis with BES and RWL
• 10 May 2010 - by Arnaud Sangnier de DISI, Università di Genova : Weak Time Petri Nets Strike back!
• 10 May 2010 - by Nadia El Mrabet de GREYC algo team - Université de Caen : Arithmétique des couplages, performance et résistance aux attaques par canaux cachés
• 10 May 2010 - by Regis Gascon de Inria Sophia-Antipolis : Verification of quantitative properties on constraint automata
• 7 May 2010 - by Kevin Marquet de Verimag : Vérification automatique de modèles de systèmes sur puce
• 7 May 2010 - by Alexandre DONZE de verimag : Model-based design and analysis of hybrid systems:simulation-based techniques, applications and perspectives
• 22 April 2010 - by Nikolay Kosmatov de CEA - LISI : All-Paths Test Generation for Programs with Internal Aliases in PathCrawler
• 7 April 2010 - by Mohamed Yassin CHKOURI de VERIMAG : Modelling real-time embedded systems using AADL for the automatic generation of applications formally verified (Thesis)
• 1 April 2010 - by Claire Maiza de Compiler Design Lab, Saarland University : Static analysis of interferences in the cache memory in preemptive real-time systems
• 19 March 2010 - by Nicolas Blanc de ETH Zurich : Analyse statique de SystemC avec Scoot : de la Verification à la Simulation
• 9 March 2010 - by Thomas GAWLITZA de verimag : Combining Strategy Iteration with Semidefinite Programming for Abstract Interpretation
• 5 March 2010 - by Marc Poulhiès de VERIMAG - DCS : Design and Implementation of Component Based Systems. Towards a Unification of the Software Engineering and the System Paradigms. (Thesis)
• 4 March 2010 - by Ondrej Sery de Charles University Prague : Code analysis with Blast
• 16 February 2010 - by Bahareh Badban de University of Konstanz : Automated Invariant Generation for the Verification of Real-Time Systems
• 4 February 2010 - by Marius Bozga de Verimag : Component-Based Construction of Real-Time Systems (HDR)
• 29 January 2010 - by Dang Thao de VERIMAG : Methods and tools for Computer Aided Design of Embedded Systems (HDR)
• 14 January 2010 - by Arnaud Sangnier de Universite de Turin : Reversal-bounded counter machines revisited
• 19 November 2009 - by Matthias Althoff de Technische Universität München : Reachability Analysis of Nonlinear and Hybrid Systems with Zonotopes
• 19 November 2009 - by Bruce Krogh de Dept. of Electrical and Computer Engineering, Carn : Research Directions in Cyber-Physical Systems
• 12 November 2009 - by Florent Garnier de Vermimagg- Team DCS : A classification of randomized fair strategies for studying termination of term rewriting
• 9 November 2009 - by Yliès Falcone de Vérimag : Study and implementation of runtime validation techniques (Thesis)
• 29 October 2009 - by Stephane Demri de ENS CACHAN : The covering and boundedness problems for branching vector addition systems
• 28 October 2009 - by Colas Le Guernic de VERIMAG : Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics (Thesis)
• 21 October 2009 - by Aldric Degorre de Vérimag : On Some Quantitative Aspects of Formal Languages (Thesis)
• 24 September 2009 - by Bageshri KARKARE de Verimag : Efficiency, Precision, Simplicity, and Generality in Interprocedural Data Flow Analysis.
• 15 September 2009 - by Dino Distefano de Queen Mary University, London : Compositional Shape Analysis by means of Bi-Abduction
• 25 June 2009 - by Zvonimir Rakamaric de University of British Columbia : Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers
• 25 June 2009 - by Scott Cotton de Verimag : On Some Problems in Satisfiability Solving (Thesis)
• 19 June 2009 - by David Monniaux de CNRS / VERIMAG : Static analysis: from theory to practice (HDR)
• 14 May 2009 - by Florian Kammueller de Technische Universitat Berlin : ASPfun: un calcul pour des objets distribués
• 7 May 2009 - by Villard Jules de LSV, Cachan : Proving Copyless Message Passing
• 16 April 2009 - by Christophe Guillon de STMicroelectronics : Les représentations SSA et Psi-SSA
• 9 April 2009 - by Alexandre Donzé de VERIMAG : Calcul numérique d'ensembles atteignables pour les systèmes hybrides et applications
• 2 April 2009 - by Domagoj Babic de Fujitsu Labs America : Scalable and Precise Extended Static Checking
• 5 March 2009 - by Thomas Gawlitza de Technische Universität München : Precise Relational Invariants Through Strategy Iteration

Archives