This paper tackles the problem of synthesizing specifications for nondeterministic programs. For such programs, useful specifications can capture demonic properties, which hold for \emph{every} nondeterministic execution, but also angelic properties, which hold for \emph{some} nondeterministic execution. We build on top of a recently proposed a framework by Park et al. in which given (i) a \textit{quantifier-free} query $\Psi$ posed about a set of function definitions (i.e., the behavior for which we want to generate a specification), and (ii) a language $\mathcal{L}$ in which each extracted property is to be expressed (we call properties in the language $\mathcal{L}$-properties), the goal is to synthesize a conjunction $\bigwedge_i \varphi_i$ of $\mathcal{L}$-properties such that each of the $\varphi_i$ is a \emph{strongest $\mathcal{L}$-consequence} for $\Psi$: $\varphi_i$ is an over-approximation of $\Psi$ and there is no other $\mathcal{L}$-property that over-approximates $\Psi$ and is strictly more precise than $\varphi_i$. This framework does not apply to nondeterministic programs for two reasons: it does not support existential quantifiers in queries (which are necessary to expressing nondeterminism) and it can only compute $\mathcal{L}$-consequences, i.e., it is unsuitable for capturing both angelic and demonic properties.

This paper addresses these two limitations and presents a framework, LOUD, for synthesizing both \emph{strongest $\mathcal{L}$-consequences} and \emph{weakest $\mathcal{L}$-implicants} (i.e., under-approximations of the query $\Psi$) for queries that can involve \textit{existential quantifiers}. We implement a solver, ASPIRE, for problems expressed in LOUD which can be used to describe and identify sources of bugs in both deterministic and nondeterministic programs, extract properties from concurrent programs, and synthesize winning strategies in two-player games.