Deciding extensions of the theories of vectors and bags

Patrick Maier

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Vectors and bags are basic collection data structures, which are used frequently in programs and specifications. Reasoning about these data structures is supported by established algorithms for deciding ground satisfiability in the theories of arrays (for vectors) and multisets (for bags), respectively. Yet, these decision procedures are only able to reason about vectors and bags in isolation, not about their combination.

This paper presents a decision procedure for the combination of the theories of vectors and bags, even when extended with a function bagof bridging between vectors and bags. The function bagof converts vectors into the bags of their elements, thus admitting vector/bag comparisons. Moreover, for certain syntactically restricted classes of ground formulae decidability is retained if the theory of vectors is extended further with a map function which applies uninterpreted functions to all elements of a vector.
Original languageEnglish
Title of host publicationVerification, Model Checking, and Abstract Interpretation
Subtitle of host publication10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings
EditorsNeil D Jones, Markus Müller-Olm
PublisherSpringer
Pages245-259
Number of pages15
Volume5403
ISBN (Electronic)978-3-540-93900-9
ISBN (Print)978-3-540-93899-6
DOIs
Publication statusPublished - 2009
Event10th International Conference on Verification, Model Checking, and Abstract Interpretation - Savannah, Georgia, United States
Duration: 18 Jan 200920 Jan 2009

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume5403
ISSN (Print)0302-9743

Conference

Conference10th International Conference on Verification, Model Checking, and Abstract Interpretation
Abbreviated titleVMCAI 2009
CountryUnited States
CitySavannah, Georgia
Period18/01/0920/01/09

Keywords

  • verification and program analysis
  • decision procedures
  • vectors
  • multisets

Fingerprint Dive into the research topics of 'Deciding extensions of the theories of vectors and bags'. Together they form a unique fingerprint.

  • Cite this

    Maier, P. (2009). Deciding extensions of the theories of vectors and bags. In N. D. Jones, & M. Müller-Olm (Eds.), Verification, Model Checking, and Abstract Interpretation: 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings (Vol. 5403, pp. 245-259). (Lecture Notes in Computer Science; Vol. 5403). Springer. https://doi.org/10.1007/978-3-540-93900-9_21