Write a Blog >>
ICSE 2021
Mon 17 May - Sat 5 June 2021

One of the main challenges of reactive synthesis, an automated procedure to obtain a correct-by-construction reactive system, is to deal with unrealizable specifications. One means to deal with unrealizability, in the context of GR(1), an expressive assume-guarantee fragment of LTL that enables efficient synthesis, is the computation of an unrealizable core, which can be viewed as a fault-localization approach. Existing solutions, however, are computationally costly, are limited to computing a single core, and do not correctly support specifications with constructs beyond pure GR(1) elements.

In this work we address these limitations. First, we present QuickCore, a novel algorithm that accelerates unrealizable core computations by relying on the monotonicity of unrealizability, on an incremental computation, and on additional properties of GR(1) specifications. Second, we present Punch, a novel algorithm to efficiently compute all unrealizable cores of a specification. Finally, we present means to correctly handle specifications that include higher-level constructs beyond pure GR(1) elements.

We implemented our ideas on top of Spectra, an open-source language and synthesis environment. Our evaluation over benchmarks from the literature shows that QuickCore is in most cases faster than previous algorithms, and that its relative advantage grows with scale. Moreover, we found that most specifications include more than one core, and that Punch finds all the cores significantly faster than a competing naive algorithm.

Conference Day
Fri 28 May

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

15:05 - 16:05
4.3.1. Analyzing System Properties: Correctness, Determinism, RealizabilityTechnical Track at Blended Sessions Room 1 +12h
Chair(s): Maria Teresa BaldassarreDepartment of Computer Science, University of Bari
15:05
20m
Paper
JEST: N+1-version Differential Testing of Both JavaScript Engines and SpecificationACM SIGSOFT Distinguished PaperArtifact ReusableTechnical TrackArtifact Available
Technical Track
Pre-print Media Attached
15:25
20m
Paper
Unrealizable Cores for Reactive Systems SpecificationsArtifact ReusableTechnical Track
Technical Track
Shahar MaozTel Aviv University, Israel, Rafi ShalomTel Aviv University, Israel
Pre-print
15:45
20m
Paper
Verifying Determinism in Sequential ProgramsArtifact ReusableTechnical Track
Technical Track
Rashmi MudduluruUniversity of Washington, Jason WaatajaUW CSE, Suzanne MillsteinUniversity of Washington, Michael D. ErnstUW CSE
Pre-print

Conference Day
Sat 29 May

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

03:05 - 04:05
4.3.1. Analyzing System Properties: Correctness, Determinism, RealizabilityTechnical Track at Blended Sessions Room 1
03:05
20m
Paper
JEST: N+1-version Differential Testing of Both JavaScript Engines and SpecificationACM SIGSOFT Distinguished PaperArtifact ReusableTechnical TrackArtifact Available
Technical Track
Pre-print Media Attached
03:25
20m
Paper
Unrealizable Cores for Reactive Systems SpecificationsArtifact ReusableTechnical Track
Technical Track
Shahar MaozTel Aviv University, Israel, Rafi ShalomTel Aviv University, Israel
Pre-print
03:45
20m
Paper
Verifying Determinism in Sequential ProgramsArtifact ReusableTechnical Track
Technical Track
Rashmi MudduluruUniversity of Washington, Jason WaatajaUW CSE, Suzanne MillsteinUniversity of Washington, Michael D. ErnstUW CSE
Pre-print