conference paper
Collections, Cardinalities, and Relations
Barthe, Gilles
•
Hermenegildo, Manuel V.
2010
Proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation
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.
Type
conference paper
Author(s)
Editors
Barthe, Gilles
•
Hermenegildo, Manuel V.
Date Issued
2010
Published in
Proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation
Series title/Series vol.
LNCS; 5944
Start page
380
End page
395
Subjects
Editorial or Peer reviewed
REVIEWED
Written at
EPFL
EPFL units
Available on Infoscience
December 1, 2010
Use this identifier to reference this record