• Projets

  • Coopération Argosim
  • Cooperation PragmaDev
  • CAOTIC : Collaborative Action on Timing Interferences
  • TAVA
  • ALDIWO

• Outils

  • Time-Critical Applications on Multicore Platforms
  • VPL (Verimag/Verified Polyhedron Library)
  • aadl2sync
  • aadl4ocaml
  • AMT 2.0
  • Argos and Larissa
  • Aspic
  • BDDC v2
  • BinSec
  • BIP Compiler
  • BIP-SMC : A Statistical Model Checking Engine for the BIP framework
  • d/dt
  • DFinder
  • FISSC
  • FLATA
  • FLATA-C
  • GUEB
  • IF Toolset
  • InVeSt
  • Kronos
  • L2CA
  • Lazart
  • LIBTLMPWT
  • Lurette
  • Lustre V6
  • Lutin
  • Mjollnir
  • Montre
  • Multi-core interference Analysis
  • NLTOOLBOX
  • OpenKronos
  • Pagai
  • ParetoLib
  • PHAVer
  • Pinapa
  • PinaVM
  • RDBG
  • Reglo
  • RTD-Finder
  • SASA
  • SatAns-Cert
  • sc-during
  • SCRV
  • SMI
  • SpaceEx
  • SR3 : Secure Resilient and Reputation-based Routing
  • ss2lus
  • StreamExplorer
  • TGV
  • the Chamois CompCert Compiler
  • The Impure Library
  • The Lustre V4 Toolbox
  • The Synchrone Reactive Toolbox
  • The VPL Tactic

• Emplois et stages

  • [Master] Implementation of critical applications on multi-core : execution mode analysis to reduce interferences
  • [PostDoc] Implementation of critical applications on multi-core : execution mode analysis to reduce interferences
  • [Master]Leakage in presence of an active and adaptive adversary
  • [Master] Adapting Hardware Platforms to a Multi-Core Response Time Analysis Framework
  • [Master] Towards New Frontiers in Multi-Core Response Time Analysis ?
  • [Master] Analyzing fault parameters triggering timing anomalies
  • [Master] Exploration by model-checking of timing anomaly cancellation in a processor
  • [Funded PhD] Quantitative analysis of software security against adaptive attacks
  • [Funded PhD] Annotations de sécurité pour compilateur optimisant formellement vérifié
  • Bourses PERSYVAL de M2

• Colloques et Conférences

• Membres

• Publications

  • Rapports Techniques

  • Avec comité de lecture

    • Classées par années
    • Classées par types

• Thèse en cours

  • Aina Rasoldier
  • Akshay Mambakam
  • Bob AUBOUIN-PAIRAULT
  • Daniel DE CARVALHO
  • Etienne BOESPFLUG
  • Hadi DAYEKH
  • Hamzah Al-Qadasi
  • Ihab ALSHAER
  • Lucas BUERI
  • Matheus Schuh
  • Oussama OULKAID
  • Soline Ducousso
  • Thomas Mari
  • Thomas Vigouroux
  • Tobias Rosenberger
  • Vincent Morice
  • Ye Xiang

• Partenaires

  • Partenaires

• Séminaires

  • Archives

• Documents

• PACS

  • Membres
  • Partenaires

  • Publications

    • par années
    • par types

  • Projets

    • SACADE

  • Outils

  • Emplois et stages

    • Phd Proposal : Inférence de modèles de faute pour simulation d’attaques sur composants sécurisés
    • Phd proposal : Optimisation de l’évaluation et des tests de sécurité des systèmes cyber-physiques par analyse des canaux auxiliaires
    • Post-Doc : Fault injection and code analysis

• MOHYTOS

  • Membres
  • Partenaires

  • Projets

  • Outils

  • Publications

    • par années
    • par types

  • Emplois et stages

    • Post-Docs : Model-Based Design and Validation of Safety-Critical Systems

• Ressources partagées

  • Membres
  • Partenaires

  • Projets

  • Emplois et stages

  • Publications

    • par types

  • Outils

• ETiCS

  • Membres

  • Thèmes de recherche

    • Le numérique peut-il aider à réduire nos impacts environnementaux ?

    • Le numérique comme outil de modélisation pour l’environnement

    • Un numérique frugal

  • Projets

  • Publications

    • par années
    • par types

• FETLAS

  • Membres
  • Partenaires

  • Publications

    • par types

  • Projets

  • Emplois et stages

    • Poste d’ingénieur : Modèles de haut niveau pour systèmes basse consommation
    • Thèse financée : Gestion dynamique de la mémoire non-volatile embarquée
    • Offre de post-doctorat : Modèles de haut niveau pour systèmes basse consommation
    • Experienced engineer wanted (compiler frontend / GUIs)
    • M2R : Timing analysis (WCET) of multi-core TDMA bus (2015-2016)
    • Performance Evaluation of Embedded Systems : a tradeoff between accuracy and scalability
    • Potential CIFRE PhD : Hardened circuits for critical applications
    • Probabilistic Methods for Routing in Wireless Sensor Network
    • Silent Self-Stabilizing Algorithms : Certification Using Coq
    • [funded PhD] avanced static analysis techniques
    • [M1 2012-2013] Optimisations de performances de simulateurs sur machines multi-cœurs
    • [M1 2013-2014] Distributed Simulation for Embedded Systems
    • [M1 2013-2014] Parallel programming in modeling of embedded systems
    • [M2R 2012-2013] Techniques de compilation dédiées pour un langage spécifique à un domaine (SystemC)
    • [M2R 2012-2013] Analyse de programme efficace : SMT-solving et itérations
    • [M2R 2012-2013] Analyse modulaire de programmes
    • [M2R 2012-2013] Borner le temps maximum d’exécution par analyse statique
    • [M2R 2012-2013] Contraintes non linéaires
    • [M2R 2012-2013] Décision de formules contenant des flottants
    • [M2R 2012-2013] Optimisation de formules SMT
    • [M2R 2012-2013] Preuve automatique de programmes
    • [M2R 2012-2013] Preuve de programmes avec des structures de données
    • [Master 2R 2011-2012] Evaluation and Validation of Clock-Synchronization Protocols in Sensor Networks
    • [master 2R 2011-2012] Routing Protocols for (Dynamic) Wireless Sensor Networks
    • [Master 2R 2014-2015] Évaluation de performances pour les systèmes embarqués avec des méthodes formelles
    • [MASTER 2] Performance Evaluation for Embedded Systems : Between Computational Simulation and Mathematical Solutions
    • [Master 2] Probabilistic Methods for Routing in Wireless Sensor Networks
    • [postdoc] Advanced static analysis
    • [TAKEN] [M1 2012-2013] Visualisation graphique de traces de simulation de systèmes sur puces

• Formal Proofs

  • Membres
  • Partenaires

  • Projets

  • Emplois et stages

  • Outils

  • Publications

    • par types

• Qui contacter

  • Qui contacter

• Venir à Verimag

  • Venir à Verimag