Blogs (1) >>
ICSE 2019
Sat 25 - Fri 31 May 2019 Montreal, QC, Canada
Fri 31 May 2019 14:20 - 14:40 at Van-Horne - Specifications and Models Chair(s): Sylvain Hallé

Unrealizability is a major challenge for GR(1), an expressive assume-guarantee fragment of LTL that enables efficient synthesis. Some works attempt to help engineers deal with unrealizability by generating counter-strategies or computing an unrealizable core. Other works propose to repair the unrealizable specification by suggesting repairs in the form of automatically generated assumptions.

In this work we present two novel symbolic algorithms for repairing unrealizable GR(1) specifications. The first algorithm infers new assumptions based on the recently introduced JVTS. The second algorithm infers new assumptions directly from the specification. Both algorithms are sound. The first is incomplete but can be used to suggest many different repairs. The second is complete but suggests a single repair. Both are symbolic and therefore efficient.

We implemented our work, validated its correctness, and evaluated it on benchmarks from the literature. The evaluation shows the strength of our algorithms, in their ability to suggest repairs and in their performance and scalability compared to previous solutions.

Conference Day
Fri 31 May

Displayed time zone: Eastern Time (US & Canada) change

14:00 - 15:30
Specifications and ModelsPapers / Demonstrations / Technical Track at Van-Horne
Chair(s): Sylvain HalléUniversité du Québec à Chicoutimi, Canada
14:00
20m
Talk
PsALM: Specification of Dependable Robotic MissionsDemos
Demonstrations
Claudio MenghiUniversity of Luxembourg, SnT, Christos TsigkanosTechnische Universität Wien, Thorsten BergerChalmers University of Technology, Sweden / University of Gothenburg, Sweden, Patrizio PelliccioneChalmers | University of Gothenburg and University of L'Aquila
14:20
20m
Talk
Symbolic Repairs for GR(1) SpecificationsArtifacts Evaluated ReusableTechnical Track
Technical Track
Shahar MaozTel Aviv University, Jan Oliver RingertTel Aviv University, Rafi ShalomTel Aviv University
14:40
20m
Talk
ARepair: A Repair Framework for AlloyDemos
Demonstrations
Kaiyuan WangGoogle, Inc., Allison SullivanNorth Carolina Agriculture and Technical State University, Sarfraz KhurshidUniversity of Texas at Austin
15:00
20m
Talk
Visual Debugging of Behavioural ModelsDemos
Demonstrations
Gianluca BarbonUniversité Grenoble Alpes, Inria, LIG, Vincent LeroyUniversity of Grenoble - CNRS, Gwen SalaünUniversity of Grenoble Alpes, Emmanuel YahUniversité Grenoble Alpes
15:20
10m
Talk
Discussion Period
Papers