Collections, Cardinalities, and Relations

Logics that involve collections (sets, multisets), and cardinality constraints are useful for reasoning about unbounded data structures and concurrent processes. To make such logics more useful in verification this paper extends them with the ability to compute direct and inverse relation and function images. We establish decidability and complexity bounds for the extended logics.


Editeur(s):
Barthe, Gilles
Hermenegildo, Manuel V.
Publié dans:
Proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation, 380-395
Année
2010
Mots-clefs:
Laboratoires:




 Notice créée le 2010-12-01, modifiée le 2019-08-12

Preprint:
Télécharger le document
PDF

Évaluer ce document:

Rate this document:
1
2
3
 
(Pas encore évalué)