In this article, we empirically study the suitability of tests as acceptance criteria for automated program fixes, by checking patches produced by automated repair tools using a bug-finding tool, as opposed to previous works that used tests or manual inspections. We develop a number of experiments in which faulty programs from IntroClass , a known benchmark for program repair techniques, are fed to the program repair tools GenProg, Angelix, AutoFix, and Nopol, using test suites of varying quality, including those accompanying the benchmark. We then check the produced patches against formal specifications using a bug-finding tool. Our results show that, in the studied scenarios, automated program repair tools are significantly more likely to accept a spurious program fix than producing an actual one. Using bounded-exhaustive suites larger than the originally given ones (with about 100 and 1,000 tests) we verify that overfitting is reduced but (a) few new correct repairs are generated and (b) some tools see their performance reduced by the larger suites and fewer correct repairs are produced. Finally, by comparing with previous work, we show that overfitting is underestimated in semantics-based tools and that patches not discarded using held-out tests may be discarded using a bug-finding tool.

Alloyis a formal specification language, which despite featuring a simple syntax and relational semantics, is very expressive and supports efficient automated specification analysis, based on SAT solving. While the language is sufficiently expressive to accommodate bothstaticanddynamicproperties of systems within specifications, the latter kind of properties require intricate, ad-hoc, constructions to encode system executions. Thus, extensions to the language have been proposed, that internalize these encodings and provide analysis techniques, specifically tailored to properties of executions. In this paper we study two particular extensions toAlloythat incorporate elements for the specification of properties of executions. These areDynAlloy, whose syntax and semantics are inspired by dynamic logic, andElectrum, based on linear-time temporal logic and inspired by languages such asTLA+. We analyze and compare the syntactic characteristics of the languages, their corresponding expressiveness, and the effectiveness and efficiency of their associated analysis tools. The comparison is based on a set ofAlloyspecifications that are taken from the literature and demand dynamic behavior analysis, including anAlloymodel of the Chord ring-maintenance protocol, that drives our qualitative comparison of the notations.

Formal specifications in Alloy are organized around user-defined data domains, associated with signatures, with almost no support for built-in datatypes. This minimality in the built-in datatypes provided by the language is one of its main features, as it contributes to the automated analyzability of models. One of the few built-in datatypes available in Alloy specifications are integers, whose SAT-based treatment allows only for small bit-widths. In many contexts, where relational datatypes dominate, the use of integers may be auxiliary, e.g., in the use of cardinality constraints and other features. However, as the applications of Alloy are increased, e.g., with the use of the language and its tool support as backend engine for different analysis tasks, the provision of efficient support for numerical datatypes becomes a need. In this work, we present our current preliminary approach to providing an efficient, scalable and user-friendly extension to Alloy, with arithmetic support for numerical datatypes. Our implementation allows for arithmetic with varying precisions, and is implemented via standard Alloy constructions, thus resorting to SAT solving for resolving arithmetic constraints in models.

We describe DynAlloy Analyzer, a tool that extends Alloy Analyzer with support for dynamic elements in Alloy models. The tool builds upon Alloy Analyzer in a way that makes it fully compatible with Alloy models, and extends their syntax with a particular idiom, inspired in dynamic logic, for the description of dynamic behaviours, understood as sequences of states over standard Alloy models, in terms of programs. The syntax is broad enough to accommodate abstract dynamic behaviours, e.g., using nondeterministic choice and finite unbounded iteration, as well as more concrete ones, using standard sequential programming constructions. The analysis of DynAlloy models resorts to the analysis of Alloy models, through an optimized translation that often makes the analysis more efficient than that of typical ad-hoc constructions to capture dynamism in Alloy.