We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Software Engineering

Title: Bounded Exhaustive Search of Alloy Specification Repairs

Abstract: 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.
Comments: 13 pages, ICSE 2021
Subjects: Software Engineering (cs.SE)
Cite as: arXiv:2103.00327 [cs.SE]
  (or arXiv:2103.00327v1 [cs.SE] for this version)

Submission history

From: Simón Emmanuel Gutiérrez Brida [view email]
[v1] Sat, 27 Feb 2021 21:28:34 GMT (122kb)

Link back to: arXiv, form interface, contact.