ATR: Template-based repair for alloy specifications

Mostrar todas las versiones(2)

"Automatic Program Repair (APR) is a practical research topic that studies techniques to automatically repair programs to fix bugs. Most existing APR techniques are designed for imperative programming languages, such as C and Java, and rely on analyzing correct and incorrect executions of progr...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Zheng, Guolong, Vu Nguyen, Thanh, Gutiérrez Brida, Simón, Regis, Germán, Aguirre, Nazareno, Frías, Marcelo F., Bagheri, Hamid
Formato: Artículo de Publicación Periódica acceptedVersion
Lenguaje:Inglés
Publicado: 2023
Materias:
REPARACIONES
ALEACIONES
Acceso en línea:https://ri.itba.edu.ar/handle/123456789/4144
Aporte de:
Repositorio Institucional Instituto Tecnológico de Buenos Aires (ITBA) de Instituto Tecnológico de Buenos Aires (ITBA)
id I32-R138-123456789-4144
record_format dspace
spelling I32-R138-123456789-41442023-01-12T03:00:59Z ATR: Template-based repair for alloy specifications Zheng, Guolong Vu Nguyen, Thanh Gutiérrez Brida, Simón Regis, Germán Aguirre, Nazareno Frías, Marcelo F. Bagheri, Hamid REPARACIONES ALEACIONES "Automatic Program Repair (APR) is a practical research topic that studies techniques to automatically repair programs to fix bugs. Most existing APR techniques are designed for imperative programming languages, such as C and Java, and rely on analyzing correct and incorrect executions of programs to identify and repair suspicious statements. We introduce a new APR approach for software specifications written in the Alloy declarative language, where specifications are not “executed”, but rather converted into logical formulas and analyzed using backend constraint solvers, to find specification instances and counterexamples to assertions. We present ATR, a technique that takes as input an Alloy specification with some violated assertion and returns a repaired specification that satisfies the assertion. The key ideas are (i) analyzing the differences between counterexamples that do not satisfy the assertion and instances that do satisfy the assertion to guide the repair and (ii) generating repair candidates from specific templates and pruning the space of repair candidates using the counterexamples and satisfying instances. Experimental results using existing large Alloy benchmarks show that ATR is effective in generating difficult repairs. ATR repairs 66.3% of 1974 fault specifications, including specification repairs that cannot be handled by existing Alloy repair techniques." 2023-01-11T18:26:55Z 2023-01-11T18:26:55Z 2022 Artículo de Publicación Periódica info:eu-repo/semantics/acceptedVersion 978-1-4503-9379-9 https://ri.itba.edu.ar/handle/123456789/4144 en info:eu-repo/grantAgreement/NSF/1755890/US. Virginia. Alexandria info:eu-repo/grantAgreement/NSF/1618132/US. Virginia. Alexandria info:eu-repo/grantAgreement/NSF/2139845/US. Virginia. Alexandria info:eu-repo/grantAgreement/NSF/1948536/US. Virginia. Alexandria info:eu-repo/grantAgreement/NSF/2107035/US. Virginia. Alexandria info:eu-repo/grantAgreement/CONICET/PICT 2017-2622/AR. Ciudad Autónoma de Buenos Aires info:eu-repo/grantAgreement/CONICET/2019-2050/AR. Ciudad Autónoma de Buenos Aires info:eu-repo/semantics/altIdentifier/doi/10.1145/3533767.3534369 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 REPARACIONES
ALEACIONES
spellingShingle REPARACIONES
ALEACIONES
Zheng, Guolong
Vu Nguyen, Thanh
Gutiérrez Brida, Simón
Regis, Germán
Aguirre, Nazareno
Frías, Marcelo F.
Bagheri, Hamid
ATR: Template-based repair for alloy specifications
topic_facet REPARACIONES
ALEACIONES
description "Automatic Program Repair (APR) is a practical research topic that studies techniques to automatically repair programs to fix bugs. Most existing APR techniques are designed for imperative programming languages, such as C and Java, and rely on analyzing correct and incorrect executions of programs to identify and repair suspicious statements. We introduce a new APR approach for software specifications written in the Alloy declarative language, where specifications are not “executed”, but rather converted into logical formulas and analyzed using backend constraint solvers, to find specification instances and counterexamples to assertions. We present ATR, a technique that takes as input an Alloy specification with some violated assertion and returns a repaired specification that satisfies the assertion. The key ideas are (i) analyzing the differences between counterexamples that do not satisfy the assertion and instances that do satisfy the assertion to guide the repair and (ii) generating repair candidates from specific templates and pruning the space of repair candidates using the counterexamples and satisfying instances. Experimental results using existing large Alloy benchmarks show that ATR is effective in generating difficult repairs. ATR repairs 66.3% of 1974 fault specifications, including specification repairs that cannot be handled by existing Alloy repair techniques."
format Artículo de Publicación Periódica
acceptedVersion
author Zheng, Guolong
Vu Nguyen, Thanh
Gutiérrez Brida, Simón
Regis, Germán
Aguirre, Nazareno
Frías, Marcelo F.
Bagheri, Hamid
author_facet Zheng, Guolong
Vu Nguyen, Thanh
Gutiérrez Brida, Simón
Regis, Germán
Aguirre, Nazareno
Frías, Marcelo F.
Bagheri, Hamid
author_sort Zheng, Guolong
title ATR: Template-based repair for alloy specifications
title_short ATR: Template-based repair for alloy specifications
title_full ATR: Template-based repair for alloy specifications
title_fullStr ATR: Template-based repair for alloy specifications
title_full_unstemmed ATR: Template-based repair for alloy specifications
title_sort atr: template-based repair for alloy specifications
publishDate 2023
url https://ri.itba.edu.ar/handle/123456789/4144
work_keys_str_mv AT zhengguolong atrtemplatebasedrepairforalloyspecifications
AT vunguyenthanh atrtemplatebasedrepairforalloyspecifications
AT gutierrezbridasimon atrtemplatebasedrepairforalloyspecifications
AT regisgerman atrtemplatebasedrepairforalloyspecifications
AT aguirrenazareno atrtemplatebasedrepairforalloyspecifications
AT friasmarcelof atrtemplatebasedrepairforalloyspecifications
AT bagherihamid atrtemplatebasedrepairforalloyspecifications
_version_ 1766727851883626496

Ejemplares similares