Vacuity is a well-known quality issue in formal specifications, studied mostly in the context of model checking. Inherent vacuity is a type of vacuity that applies to specifications, without the context of a model. GR(1) is an expressive assume-guarantee fragment of LTL, which enables efficient symbolic synthesis.
In this work we investigate inherent vacuity for GR(1) specifications. We define several general types of inherent vacuity for GR(1), including specification element vacuity and domain value vacuity. We detect vacuities using a reduction to LTL satisfiability, specialized for the context of GR(1). We further extend vacuity detection to handle GR(1) specifications that are enriched with past LTL, monitors, and patterns. Finally, we define a novel notion of vacuity core, which provides means to localize the cause of vacuity.
We implemented our work and evaluated it on benchmarks from the literature. The evaluation shows that vacuities are indeed common in GR(1) specifications, and that we are able to efficiently detect them and effectively localize their causes. Moreover, our evaluation shows that removal of vacuous specification elements may significantly reduce synthesis time.
Thu 12 NovDisplayed time zone: (UTC) Coordinated Universal Time change
08:30 - 09:00 | |||
08:30 2mTalk | Domain-Independent Interprocedural Program Analysis using Block-Abstraction Memoization Research Papers DOI Pre-print Media Attached | ||
08:33 1mTalk | Inherent Vacuity for GR(1) Specifications Research Papers DOI | ||
08:35 1mTalk | Interval Counterexamples for Loop Invariant Learning Research Papers DOI | ||
08:37 1mTalk | Modular Collaborative Program Analysis in OPAL Research Papers Dominik Helm TU Darmstadt, Germany, Florian Kübler TU Darmstadt, Germany, Michael Reif TU Darmstadt, Germany, Michael Eichberg TU Darmstadt, Germany, Mira Mezini TU Darmstadt, Germany DOI | ||
08:39 1mTalk | Past-Sensitive Pointer Analysis for Symbolic Execution Research Papers David Trabish Tel Aviv University, Israel, Timotej Kapus Imperial College London, UK, Noam Rinetzky Tel Aviv University, Cristian Cadar Imperial College London, UK DOI Pre-print Media Attached | ||
08:41 19mTalk | Conversations on Analysis 4 Paper Presentations David Trabish Tel Aviv University, Israel, Dominik Helm TU Darmstadt, Germany, Rafi Shalom Tel Aviv University, Israel, Rongchen Xu Tsinghua University, China, Shahar Maoz Tel Aviv University, Israel, M: Rachel Tzoref-Brill IBM Research |