SUMO Research team
SUpervision of large MOdular and distributed systems
- Leader : Eric Fabre
- Type : Project team
- Research center(s) : Rennes
- Field : Algorithmics, Programming, Software and Architecture
- Theme : Proofs and Verification
- Partner(s) : Université Rennes 1,CNRS
- Collaborator(s) : Institut de recherche en informatique et systèmes aléatoires (IRISA) (UMR6074)
The SUMO team proposes to combine formal methods approaches with concurrency theory, in order to address the modeling, analysis and management of large distributed or modular systems exhibiting quantitative aspects. Large distributed softwares and systems are indeed calling for quantitative models involving time, probabilities, costs, and combinations of them. As many problems in this setting become untractable or even undecidable, we are interested in the design of efficient approximation techniques, for example borrowed from electrical engineering approaches to the management of large stochastic systems.
A strong point of SUMO is to gather skills from formal methods, discrete event systems, concurrency theory, and electrical engineering. Several application fields are covered: telecommunication networks management, modeling and verification of web services, control issues in large data centers, plus more opportunistic applications in the field of embedded systems or biological pathways.
International and industrial relations
- AVerTS Indo-French project on the algorithmic verification of real-time systems
- QuantProb Associated team on optimization of non-standard quantitative properties in partially observable probabilistic models with Dresden Technical University
- EQUAVE Associated team on efficient quantitative verification.
- ANR Project STOCH-MC (2014-2018), Stochastic Models: Scalable Model Checking.
- P22 Project (2015-2018), Industrial project with Alstom Transport
- ANR Headwork (2016-2020), Human-Centric Data Oriented Workflows
- Softwarisation of everything: A joint resserach team within the INRIA-Nokia Bell Labs common lab, dedicated to programmability and management of SDNs
Research teams of the same theme :
- ANTIQUE - Static Analysis by Abstract Interpretation
- CELTIQUE - Software certification with semantic analysis
- CONVECS - Construction of verified concurrent systems
- DEDUCTEAM - DEDUCTEAM
- GALLINETTE - Gallinette: developing a new generation of proof assistants
- GALLIUM - Programming languages, types, compilation and proofs
- MARELLE - Mathematical, Reasoning and Software
- MEXICO - Modeling and Exploitation of Interaction and Concurrency
- MOCQUA - Designing the Future of Computational Models
- PARSIFAL - Proof search and reasoning with logic specifications
- PI.R2 - Design, study and implementation of languages for proofs and programs
- TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
- VERIDIS - Modeling and Verification of Distributed Algorithms and Systems