Deciding functional lists with sublist sets

Thomas Wies, Marco Muñiz, Viktor Kuncak

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

Abstract

Motivated by the problem of deciding verification conditions for the verification of functional programs, we present new decision procedures for automated reasoning about functional lists. We first show how to decide in NP the satisfiability problem for logical constraints containing equality, constructor, selectors, as well as the transitive sublist relation. We then extend this class of constraints with operators to compute the set of all sublists, and the set of objects stored in a list. Finally, we support constraints on sizes of sets, which gives us the ability to compute list length as well as the number of distinct list elements. We show that the extended theory is reducible to the theory of sets with linear cardinality constraints, and therefore still in NP. This reduction enables us to combine our theory with other decidable theories that impose constraints on sets of objects, which further increases the potential of our decidability result in verification of functional and imperative software.

Original languageEnglish (US)
Title of host publicationVerified Software: Theories, Tools, Experiments - 4th International Conference, VSTTE 2012, Proceedings
Pages66-81
Number of pages16
Volume7152 LNCS
DOIs
StatePublished - 2012
Event4th International Conference on Verified Software: Theories, Tool and Experiments, VSTTE 2012 - Philadelphia, PA, United States
Duration: Jan 28 2012Jan 29 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7152 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other4th International Conference on Verified Software: Theories, Tool and Experiments, VSTTE 2012
CountryUnited States
CityPhiladelphia, PA
Period1/28/121/29/12

Fingerprint

Computability and decidability
Cardinality Constraints
Automated Reasoning
Selector
Satisfiability Problem
Decision Procedures
Equality Constraints
Linear Constraints
Decidability
Distinct
Software
Operator
Object
Class

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Wies, T., Muñiz, M., & Kuncak, V. (2012). Deciding functional lists with sublist sets. In Verified Software: Theories, Tools, Experiments - 4th International Conference, VSTTE 2012, Proceedings (Vol. 7152 LNCS, pp. 66-81). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7152 LNCS). https://doi.org/10.1007/978-3-642-27705-4_6

Deciding functional lists with sublist sets. / Wies, Thomas; Muñiz, Marco; Kuncak, Viktor.

Verified Software: Theories, Tools, Experiments - 4th International Conference, VSTTE 2012, Proceedings. Vol. 7152 LNCS 2012. p. 66-81 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7152 LNCS).

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

Wies, T, Muñiz, M & Kuncak, V 2012, Deciding functional lists with sublist sets. in Verified Software: Theories, Tools, Experiments - 4th International Conference, VSTTE 2012, Proceedings. vol. 7152 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7152 LNCS, pp. 66-81, 4th International Conference on Verified Software: Theories, Tool and Experiments, VSTTE 2012, Philadelphia, PA, United States, 1/28/12. https://doi.org/10.1007/978-3-642-27705-4_6
Wies T, Muñiz M, Kuncak V. Deciding functional lists with sublist sets. In Verified Software: Theories, Tools, Experiments - 4th International Conference, VSTTE 2012, Proceedings. Vol. 7152 LNCS. 2012. p. 66-81. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-27705-4_6
Wies, Thomas ; Muñiz, Marco ; Kuncak, Viktor. / Deciding functional lists with sublist sets. Verified Software: Theories, Tools, Experiments - 4th International Conference, VSTTE 2012, Proceedings. Vol. 7152 LNCS 2012. pp. 66-81 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{c718b263f66b486cb0a6c9cec43180ec,
title = "Deciding functional lists with sublist sets",
abstract = "Motivated by the problem of deciding verification conditions for the verification of functional programs, we present new decision procedures for automated reasoning about functional lists. We first show how to decide in NP the satisfiability problem for logical constraints containing equality, constructor, selectors, as well as the transitive sublist relation. We then extend this class of constraints with operators to compute the set of all sublists, and the set of objects stored in a list. Finally, we support constraints on sizes of sets, which gives us the ability to compute list length as well as the number of distinct list elements. We show that the extended theory is reducible to the theory of sets with linear cardinality constraints, and therefore still in NP. This reduction enables us to combine our theory with other decidable theories that impose constraints on sets of objects, which further increases the potential of our decidability result in verification of functional and imperative software.",
author = "Thomas Wies and Marco Mu{\~n}iz and Viktor Kuncak",
year = "2012",
doi = "10.1007/978-3-642-27705-4_6",
language = "English (US)",
isbn = "9783642277047",
volume = "7152 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "66--81",
booktitle = "Verified Software: Theories, Tools, Experiments - 4th International Conference, VSTTE 2012, Proceedings",

}

TY - GEN

T1 - Deciding functional lists with sublist sets

AU - Wies, Thomas

AU - Muñiz, Marco

AU - Kuncak, Viktor

PY - 2012

Y1 - 2012

N2 - Motivated by the problem of deciding verification conditions for the verification of functional programs, we present new decision procedures for automated reasoning about functional lists. We first show how to decide in NP the satisfiability problem for logical constraints containing equality, constructor, selectors, as well as the transitive sublist relation. We then extend this class of constraints with operators to compute the set of all sublists, and the set of objects stored in a list. Finally, we support constraints on sizes of sets, which gives us the ability to compute list length as well as the number of distinct list elements. We show that the extended theory is reducible to the theory of sets with linear cardinality constraints, and therefore still in NP. This reduction enables us to combine our theory with other decidable theories that impose constraints on sets of objects, which further increases the potential of our decidability result in verification of functional and imperative software.

AB - Motivated by the problem of deciding verification conditions for the verification of functional programs, we present new decision procedures for automated reasoning about functional lists. We first show how to decide in NP the satisfiability problem for logical constraints containing equality, constructor, selectors, as well as the transitive sublist relation. We then extend this class of constraints with operators to compute the set of all sublists, and the set of objects stored in a list. Finally, we support constraints on sizes of sets, which gives us the ability to compute list length as well as the number of distinct list elements. We show that the extended theory is reducible to the theory of sets with linear cardinality constraints, and therefore still in NP. This reduction enables us to combine our theory with other decidable theories that impose constraints on sets of objects, which further increases the potential of our decidability result in verification of functional and imperative software.

UR - http://www.scopus.com/inward/record.url?scp=84856530571&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84856530571&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-27705-4_6

DO - 10.1007/978-3-642-27705-4_6

M3 - Conference contribution

SN - 9783642277047

VL - 7152 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 66

EP - 81

BT - Verified Software: Theories, Tools, Experiments - 4th International Conference, VSTTE 2012, Proceedings

ER -