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

### Citation

Thomas Wies, Marco Mu niz, and Viktor Kuncak.
On deciding functional lists with sublist sets.
Technical Report EPFL-REPORT-148361, EPFL, April 2010.### BibTex Entry

@techreport{WiesETAL10DecidingFunctionalListswithSublistSets,
author = {Thomas Wies and Marco Mu\~niz and Viktor Kuncak},
title = {On Deciding Functional Lists with Sublist Sets},
institution = {EPFL},
year = 2010,
number = {EPFL-REPORT-148361},
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.},
month = {April}
}