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...

Descripción completa

Detalles Bibliográficos
Autores principales: Gutiérrez Brida, Simón, Regis, Germán, Zheng, Guolong, Bagher, Hamid, Nguyen, Thanh Vu, Aguirre, Nazareno, Frías, Marcelo
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