- Presentation
- HAL publications
- Activity reports
MOSCOVA Research team
Mobililty, security, concurrence, verification and analysis
- Leader : Luc Maranget
- Type : Project team
- Research center(s) : Paris - Rocquencourt
- Field : Algorithmics, Programming, Software and Architecture
- Theme : Programs, Verification and Proofs
Team presentation
The research of the MOSCOVA project-team follows two main directions: studying programming languages for distributed and mobile applications, and analyzing and verifying multitasking programs. The team produces a system (compiler and runtime environment) for programming such distributed and mobile applications.
Research themes
- Fine-grain integration of concurrent programming into functional programming, while preserving static typing, pattern matching and modularity.
- Interaction control by using lexical scoping, achievable by classical cryptographic methods.
- Failure management in a distributed setting.
Our work is based upon the join-calculus, a theory of concrurrency that is well adapted to distributed systems. More generally, the team takes part to studying and implementing functionnal languages. As regards our activity on program verification and analysis, we aim at producing tools that handle industrial size codes, detect interference beetween tasks, out of bound array accesses and overflows.
International and industrial relations
- We distribute implementations of our join-calculus based languages.
- We collaborate with the danish company Terma A/S, on a methodogical study for producing robust space software.
- We are part of the Esprit projet PEPITO with KTH, EPFL, SICS, UCL and the University of Cambridge.
- Several members of the MOSCOVA team direct courses at École polytechnique.
Keywords: Parallelism Asynchronous parallelism Functional programming Multiprocessor architecture Instruction ordering Concurrence Lambda-calculus Garbage collection
Research teams of the same theme :
- ABSTRACTION - Abstract Interpretation and Static Analysis
- ATEAMS - Analysis and Transformation based on rEliAble tool coMpositionS
- CARTE - Theoretical adverse computations, and safety
- CASSIS - Combination of approaches to the security of infinite states systems
- CELTIQUE - Software certification with semantic analysis
- COMETE - Concurrency, Mobility and Transactions
- CONTRAINTES - Constraint programming
- DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
- FORMES - Formal Methods for Embedded Systems
- GALLIUM - Programming languages, types, compilation and proofs
- MARELLE - Mathematical, Reasoning and Software
- MEXICO - Modeling and Exploitation of Interaction and Concurrency
- PAREO - Formal islands: foundations and applications
- PARSIFAL - Proof search and reasoning with logic specifications
- PI.R2 - Design, study and implementation of languages for proofs and programs
- PROSECCO - Programming securely with cryptography
- SECSI - Security of information systems
- TASC - Theory, Algorithms and Systems for Constraints
- TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
- TYPICAL - Types, Logic and computing
- VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Contact
Team leader
Luc Maranget
Tel.: +33 1 39 63 56 89
Secretariat
Tel.: +33 1 39 63 57 19
Find out more
Genealogy
This team follows
Inria
Inria.fr
Inria Channel

See also