ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Auteurs : soumettez
votre article en ligne

APPEL À
CONTRIBUTION

Le comité de rédaction du JESA lance un appel à proposition de numéros spéciaux.

En savoir plus >>
Autres revues >>

Journal Européen des Systèmes Automatisés

1269-6935
Revues des Systèmes
 

 ARTICLE VOL 47/1-3 - 2013  - pp.45-59  - doi:10.3166/jesa.47.45-59
TITRE
Élimination de quantificateurs : extrapolation efficace par analyse structurelle et cœurs insatisfiables

RÉSUMÉ
Les utilisations de l’élimination de quantificateurs (QE) en vérification formelle sont nombreuses : calcul symbolique de préimage, découverte d’invariants par instanciation de patrons, abstraction automatique de programmes, etc. Sur la base d’un algorithme de QE très efficace, dû à Monniaux en 2008, qui combine tests SMT et projections polyédriques, nous présentons les améliorations suivantes : une généralisation de la phase projection permettant de traiter des formules contenant des atomes Booléens, entiers et réels ; l’emploi des cœurs insatisfiables des formules dans la phase d’extrapolation pour aider à minimiser l’extrapolant et accélérer sa création ; une analyse structurelle qui identifie un sous-ensemble de litéraux expliquant la satisfiabilité de la formule, et en dérive un extrapolant ; un algorithme d’extrapolation hybride mêlant analyse structurelle, tests SMT et cœurs insatisfiables. Enfin, nous discutons des résultats expérimentaux obtenus sur des exemples tirés d’applications industrielles.


ABSTRACT
Quantifier Elimination (QE) enjoys many sucessful applications in reactive systems verification : symbolic preimage computation, template-based invariant discovery, automatic program abstraction, to name a few. Starting from a very effective QE algorithm due to Monniaux in 2008, which combines SMT solving and polyhedral projection, we propose the following enhancements : a generalisation of the projection phase of this QE algorithm to the case of formulas mixing Boolean, integer and real atoms ; the use of unsatisfiable cores of formulas in the extrapolation phase to minimise the extrapolants and speed-up their creation ; a structural analysis to quickly identify literals relevant to the satisfiability of a formula and derive an extrapolant, as well as an hybrid extrapolation algorithm mixing structural, SMT and unsat core analyses. Last, we discuss the results of experiments conducted on examples stemming from industrial applications.


AUTEUR(S)
Rémi DELMAS, Adrien CHAMPION

MOTS-CLÉS
élimination de quantificateurs, extrapolation, analyse structurelle, SMT, cœurs insatisfiables.

KEYWORDS
quantifier elimination, extrapolation, structural analysis, SMT, unsatisfiable cores.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 7.5 €
• Non abonné : 15.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (303 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier