Logical Abstract Domains and Interpretations
Résumé
We give semantic foundations to abstract domains consisting in first order logic formulae in a theory, as used in verification tools or methods using SMT-solvers or theorem provers. We exhibit conditions for a sound usage of such methods with respect to multi-interpreted semantics and extend their usage to automatic invariant generation by abstract interpretation.
Domaines
Langage de programmation [cs.PL]
Origine : Fichiers produits par l'(les) auteur(s)
Loading...