Writing formal specifications is an important yet challenging aspect of software engineering. Correct specifications facilitate verification efforts and reduce bugs. However, the declarative nature of specifications differs from the imperative approach of most common programming languages, and software engineers often perceive formal methods as difficult. Arguably, guidelines and tools for writing readable specifications should lower the barrier to formal methods adoption. In this work, we focus on Boolean formulas, a fundamental building block of specifications. Analogous to research on code comprehension, we conducted an experiment that attempts to identify what properties affect Boolean formula comprehension by software engineers. To this end, we collected 59 representative Boolean formulas and tested how various syntactic properties, such as negation symbol count and nesting level, affect comprehension task response times and correctness. Our experiment with 181 participants shows that eliminating negation symbols and decreasing operator count are among the most significant factors that improve comprehension. We use these empirical results to derive a reading complexity score and develop a fast regression-based refactoring algorithm for Boolean formulas. Finally, we conducted a follow-up experiment with 57 participants, which provided strong evidence for the algorithm’s effectiveness in improving comprehension.

Abstract Reactive synthesis is an automated process for deriving correct-by-construction reactive systems from temporal specifications. GR(1), in particular, is a popular LTL fragment that balances efficient synthesis complexity and expressiveness. In this paper, we present a set of novel heuristics to further improve the performance of GR(1) realizability checking and related algorithms, motivated by several observations. These heuristics include (1) discarding intermediate memory not required for many GR(1) algorithms, (2) setting good initial orders of variables and justice constraints, (3) improving the embedding of finite automata into GR(1) when supporting advanced language constructs, and (4) algorithm-specific heuristics for additional GR(1) analyses such as non-well-separation and inherent vacuity detection. We implemented these heuristics in the Spectra synthesizer, and extensively validated and evaluated them on well-known benchmarks consisting of hundreds of specifications. Our results show major performance gains, in particular, an average of realizability checking at least two times faster than the baseline.

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. GR(1) is an expressive assume-guarantee fragment of LTL that enables efficient synthesis and has been recently used in different contexts and application domains.