-
Formal verification of secured routing protocols
With the development of digital networks, such as Internet, communication protocols are omnipresent. Digital devices have to interact with each other in order to... -
Environment for the systematic development and proof of correction of functio...
Parallel program design and implementation is a complex, error prone task. Verifying parallel programs is also harder than verifying sequential ones. To ease the... -
Modern languages for modeling and verifying asynchronous systems
The work in this thesis is at the intersection of two major research domains~: Model-Driven Engineering (MDE) and formal methods, and has various fields of... -
Modélisation algorithmique et synthèse d'architectures assistées par model-ch...
International audience -
Formal verification of a key establishment protocol for EPC Gen2 RFID systems...
International audience -
On Post’s embedding problem and the complexity of lossy channels
Lossy channel systems were originally introduced to model communication protocols. It gave birth to a complexity class wich remained scarcely undersood for a long... -
Utilisation de B pour la vérification de spécifications UML et le développeme...
The coupling of object-oriented approaches with the B method makes improvement the activities of software specification and development. The B method provides... -
Towards an integrative approach for the modeling and formal verification of b...
The study of large models of biological networks by means of analysis and simulation tools leads to large amounts of predictions. This raises the question of how to... -
Generation of test sequences for accelerating assertions
With the increasing complexity of SoC, the verification process becomes a task more crucial at all levels of the design cycle, and monopolize a large share of... -
Automatic verification of cryptographic protocols : privacy-type properties
Many tools have been developed to automatically verify security properties on cryptographic protocols. But until recently, most tools focused on trace properties (or... -
Formal specification and verification of distributed component systems
A component is a self contained entity that interacts with its environment through well-defined interfaces. The component library Fractive provides high level... -
Mapping of control functions of critical systems by reachability analysis in ...
The design of operational control architectures is a very important step of the design of energy production systems. This step consists in mapping the functional... -
Development and verification of probability logics and logical frameworks
We introduce a Probability Logic with Conditional Operators - LPCP, its syntax, semantics, and a sound and strongly-complete axiomatic system, featuring an infinitary... -
Safe design method of embedded systems based on COTS
This PhD dissertation contributes to the safe design of COTS-based control-command embedded systems. Due to design constraints bounding delays, costs and engineering... -
Spécifier des agents composés d'agents avec les GDTs
International audience -
Specification and verification of quantitative properties : expressions, logi...
Automatic verification has nowadays become a central domain of investigation in computer science. Over 25 years, a rich theory has been developed leading to numerous... -
Deductive Verification of Distributed Groupware Systems
Colloque avec actes et comité de lecture. nationale.
