Ph.D
Group : Verification of Algorithms, Languages and Systems
Inférence d'invariants pour le model checking de systèmes paramétrés
Starts on 03/10/2011
Advisor : CONCHON, Sylvain
[ZAIDI Fatiha]
Funding :
Affiliation : Université Paris-Saclay
Laboratory : LRI PROVAL
Defended on 29/09/2014, committee :
Directeur de thèse :
- M. Sylvain Conchon, Professeur, Université Paris-Sud
Co-encadrante :
- Mme Fatiha Zaïdi, Maître de conférences, Université Paris-Sud
Rapporteurs :
- M. Ahmed Bouajjani, Professeur, Université Paris Diderot et IUF
- M. Silvio Ranise, Chercheur, Fondazione Bruno Kessler
Examinateurs :
- M. Rémi Delmas, Ingénieur de recherche, ONERA
- M. Alan Schmitt, Chargé de recherche, INRIA Rennes Bretagne Atlantique
- M. Philippe Dague, Professeur, Université Paris-Sud
Research activities :
- Automated Proof, SMT and Applications
Abstract :
This thesis tackles the problem of automatically verifying complex
parameterized systems. This approach is important because it can guarantee that
some properties hold without knowing a priori the number of components in the
system. We focus in particular on the safety of such systems and we handle the
parameterized aspect with symbolic methods. This work is set in the theoretical
framework of the model checking modulo theories and resulted in a new model
checker: Cubicle.
One of the main contribution of this thesis is a novel technique for
automatically inferring invariants. The process of invariant generation is
integrated with the model checking algorithm and allows the verification in
practice of systems which are out of reach for traditional symbolic
approaches. One successful application of this algorithm is the safety analysis
of industrial size parameterized cache coherence protocols.
Finally, to address the problem of trusting the answer given by the model
checker, we present two techniques for certifying our tool Cubicle based on the
framework Why3. The first consists in producing certificates whose validity can
be assessed independently while the second is an approach by deductive
verification of the heart of Cubicle.
