Write a Blog >>
Thu 12 Nov 2020 08:33 - 08:34 at Virtual room 1 - Analysis 4

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.

Conference Day
Thu 12 Nov

Displayed time zone: (UTC) Coordinated Universal Time change

08:30 - 09:00
08:30
2m
Talk
Domain-Independent Interprocedural Program Analysis using Block-Abstraction Memoization
Research Papers
Dirk BeyerLMU Munich, Germany, Karlheinz FriedbergerLMU Munich, Germany
DOI Pre-print Media Attached
08:33
1m
Talk
Inherent Vacuity for GR(1) Specifications
Research Papers
Shahar MaozTel Aviv University, Israel, Rafi ShalomTel Aviv University, Israel
DOI
08:35
1m
Talk
Interval Counterexamples for Loop Invariant Learning
Research Papers
Rongchen XuTsinghua University, China, Fei HeTsinghua University, Bow-Yaw WangAcademia Sinica
DOI
08:37
1m
Talk
Modular Collaborative Program Analysis in OPAL
Research Papers
Dominik HelmTU Darmstadt, Germany, Florian K├╝blerTU Darmstadt, Germany, Michael ReifTU Darmstadt, Germany, Michael EichbergTU Darmstadt, Germany, Mira MeziniTU Darmstadt, Germany
DOI
08:39
1m
Talk
Past-Sensitive Pointer Analysis for Symbolic Execution
Research Papers
David TrabishTel Aviv University, Israel, Timotej KapusImperial College London, UK, Noam RinetzkyTel Aviv University, Cristian CadarImperial College London, UK
DOI Pre-print Media Attached
08:41
19m
Talk
Conversations on Analysis 4
Paper Presentations
David TrabishTel Aviv University, Israel, Dominik HelmTU Darmstadt, Germany, Rafi ShalomTel Aviv University, Israel, Rongchen XuTsinghua University, China, Shahar MaozTel Aviv University, Israel, M: Rachel Tzoref-BrillIBM Research