Write a Blog >>
ESEC/FSE 2022
Mon 14 - Fri 18 November 2022 Singapore
Tue 15 Nov 2022 10:45 - 11:00 at SRC LT 52 - ESEC/FSE 20 Program Analysis I Chair(s): Haipeng Cai

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.

Tue 15 Nov

Displayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change

10:45 - 12:15
ESEC/FSE 20 Program Analysis IESEC/FSE 2020 at SRC LT 52
Chair(s): Haipeng Cai Washington State University
10:45
15m
Talk
Inherent Vacuity for GR(1) Specifications
ESEC/FSE 2020
Shahar Maoz Tel Aviv University, Israel, Rafi Shalom Tel Aviv University, Israel
Link to publication DOI
11:00
15m
Talk
Mining Input Grammars from Dynamic Control Flow
ESEC/FSE 2020
Rahul Gopinath University of Sydney, Björn Mathis CISPA, Germany, Andreas Zeller CISPA Helmholtz Center for Information Security
Link to publication DOI
11:15
15m
Talk
Flexeme: Untangling Commits Using Lexical Flows
ESEC/FSE 2020
Profir-Petru Pârțachi National Institute of Informatics, Japan, Santanu Dash University of Surrey, UK, Miltiadis Allamanis Microsoft Research, Earl T. Barr University College London
DOI Pre-print
11:30
15m
Talk
Past-Sensitive Pointer Analysis for Symbolic Execution
ESEC/FSE 2020
David Trabish Tel Aviv University, Timotej Kapus Imperial College London, UK, Noam Rinetzky Tel Aviv University, Cristian Cadar Imperial College London, UK
11:45
15m
Talk
TypeWriter: Neural Type Prediction with Search-Based Validation
ESEC/FSE 2020
Michael Pradel University of Stuttgart, Georgios Gousios Endor Labs & Delft University of Technology, Jason Liu Facebook, USA, Satish Chandra Meta Platforms
12:00
15m
Talk
Domain-Independent Interprocedural Program Analysis using Block-Abstraction Memoization
ESEC/FSE 2020
Dirk Beyer LMU Munich, Karlheinz Friedberger LMU Munich, Germany
DOI Media Attached