Kuncak, ViktorRaya, Rodrigo2023-06-052023-06-05202310.5075/epfl-thesis-10546https://infoscience.epfl.ch/handle/20.500.14299/198135We study the decision problem for the existential fragment of the theory of power structures. We prove complexity results that parallel the decidability results of Feferman-Vaught for the theories of product structures thereby showing that the construction of Hintikka formulae is not necessary in the quantifier-free case. We show that the result stays true when the theory of the indices is enriched with a finiteness or an order predicate. We prove that the resulting logical fragment gives quantifier-free logics suitable for verification. We conclude by applying the developed techniques to the existential fragment of the theory of non-linear integer arithmetic and the theory of arrays.enLogicComputer Sciencethesis::doctoral thesis