Kaïs Klai

Application/Adaptation of Formal Verification Techniques to a Specific Domains

Parallel to my interest in model checking technique, I am interested in applying and adapting formal verification techniques to specific domains such as inter-enterprise business processes, service composition, Cloud-based systems, diagnosis/control of discret event systems (DES), security properties, and processes in the Blockchain. Indeed, I have the conviction that developing domain-specific verification approaches may be more effective than general purpose verification techniques. Specific domains could have particular requirements/constraints and even specific properties that make existing monolithic verification approaches inappropriate or even inapplicable. On one hand, developing domain-specific verification approaches could allow to take benefit from the own characteristics of the domain’s applications, leading to a better efficiency. On the other hand, domain-specific approaches could bring new ideas to improve the verification in the general case. This would ideally create a virtuous circle where general and specific-domain verification approaches enrich each other.