• Projects

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

• Tools

  • 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

• Jobs and Internships

  • [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é
  • PERSYVAL Master 2 Scholarships

• Workshops and Conferences

• Members

• Publications

  • Technical Reports

  • Peer reviewed

    • Sorted by year
    • Sorted by kinds

• Ongoing Phd Thesis

  • 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

• Partners

  • Partners

• Seminars

  • Archives

• Documents

• PACS

  • Members
  • Partners

  • Publications

    • by years
    • by kinds

  • Projects

    • SACADE

  • Tools

  • Jobs and Internships

    • 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

  • Members
  • Partners

  • Projects

  • Tools

  • Publications

    • by years
    • by kinds

  • Jobs and Internships

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

• Shared Resources

  • Members
  • Partners

  • Projects

  • Jobs and Internships

  • Publications

    • by kinds

  • Tools

• ETiCS

  • Members

  • Research topics

    • Can Digital Technology help reduce environmental impacts?

    • Digital technologies for modeling the environment

    • Frugal Digital Systems

  • Projects

  • Publications

    • by years
    • by kinds

• FETLAS

  • Members
  • Partners

  • Publications

    • by kinds

  • Projects

  • Jobs and Internships

    • Engineer position: High Level Models for Low Power Systems
    • Funded Ph.D: Dynamic Memory Management For Embedded Non-Volatile Memory
    • Postdoc position: High Level Models for Low Power Systems
    • 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] Dedicated compilation techniques for a domain-specific language (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] Performance Evaluation for Embedded Systems using Formal Methods
    • [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

  • Members
  • Partners

  • Projects

  • Jobs and Internships

  • Tools

  • Publications

    • by kinds

• Whom to contact

  • Whom to contact

• How to reach us

  • How to reach us