This thesis provides strategies for multiple vehicles to explore unknown environments in a cooperative and systematic manner. These strategies are called Simultaneous Cooperative Exploration and Networking (SCENT) strategies. As the basis for development of SCENT strategies, we first tackle the motion control and planning for one vehicle with range sensors. In particular, we develop the curve-tracking controllers for autonomous vehicles with rigidly mounted range sensors, and a provably complete exploration strategy is proposed so that one vehicle with range sensors builds a topological map of an environment. The SCENT algorithms introduced in this thesis extend the exploration strategy for one vehicle to multiple vehicles. The enabling idea of the SCENT algorithms is to construct a topological map of the environment, which is considered completely explored if the map corresponds to a complete Voronoi diagram of the environment. To achieve this, each vehicle explores its local area by incrementally expanding the already visited areas of the environment. At the same time, every vehicle deploys communication devices at selected locations and, as a result, a communication network is created concurrently with a topological map. This additional network allows the vehicles to share information in a distributed manner resulting in an efficient exploration of the workspace. The efficiency of the proposed SCENT algorithms is verified through theoretical investigations as well as experiments using mobile robots. Moreover, the resulting networks and the topological maps are used to solve coordinated multi-robot tasks, such as capturing intruders.

La sécurité est une des préoccupations principales de l'informatique moderne. De plus en plus de personnes utilisent un ordinateur pour des opérations sensibles comme pour des transferts bancaires, des achats sur internet, le payement des impôts ou même pour voter. La plupart de ces utilisateurs ne savent pas comment la sécurité est assurée, par conséquence ils font totalement confiance à leurs applications. Souvent ces applications utilisent des protocoles cryptographiques qui sont sujet à erreur, comme le montre la célèbre faille de sécurité découverte sur le protocole de Needham-Schroeder dix-sept ans après sa publication. Ces erreurs proviennent de plusieurs aspects : -- Les preuves de primitives cryptographiques peuvent contenir des erreurs. -- Les propriétés de sécurité ne sont pas bien spécifiées, par conséquence, il n'est pas facile d'en faire la preuve. -- Les hypothèses faites sur le modèle de l'intrus sont trop restrictives. Dans cette habilitation, nous présentons des méthodes formelles pour vérifier la sécurité selon ces trois aspects. Tout d'abord, nous construisons des logiques de Hoare afin de prouver la sécurité de primitives cryptographiques comme les chiffrements à clef publique, les modes de chiffrement asymétriques et les codes d'authentification de message ( Message authentication codes, MACs). Nous étudions aussi les protocoles de votes électroniques et les réseaux de capteus sans fil ( Wireless Sensor Networks, WSNs ). Dans ces deux domaines, nous analysons les propriétés de sécurité afin de les modéliser formellement. Ensuite nous développons des techniques appropriées afin de les vérifier.