list | abstracts | bib ]

On Decision Procedures for Collections, Cardinalities, and Relations

paper pdf    paper ps   

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.

Citation

Kuat Yessenov, Viktor Kuncak, and Ruzica Piskac. On decision procedures for collections, cardinalities, and relations. Technical Report LARA-REPORT-2009-004, EPFL, 29 August 2009.

BibTex Entry

@TECHREPORT{YessenovETAL09OnDecisionProceduresCollectionsRelations,
  author = {Kuat Yessenov and Viktor Kuncak and Ruzica Piskac},
  title = {On Decision Procedures for Collections, Cardinalities, and Relations},
  institution = {EPFL},
  year = 2009,
  number = {LARA-REPORT-2009-004},
  month = {29 August},
  localurl = {http://lara.epfl.ch/~kuncak/papers/YessenovETAL09OnDecisionProceduresCollectionsRelations.pdf}
}

list | abstracts | bib ]