  The rising popularity of declarative languages and the hard to debug nature
thereof have motivated the need for applicable, automated repair techniques for
such languages. However, despite significant advances in the program repair of
imperative languages, there is a dearth of repair techniques for declarative
languages. This paper presents BeAFix, an automated repair technique for faulty
models written in Alloy, a declarative language based on first-order relational
logic. BeAFix is backed with a novel strategy for bounded exhaustive, yet
scalable, exploration of the spaces of fix candidates and a formally rigorous,
sound pruning of such spaces. Moreover, different from the state-of-the-art in
Alloy automated repair, that relies on the availability of unit tests, BeAFix
does not require tests and can work with assertions that are naturally used in
formal declarative languages. Our experience with using BeAFix to repair
thousands of realworld faulty models, collected by other researchers,
corroborates its ability to effectively generate correct repairs and outperform
the state-of-the-art.
