Paper Info
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.
Year
DOI
Venue
2012
10.1007/978-3-642-27705-4_6
VSTTE
Keywords
Field
DocType
satisfiability problem,decidable theory,sublist set,functional list,functional program,decidability result,verification condition,list length,automated reasoning,distinct list element,extended theory,satisfiability,functional programming
Automated reasoning,Programming language,Computer science,Boolean satisfiability problem,Cardinality,Theoretical computer science,Decidability,Canonical model,Software,Operator (computer programming),Transitive relation
Conference
Volume
ISSN
Citations 
7152
0302-9743
3
PageRank 
References 
Authors
0.39
22
3
Name
Order
Citations
PageRank
Thomas Wies151528.26
Marco Muñiz2545.68
Viktor Kuncak3112970.57