Department 2 : formal methods

Team leader : Michaël Rusinowitch
Tél. : +33 3 83 59 30 20
Mail : michael.rusinowitch@loria.fr

Presentation

The objective of the project is to design and develop tools to verify the safety of systems with an infinite number of states. The analysis of such systems is based on a symbolic representation of sets of states in terms of formal languages or logical formulas. Safety is obtained via automatic proof, symbolic exploration of models or test generation. These validation methods are com- plementary. They rely on the study of accessibility problems and their reduction to constraint solving.

Research activities

• Automated Deduction
• Security Protocol Verification
• Verification for Service Oriented Computing

Software

• CI-Atse

• AVANTSSAR Orchestrator
• P2PEdit
• DeSCal

Collaborations

• Clarkson University
• Genova University
• Verona [University
• Milan University
• INRIA project-team DAHU (LSV Cachan)
• Bristol University, UK,
• Edinburgh University, UK,
• Kiel University, Germany and ETH Zurich
• Albany University, USA,
• France Telecom R&D
• INRIA project-team SECSI (LSV Cachan)
• INRIA project-team MADYNES
• IRIT Toulouse
• UTFSM Valparaiso and Score LORIA

Keywords

Formal methods, automated deduction, automated verification, security, embedded systems, cryptographic protocols, Web services, symbolic models, computational models, test generation, decision procedures, equational logic, constraint solving, automata