Description
Date depot: 1 janvier 1900
Titre: Concurrency, Random Generation and Model Checking
Directeur de thèse:
Jean MAIRESSE (LIP6)
Directeur de thèse:
Samy ABBES (IRIF)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Algorithmique, combinatoire
Resumé:
This research proposal is at the intersection of several research areas: combina- torics and probabilities, random generation and model checking.
Nowadays software systems are of increasing complexity and scale, important factors of this complexity relating to parallelism and concurrency. The domain of model checking aims at ensuring that such complex systems are free of defects by verifying logical properties on the systems. This has been addressed by many researchers, with various analysis methods and techniques for giving formal complete proofs of correctnes. The central point of most of these approaches is to tackle the so called ”combinatorial explosion problem”, a phenomenon due to the multiplicity of concurrent executions. However, even if great progress has been achieved, the formal verification of even medium sized software systems mainly remains inaccessible. A very promising approach to scale the existing techniques to larger and more realistic software systems is to adopt a probabilistic view of the problem.
Statistical checking allows to deal with larger models and more complex spec- ifications. However the answer is probabilistic and maybe false. Thus statistical model checking requires first a probabilistic method to evaluate the number of trials, and second a stochastical model for uniformly generating the objects.
Our PhD proposal adopts a combinatorial approach of developing probabilis- tic analysis techniques for concurrent systems, based on relationships between the theory of concurrency and trace monoids. It aims at developing theoretical studies as well as an algorithmic framework for practical applications.
Doctorant.e: Chen Yi Ting