arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 2001.05059cs.PLcs.LO

Gillian: Compositional Symbolic Execution for All

José Fragoso Santos, Petar Maksimović, Sacha-Élie Ayoun, Philippa Gardner

英文摘要:

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.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑