Deciding extensions of the theories of vectors and bags

Patrick Maier

doi:10.1007/978-3-540-93900-9_21

Deciding extensions of the theories of vectors and bags

Patrick Maier

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English
Title of host publication	Verification, Model Checking, and Abstract Interpretation
Subtitle of host publication	10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings
Editors	Neil D Jones, Markus Müller-Olm
Publisher	Springer
Pages	245-259
Number of pages	15
Volume	5403
ISBN (Electronic)	978-3-540-93900-9
ISBN (Print)	978-3-540-93899-6
DOIs	https://doi.org/10.1007/978-3-540-93900-9_21
Publication status	Published - 2009
Event	10th International Conference on Verification, Model Checking, and Abstract Interpretation - Savannah, Georgia, United States Duration: 18 Jan 2009 → 20 Jan 2009

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	5403
ISSN (Print)	0302-9743

Conference

Conference	10th International Conference on Verification, Model Checking, and Abstract Interpretation
Abbreviated title	VMCAI 2009
Country/Territory	United States
City	Savannah, Georgia
Period	18/01/09 → 20/01/09

Keywords

verification and program analysis
decision procedures
vectors
multisets

Access to Document

10.1007/978-3-540-93900-9_21

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

@inproceedings{5c4aed1c47d2415ca0a81fff8787af47,

title = "Deciding extensions of the theories of vectors and bags",

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.",

keywords = "verification and program analysis, decision procedures, vectors, multisets",

author = "Patrick Maier",

year = "2009",

doi = "10.1007/978-3-540-93900-9_21",

language = "English",

isbn = "978-3-540-93899-6",

volume = "5403",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "245--259",

editor = "Jones, {Neil D} and Markus M{\"u}ller-Olm",

booktitle = "Verification, Model Checking, and Abstract Interpretation",

address = "United States",

note = "10th International Conference on Verification, Model Checking, and Abstract Interpretation , VMCAI 2009 ; Conference date: 18-01-2009 Through 20-01-2009",

}

Maier, P 2009, Deciding extensions of the theories of vectors and bags. in ND 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, Lecture Notes in Computer Science, vol. 5403, Springer, pp. 245-259, 10th International Conference on Verification, Model Checking, and Abstract Interpretation , Savannah, Georgia, United States, 18/01/09. https://doi.org/10.1007/978-3-540-93900-9_21

Deciding extensions of the theories of vectors and bags. / Maier, Patrick.
Verification, Model Checking, and Abstract Interpretation: 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings. ed. / Neil D Jones; Markus Müller-Olm. Vol. 5403 Springer, 2009. p. 245-259 (Lecture Notes in Computer Science; Vol. 5403).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Deciding extensions of the theories of vectors and bags

AU - Maier, Patrick

PY - 2009

Y1 - 2009

N2 - 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.

AB - 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.

KW - verification and program analysis

KW - decision procedures

KW - vectors

KW - multisets

U2 - 10.1007/978-3-540-93900-9_21

DO - 10.1007/978-3-540-93900-9_21

M3 - Conference contribution

SN - 978-3-540-93899-6

VL - 5403

T3 - Lecture Notes in Computer Science

SP - 245

EP - 259

BT - Verification, Model Checking, and Abstract Interpretation

A2 - Jones, Neil D

A2 - Müller-Olm, Markus

PB - Springer

T2 - 10th International Conference on Verification, Model Checking, and Abstract Interpretation

Y2 - 18 January 2009 through 20 January 2009

ER -

Deciding extensions of the theories of vectors and bags

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this