Collections, Cardinalities, and Relations

paper ps   
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.

Citation

Kuat Yessenov, Ruzica Piskac, and Viktor Kuncak. Collections, cardinalities, and relations. In Verification, Model Checking, and Abstract Interpretation (VMCAI), 2010.

BibTex Entry

@inproceedings{YessenovETAL10CollectionsRelations,
  author = {Kuat Yessenov and Ruzica Piskac and Viktor Kuncak},
  title = {Collections, Cardinalities, and Relations},
  booktitle = {Verification, Model Checking, and Abstract Interpretation (VMCAI)},
  year = 2010,
  abstract = {  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.}
}