Extensions de l’algorithme d’atteignabilité arrière dans le cadre de la vérification de modèles modulo théories
| Autor: | Roux, Mattias |
|---|---|
| Přispěvatelé: | Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Université Paris Saclay (COmUE), Sylvain Conchon, Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), STAR, ABES |
| Jazyk: | francouzština |
| Rok vydání: | 2019 |
| Předmět: |
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO]
Apprentissage non supervisé [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] Vérification de modèles Vérification de modèles modulo theories Unsupervised learning [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL] Model Checking Vérification déductive Satisfiability Modulo Theories [INFO.INFO-CL] Computer Science [cs]/Computation and Language [cs.CL] Model Checking Modulo Theories Distributed Systems Deductive Verification Systèmes distribués Satisfiabilité modulo théories |
| Zdroj: | Logique en informatique [cs.LO]. Université Paris Saclay (COmUE), 2019. Français. ⟨NNT : 2019SACLS582⟩ |
| Popis: | This thesis proposes to present several extensions that have been added to the Cubicle model checker.Cubicle is a software allowing to automatically check the safety of parameterized systems using model checking modulo theory techniques.The first contribution made by this thesis consists in the implementation of a new reachability algorithm called FAR (for Forward Abstracted Reachabilty). FAR is an algorithm involving both backward reachability analysis techniques already implemented in Cubicle as well as forward reachability analysis techniques.The second contribution consists of multiple additions inspired by artificial intelligence methods to improve the automatic generation of Cubicle invariants.Finally, the last contribution has increased Cubicle's expressiveness in order to prove properties involving universal quantifiers. This contribution was implemented by associating Cubicle with Why3, a deductive verification platform. Cette thèse se propose de présenter plusieurs extensions ayant été ajoutées au vérificateur de modèles Cubicle.Cubicle est un logiciel permettant de vérifier automatiquement la sûreté de systèmes paramétrés au moyen de techniques de vérification de modèles modulo théories.La première contribution apportée par cette thèse consiste en l'implémentation d'un nouvel algorithme d'atteignabilité baptisé FAR (pour Forward Abstracted Reachabilty). FAR est un algorithme faisant intervenir à la fois des techniques de l'analyse d'atteignabilité en arrière déjà implémentée dans Cubicle ainsi que des techniques d'analyse d'atteignabilité en avant.La seconde contribution est constituée de multiples ajouts inspirés de méthodes de l'intelligence artificielle afin d'améliorer la génération automatique d'invariants de Cubicle.Enfin, la dernière contribution a permis d'augmenter l'expressivité de Cubicle afin de prouver des propriétés faisant intervenir des quantificateurs universels. Cette contribution a été mise en œuvre en associant Cubicle à Why3, une plateforme de vérification déductive. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|