A Configurable CEGAR Framework with Interpolation-Based Refinements

Abstract : Correctness of software components in a distributed system is a key issue to ensure overall reliability. Formal verification techniques such as model checking can show design flaws at early stages of development. Abstraction is a key technique for reducing complexity by hiding information, which is not relevant for verification. Counterexample-Guided Abstraction Refinement (CEGAR) is a verification algorithm that starts from a coarse abstraction and refines it iteratively until the proper precision is obtained. Many abstraction types and refinement strategies exist for systems with different characteristics. In this paper we show how these algorithms can be combined into a configurable CEGAR framework. In our framework we also present a new CEGAR configuration based on a combination of abstractions, being able to perform better for certain models. We demonstrate the use of the framework by comparing several configurations of the algorithms on various problems, identifying their advantages and shortcomings.
Type de document :
Communication dans un congrès
Elvira Albert; Ivan Lanese. 36th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2016, Heraklion, Greece. Lecture Notes in Computer Science, LNCS-9688, pp.158-174, 2016, Formal Techniques for Distributed Objects, Components, and Systems. 〈10.1007/978-3-319-39570-8_11〉
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01432916
Contributeur : Hal Ifip <>
Soumis le : jeudi 12 janvier 2017 - 11:34:15
Dernière modification le : vendredi 8 décembre 2017 - 18:04:01
Document(s) archivé(s) le : vendredi 14 avril 2017 - 16:04:56

Fichier

 Accès restreint
Fichier visible le : 2019-01-01

Connectez-vous pour demander l'accès au fichier

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Ákos Hajdu, Tamás Tóth, András Vörös, István Majzik. A Configurable CEGAR Framework with Interpolation-Based Refinements. Elvira Albert; Ivan Lanese. 36th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2016, Heraklion, Greece. Lecture Notes in Computer Science, LNCS-9688, pp.158-174, 2016, Formal Techniques for Distributed Objects, Components, and Systems. 〈10.1007/978-3-319-39570-8_11〉. 〈hal-01432916〉

Partager

Métriques

Consultations de la notice

28