FLACK: Counterexample-guided fault localization for alloy models

Mostrar todas las versiones(2)

"Fault localization is a practical research topic that helps developers identify code locations that might cause bugs in a program. Most existing fault localization techniques are designed for imperative programs (e.g., C and Java) and rely on analyzing correct and incorrect executions of the...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Zheng, Guolong, Nguyen, Thanh Vu, Gutiérrez Brida, Simón, Regis, Germán, Frías, Marcelo, Aguirre, Nazareno, Bagher, Hamid
Formato: Ponencias en Congresos acceptedVersion
Lenguaje:Inglés
Publicado: 2022
Materias:
ANALISIS DE FALLAS
LENGUAJES DE PROGRAMACION
Acceso en línea:http://ri.itba.edu.ar/handle/123456789/3909
Aporte de:
Repositorio Institucional Instituto Tecnológico de Buenos Aires (ITBA) de Instituto Tecnológico de Buenos Aires (ITBA)
id I32-R138-123456789-3909
record_format dspace
spelling I32-R138-123456789-39092022-12-07T14:13:46Z FLACK: Counterexample-guided fault localization for alloy models Zheng, Guolong Nguyen, Thanh Vu Gutiérrez Brida, Simón Regis, Germán Frías, Marcelo Aguirre, Nazareno Bagher, Hamid ANALISIS DE FALLAS LENGUAJES DE PROGRAMACION "Fault localization is a practical research topic that helps developers identify code locations that might cause bugs in a program. Most existing fault localization techniques are designed for imperative programs (e.g., C and Java) and rely on analyzing correct and incorrect executions of the program to identify suspicious statements. In this work, we introduce a fault localization approach for models written in a declarative language, where the models are not “executed,” but rather converted into a logical formula and solved using backend constraint solvers. We present FLACK, a tool that takes as input an Alloy model consisting of some violated assertion and returns a ranked list of suspicious expressions contributing to the assertion violation. The key idea is to analyze the differences between counterexamples, i.e., instances of the model that do not satisfy the assertion, and instances that do satisfy the assertion to find suspicious expressions in the input model. The experimental results show that FLACK is efficient (can handle complex, real world Alloy models with thousand lines of code within 5 seconds), accurate (can consistently rank buggy expressions in the top 1.9% of the suspicious list), and useful (can often narrow down the error to the exact location within the suspicious expressions)." 2022-06-03T13:54:30Z 2022-06-03T13:54:30Z 2021 Ponencias en Congresos info:eu-repo/semantics/acceptedVersion 13-978-1-6654-1219-3 http://ri.itba.edu.ar/handle/123456789/3909 en info:eu-repo/semantics/altIdentifier/doi/10.1109/ICSE43902.2021.00065 info:eu-repo/grantAgreement/ARO/W911NF-19-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 nfo:eu-repo/grantAgreement/ANCyP/PICT/2016-1384/AR. Ciudad Autónoma de Buenos Aires info:eu-repo/grantAgreement/ANCyP/PICT/2016-1384/AR. Ciudad Autónoma de Buenos Aires info:eu-repo/grantAgreement/ANCyP/PICT/2017-2622/AR. Ciudad Autónoma de Buenos Aires 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 ANALISIS DE FALLAS
LENGUAJES DE PROGRAMACION
spellingShingle ANALISIS DE FALLAS
LENGUAJES DE PROGRAMACION
Zheng, Guolong
Nguyen, Thanh Vu
Gutiérrez Brida, Simón
Regis, Germán
Frías, Marcelo
Aguirre, Nazareno
Bagher, Hamid
FLACK: Counterexample-guided fault localization for alloy models
topic_facet ANALISIS DE FALLAS
LENGUAJES DE PROGRAMACION
description "Fault localization is a practical research topic that helps developers identify code locations that might cause bugs in a program. Most existing fault localization techniques are designed for imperative programs (e.g., C and Java) and rely on analyzing correct and incorrect executions of the program to identify suspicious statements. In this work, we introduce a fault localization approach for models written in a declarative language, where the models are not “executed,” but rather converted into a logical formula and solved using backend constraint solvers. We present FLACK, a tool that takes as input an Alloy model consisting of some violated assertion and returns a ranked list of suspicious expressions contributing to the assertion violation. The key idea is to analyze the differences between counterexamples, i.e., instances of the model that do not satisfy the assertion, and instances that do satisfy the assertion to find suspicious expressions in the input model. The experimental results show that FLACK is efficient (can handle complex, real world Alloy models with thousand lines of code within 5 seconds), accurate (can consistently rank buggy expressions in the top 1.9% of the suspicious list), and useful (can often narrow down the error to the exact location within the suspicious expressions)."
format Ponencias en Congresos
acceptedVersion
author Zheng, Guolong
Nguyen, Thanh Vu
Gutiérrez Brida, Simón
Regis, Germán
Frías, Marcelo
Aguirre, Nazareno
Bagher, Hamid
author_facet Zheng, Guolong
Nguyen, Thanh Vu
Gutiérrez Brida, Simón
Regis, Germán
Frías, Marcelo
Aguirre, Nazareno
Bagher, Hamid
author_sort Zheng, Guolong
title FLACK: Counterexample-guided fault localization for alloy models
title_short FLACK: Counterexample-guided fault localization for alloy models
title_full FLACK: Counterexample-guided fault localization for alloy models
title_fullStr FLACK: Counterexample-guided fault localization for alloy models
title_full_unstemmed FLACK: Counterexample-guided fault localization for alloy models
title_sort flack: counterexample-guided fault localization for alloy models
publishDate 2022
url http://ri.itba.edu.ar/handle/123456789/3909
work_keys_str_mv AT zhengguolong flackcounterexampleguidedfaultlocalizationforalloymodels
AT nguyenthanhvu flackcounterexampleguidedfaultlocalizationforalloymodels
AT gutierrezbridasimon flackcounterexampleguidedfaultlocalizationforalloymodels
AT regisgerman flackcounterexampleguidedfaultlocalizationforalloymodels
AT friasmarcelo flackcounterexampleguidedfaultlocalizationforalloymodels
AT aguirrenazareno flackcounterexampleguidedfaultlocalizationforalloymodels
AT bagherhamid flackcounterexampleguidedfaultlocalizationforalloymodels
_version_ 1765660930520121344

Ejemplares similares