Bounded exhaustive search of alloy specification repairs
"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 technique...
Autores principales: | , , , , , , |
---|---|
Formato: | Ponencias en Congresos acceptedVersion |
Lenguaje: | Inglés |
Publicado: |
2022
|
Materias: | |
Acceso en línea: | http://ri.itba.edu.ar/handle/123456789/3900 |
Aporte de: |
id |
I32-R138-123456789-3900 |
---|---|
record_format |
dspace |
spelling |
I32-R138-123456789-39002022-12-07T14:13:44Z Bounded exhaustive search of alloy specification repairs Gutiérrez Brida, Simón Regis, Germán Zheng, Guolong Bagher, Hamid Nguyen, Thanh Vu Aguirre, Nazareno Frías, Marcelo LENGUAJES DE PROGRAMACION AUTOMATIZACION REPARACIONES "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, ex ploration 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 real world faulty models, collected by other researchers, corroborates its ability to effectively generate correct repairs and outperform the state-of-the-art." 2022-05-31T18:54:49Z 2022-05-31T18:54:49Z 2021 Ponencias en Congresos info:eu-repo/semantics/acceptedVersion 13-978-1-6654-1219-3 http://ri.itba.edu.ar/handle/123456789/3900 en info:eu-repo/semantics/altIdentifier/doi/10.1109/ICSE43902.2021.00105 nfo:eu-repo/grantAgreement/ANCyP/PICT/2016-1384/AR. Ciudad Autónoma de Buenos Aires nfo:eu-repo/grantAgreement/ANCyP/PICT/2017-1979/AR. Ciudad Autónoma de Buenos Aires info:eu-repo/grantAgreement/ANCyP/PICT/2017-2622/AR. Ciudad Autónoma de Buenos Aires info:eu-repo/grantAgreement/ARO/W911NF19-1-0054/US. Durham info:eu-repo/grantAgreement/NSF/CCF-1948536/US. Virginia. Alexandria info:eu-repo/grantAgreement/NSF/CCF-1755890/US. Virginia. Alexandria info:eu-repo/grantAgreement/NSF/CCF-1618132/US. Virginia. Alexandria application/pdf |
institution |
Instituto Tecnológico de Buenos Aires (ITBA) |
institution_str |
I-32 |
repository_str |
R-138 |
collection |
Repositorio Institucional Instituto Tecnológico de Buenos Aires (ITBA) |
language |
Inglés |
topic |
LENGUAJES DE PROGRAMACION AUTOMATIZACION REPARACIONES |
spellingShingle |
LENGUAJES DE PROGRAMACION AUTOMATIZACION REPARACIONES Gutiérrez Brida, Simón Regis, Germán Zheng, Guolong Bagher, Hamid Nguyen, Thanh Vu Aguirre, Nazareno Frías, Marcelo Bounded exhaustive search of alloy specification repairs |
topic_facet |
LENGUAJES DE PROGRAMACION AUTOMATIZACION REPARACIONES |
description |
"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, ex ploration 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 real world faulty models, collected by other researchers, corroborates its ability to effectively generate correct repairs and outperform
the state-of-the-art." |
format |
Ponencias en Congresos acceptedVersion |
author |
Gutiérrez Brida, Simón Regis, Germán Zheng, Guolong Bagher, Hamid Nguyen, Thanh Vu Aguirre, Nazareno Frías, Marcelo |
author_facet |
Gutiérrez Brida, Simón Regis, Germán Zheng, Guolong Bagher, Hamid Nguyen, Thanh Vu Aguirre, Nazareno Frías, Marcelo |
author_sort |
Gutiérrez Brida, Simón |
title |
Bounded exhaustive search of alloy specification repairs |
title_short |
Bounded exhaustive search of alloy specification repairs |
title_full |
Bounded exhaustive search of alloy specification repairs |
title_fullStr |
Bounded exhaustive search of alloy specification repairs |
title_full_unstemmed |
Bounded exhaustive search of alloy specification repairs |
title_sort |
bounded exhaustive search of alloy specification repairs |
publishDate |
2022 |
url |
http://ri.itba.edu.ar/handle/123456789/3900 |
work_keys_str_mv |
AT gutierrezbridasimon boundedexhaustivesearchofalloyspecificationrepairs AT regisgerman boundedexhaustivesearchofalloyspecificationrepairs AT zhengguolong boundedexhaustivesearchofalloyspecificationrepairs AT bagherhamid boundedexhaustivesearchofalloyspecificationrepairs AT nguyenthanhvu boundedexhaustivesearchofalloyspecificationrepairs AT aguirrenazareno boundedexhaustivesearchofalloyspecificationrepairs AT friasmarcelo boundedexhaustivesearchofalloyspecificationrepairs |
_version_ |
1765660836555128832 |