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
AN - SCOPUS:84856530571
SN - 9783642277047
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
T2 - 4th International Conference on Verified Software: Theories, Tool and Experiments, VSTTE 2012
Y2 - 28 January 2012 through 29 January 2012
ER -