Abstract Non-well-separation is a common quality issue in reactive synthesis specifications, where the synthesized system can avoid satisfying its guarantees by preventing the environment from satisfying its assumptions. Kind realizability extends the usual GR(1) by additionally requiring the system to always enable the environment to satisfy its assumptions, thereby addressing this issue, and is expected to replace the usual GR(1) realizability checking. Kind realizability relies on a reduction and a 4-nested fixed-point algorithm, whose runtime typically exceeds that of the usual GR(1) realizability checking algorithm by more than 3 times, creating a significant performance bottleneck in specification development processes that require frequent realizability checks. This paper presents a framework designed to accelerate kind realizability checking, comprising: (1) a multi-level incremental checking framework that sequentially integrates approximate computation with the complete 4FP algorithm, reusing previously computed sound bounds at each stage to eliminate redundant state-space exploration; and (2) two accompanying approximation algorithms with lower asymptotic time complexity, which efficiently compute sound upper and lower bounds of the system winning region. Experiments on benchmarks comprising hundreds of specifications demonstrate significant performance improvements.

Although reactive synthesis guarantees correct-by-construction implementations, its practical adoption is limited by a performance bottleneck in the iterative design-and-refinement cycle of formal specifications. GR(1) synthesizers perform redundant, from-scratch computations for each specification modification, severely slowing the development workflow. To address this inefficiency, we propose an incremental synthesis method that exploits the monotonicity of the underlying fixed-point computations. By reusing the system winning region from the preceding check, our method significantly accelerates realizability check. Our work applies an incremental method to iterative GR(1) specification development covering the full GR(1) scope, including system guarantees and environment assumptions, to accelerate realizability checking. Furthermore, we introduce two heuristics for early fixed-point detection during incremental realizability checking. Finally, we analyze why prior work failed to integrate an incremental technique limited to system guarantees into the unrealizable core minimization algorithm DDMin , further establishing iterative development as a suitable application setting for incremental methods. Evaluated on a large-scale benchmark of 8,282 specifications, our method exhibits a strong positive correlation between performance gain and specification complexity. For the most challenging specifications, which constitute the primary bottlenecks in development, our approach achieves speedups of several orders of magnitude, reducing computation times in some cases from nearly an hour to just seconds.

Unit testing, as a critical means of ensuring software quality, is often constrained in practice by the high cost and low efficiency of manual test case construction, resulting in limited test coverage and scarcity of unit test cases in real-world projects. Traditional test generation tools can improve coverage but suffer from poor readability and limited generalization. In recent years, large language models (LLMs) have demonstrated strong potential in the field of test generation, owing to their powerful generalization and reasoning capabilities. However, the static nature of training data often causes hallucinations, undermining the reliability of generated tests. To address this, we propose MUATC, a multi-agent unit test generation framework based on LLMs. This work introduces, for the first time in coverage-driven LLM-based test generation, a multi-agent collaborative mechanism that integrates Chain-of-Thought reasoning and Retrieval-Augmented Generation to enhance both the quality and coverage of generated test cases. Additionally, we propose a unit test repair algorithm MTCRA aimed at further improving test coverage. The experimental results show that MUATC achieves 4.8%–5.5% higher coverage than Coverup, with performance gains independent of model architecture and programming languages. Compared with advanced LLM-based coverage enhancement tools such as ChatUniTest, TestPilot and Coverup, MUATC achieves a 12.7% improvement in test coverage on the benchmark dataset provided by ChatUniTest. To demonstrate the superior readability of test cases generated by MUATC, we conducted a readability study via the HumanEval platform. The results indicate that MUATC-generated test cases are significantly more readable than those produced by Pynguin. Therefore, to leverage the high readability of generated test cases, we also develop UnitTestPlat, a user-oriented platform for visualized unit test generation.