Automated logic circuit design enhances chip performance, energy efficiency, and reliability, with applications in model-checking, reactive synthesis, and hyperproperty verification. AIGER circuits are a standard format for these domains, used in hardware model-checking, synthesis competitions such as Syntcomp, symbolic synthesis algorithms, and the verification of security properties in neural networks and safety-critical systems. Traditionally, AIGER circuits are generated from Linear Temporal Logic (LTL) specifications through complex pipelines, such as translating LTL to SMV or to automata and then to AIGER. These pipelines guarantee functional equivalence but produce large circuits with auto-generated labels that obscure the specification’s meaning. In applications like symbolic reactive synthesis, model-checking, and neural network verification, understanding latches and outputs is critical for debugging and tool improvement. In this tool paper, we introduce AIGLE, a novel tool that generates compact AIGER circuits directly from LTL[X] or Past-LTL specifications. Our approach uses linear-size translation from LTL[X] to Past-LTL, which produces highly legible circuits. Compared to tools like py-aiger, our tool reduces gate counts-—often by thousands-— improving readability and synthesis speed. Our empirical evaluation demonstrates smaller, more understandable circuits and faster synthesis, offering a scalable, engineer-friendly solution for formal methods applications.

Abstract System goals are the statements that, in the context of software requirements specification, capture how the software should behave. Many times, the understanding of stakeholders on what the system should do, as captured in the goals, can lead to different problems, from clearly contradicting goals, to more subtle situations in which the satisfaction of some goals inhibits the satisfaction of others. These latter issues, calledgoal divergences, are the subject ofgoal conflict analysis, which consists of identifying, assessing, and resolving divergences, as part of a more general activity known as goal refinement. While there exist techniques that, when requirements are expressed formally, can automatically identify and assess goal conflicts, there is currently no automated approach to support engineers inresolvingidentified divergences. In this paper, we presentACoRe, the first approach that automatically proposes potential resolutions to goal conflicts, in requirements specifications formally captured using linear-time temporal logic.ACoResystematically explores syntactic modifications of the conflicting specifications, aiming at obtaining resolutions that disable previously identified conflicts, while preserving specification consistency.ACoReintegrates modern multi-objective search algorithms (in particular, NSGA-III, WBGA, and AMOSA) to produce resolutions that maintain coherence with the original conflicting specification, by searching for specifications that are eithersyntacticallyorsemanticallysimilar to the original specification. We assessACoReon 25 requirements specifications taken from the literature. We show thatACoRecan successfully produce various conflict resolutions for each of the analyzed case studies, including resolutions that resemble specification repairs manually provided as part of conflict analyses.

The reactive synthesis problem consists of automatically producing correct-by-construction operational models of systems from high-level formal specifications of their behaviours. However, specifications are often unrealisable, meaning that no system can be synthesised from the specification. To deal with this problem, we present AuRUS, a search-based approach to repair unrealisable Linear-Time Temporal Logic (LTL) specifications. AuRUS aims at generating solutions that are similar to the original specifications by using the notions of syntactic and semantic similarities. Intuitively, the syntactic similarity measures the text similarity between the specifications, while the semantic similarity measures the number of behaviours preserved/removed by the candidate repair. We propose a new heuristic based on model counting to approximate semantic similarity. We empirically assess AuRUS on many unrealisable specifications taken from different benchmarks and show that it can successfully repair all of them. Also, compared to related techniques, AuRUS can produce many unique solutions while showing more scalability.