  We present Gillian, a language-independent framework for the development of
compositional symbolic analysis tools. Gillian supports three flavours of
analysis: whole-program symbolic testing, full verification, and bi-abduction.
It comes with fully parametric meta-theoretical results and a modular
implementation, designed to minimise the instantiation effort required of the
user. We evaluate Gillian by instantiating it to JavaScript and C, and perform
its analyses on a set of data-structure libraries, obtaining results that
indicate that Gillian is robust enough to reason about real-world programming
languages.
