Actualités
Séminaires
- Séminaires
- 29 novembre 2021 Nicolas Basset: Uniform sampling for networks of automata
- 2 décembre 2021 Leo Exibard: Reactive synthesis over infinite data domains with machines with registers
- 7 décembre 2021 Alessio Mansutti: Efficient complementation of semilinear sets and the vc dimension of presburger (...)
- 9 décembre 2021 Le séminaire de Charlie Jacomme: est annulé ou reporté
- 13 décembre 2021 Joseph Sifakis: Specification and validation of autonomous driving systems: a multilevel semantic (...)
- 13 janvier 2022 Benjamin Blanc: Formal methods in practice: model checking in the railway industry
Dernières brèves
- Nouvelles brèves
- 5 décembre 2021 La science taille XX’Elles
Nouvelles publications
- Quelques Publications
Récentes
- Karine Altisen, Stéphane Devismes, Erwan Jahier: SASA: A SimulAtor of Self-stabilizing Algorithms
- Mnacho Echenim, Radu Iosif, Nicolas Peltier: The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates
- Léo Gourdin, Sylvain Boulmé: Certifying assembly optimizations in Coq by symbolic execution with hash-consing
- Guillaume Brau, Mohammed Foughali: Contract-Based Verification of Model Transformations: A Formally Founded Approach
Offres d'emploi et stages
- Offres d'emploi et stages
- PhD position : software vulnerability analysis guided by countermeasures and attacker capabilities
- (un)decidability of polyhedral invariant inference
- PhD position : Encoding and Sampling of Constrained Signal Spaces for Validation of CPS
- verified decomposition of arithmetic operators
- Verified global value numbering
- [L3/M1/M2 Internship] Topics in Formally Verified Compilation
- [M2 Internship] Leakage in presence of an active and adaptive adversary
- [M2 Internship] Security counter-measures in a certified optimizing compiler
- [M2R Internship] Analyse et Evaluation d’implémentations sécurisées robustes à l’injection de fautes
- [M2R Internship] Patch analysis of IIoT components
- [master or PhD] Convex polyhedra in floating point
- [master] automatic insertion of countermeasures in a verified compiler
- [Master] Decision Procedures for Separation Logic Modulo Theories of Data
- [Master] Design and Evaluation of Strategies for Automated Proofs using Reasoning Modulo Equivalence
- [master] formally verified hash-consing
- [Master] Local Reasoning about Reconfigurable Component-based Systems
- [Master] Multi-core Interference analysis and Global Scheduling
- [Master] Simulation of Distributed Algorithms
- [Master] Verifying Concurrent Systems with Automata over Infinite Alphabets
