2020/01/14 by José Fragoso Santos, Petar Maksimović, Santos, José Fragoso +5 · 1 citation
Chemistry · Computer Science · #Chemical synthesis and alkaloids #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Programming Languages (cs.PL) #Security and Verification in Computing
paper · pdf · doi:10.48550/arxiv.2001.05059
openalex publication_date 2020/01/14 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.