Demo Data from SIGIR 2026 / reviewers in the wild / expert
Shachaf Cohen
dblp:436/3931
· DBLP profile ↗
1ranked-venue papers
1as first author
1since 2021 · last 2026
—ORCID · none
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 1 · 1 first-author · 1 since 2021Theory of computation · 1 · 1 first-author · 1 since 2021
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Theoretical computer science
1 paper |
Automated reasoning and model checking · 100% |
Topics — the 2 heaviest of 2, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Automated reasoning and model checking › reactive synthesis
GR(1) synthesis |
1.0 | 1 | 2026 | Performance Heuristics for GR(1) Unrealizable Core Computation · FM (2) 2026 |
Automated reasoning and model checking
reactive synthesis |
1.0 | 1 | 2026 | Performance Heuristics for GR(1) Unrealizable Core Computation · FM (2) 2026 |
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2026 | Performance Heuristics for GR(1) Unrealizable Core ComputationabstractAbstract A major challenge of reactive synthesis, an automated process for deriving correct-by-construction reactive systems from temporal specifications, is debugging unrealizable specifications. One way to debug them in the context of GR(1), an LTL fragment that balances efficient synthesis complexity and expressiveness, is the computation of unrealizable cores. Although work has been done to accelerate core computation, it remains a costly operation, despite being commonly used during specification development. In this paper, we first examine a version of the existing core computation algorithm, where we replace the classic algorithm with , a state-of-the-art domain-agnostic minimization algorithm. Then, we present two novel GR(1)-specific heuristics to improve the core computation time by exploiting attributes of the realizability checking algorithm. These heuristics include (1) quickly discarding unneeded justice guarantees, and (2) reusing realizability check results to make subsequent checks faster. We implemented our work on top of the Spectra language and synthesizer and evaluated it over hundreds of specifications. Our evaluation shows that while using CDD in our context was ineffective, the new heuristics improve core computation times for 80% of the specifications, with an average improvement of more than three times compared to the baseline algorithm. Shachaf Cohen, Shahar Maoz |
FM (2) | 1 |