We analyze the bounded reachability problem of programs that use abstract data types and set comprehensions. Such programs are common as high-level executable specifications of complex protocols. We prove decidability and undecidability results of restricted cases of the problem and extend the Satisfiability Modulo Theories approach to support analysis of set comprehensions over tuples and bag axioms. We use the Z3 solver for our implementation and experiments, and we use AsmL as the modeling language. © 2008 Springer Berlin Heidelberg.
CITATION STYLE
Veanes, M., & Saabas, A. (2008). On bounded reachability of programs with set comprehensions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5330 LNAI, pp. 305–317). https://doi.org/10.1007/978-3-540-89439-1_22
Mendeley helps you to discover research relevant for your work.