EvoSpex: An evolutionary algorithm for learning postconditions (artifact)

"Having the expected behavior of software specified in a formal language can greatly improve the automation of software verification activities, since these need to contrast the intended behavior with the actual software implementation. Unfortunately, software many times lacks such specificatio...

Descripción completa

Detalles Bibliográficos
Autores principales: Molina, Facundo, Ponzio, Pablo, Aguirre, Nazareno, Frías, Marcelo
Formato: Ponencias en Congresos acceptedVersion
Lenguaje:Inglés
Publicado: 2022
Materias:
VERIFICACION DE SOFTWARE
JAVA
ESPECIFICACIONES
ALGORITMOS
Acceso en línea:http://ri.itba.edu.ar/handle/123456789/3903
Aporte de:
Repositorio Institucional Instituto Tecnológico de Buenos Aires (ITBA) de Instituto Tecnológico de Buenos Aires (ITBA)
id I32-R138-123456789-3903
record_format dspace
spelling I32-R138-123456789-39032022-12-07T14:13:55Z EvoSpex: An evolutionary algorithm for learning postconditions (artifact) Molina, Facundo Ponzio, Pablo Aguirre, Nazareno Frías, Marcelo VERIFICACION DE SOFTWARE JAVA ESPECIFICACIONES ALGORITMOS "Having the expected behavior of software specified in a formal language can greatly improve the automation of software verification activities, since these need to contrast the intended behavior with the actual software implementation. Unfortunately, software many times lacks such specifications, and thus providing tools and techniques that can assist developers in the construction of software specifications are relevant in software engineering. As an aid in this context, we present EvoSpex, a tool that given a Java method, automatically produces a specification of the method’s current behavior, in the form of postcondition assertions. EvoSpex is based on generating software runs from the implementation (valid runs), making modifications to the runs to build divergent behaviors (invalid runs), and executing a genetic algorithm that tries to evolve a specification to satisfy the valid runs, and leave out the invalid ones. Our tool supports a rich JML-like assertion language, that can capture complex specifications, including sophisticated object structural properties." 2022-05-31T19:50:44Z 2022-05-31T19:50:44Z 2021 Ponencias en Congresos info:eu-repo/semantics/acceptedVersion http://ri.itba.edu.ar/handle/123456789/3903 en info:eu-repo/semantics/altIdentifier/doi/10.1109/ICSE-Companion52605.2021.00080 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 VERIFICACION DE SOFTWARE
JAVA
ESPECIFICACIONES
ALGORITMOS
spellingShingle VERIFICACION DE SOFTWARE
JAVA
ESPECIFICACIONES
ALGORITMOS
Molina, Facundo
Ponzio, Pablo
Aguirre, Nazareno
Frías, Marcelo
EvoSpex: An evolutionary algorithm for learning postconditions (artifact)
topic_facet VERIFICACION DE SOFTWARE
JAVA
ESPECIFICACIONES
ALGORITMOS
description "Having the expected behavior of software specified in a formal language can greatly improve the automation of software verification activities, since these need to contrast the intended behavior with the actual software implementation. Unfortunately, software many times lacks such specifications, and thus providing tools and techniques that can assist developers in the construction of software specifications are relevant in software engineering. As an aid in this context, we present EvoSpex, a tool that given a Java method, automatically produces a specification of the method’s current behavior, in the form of postcondition assertions. EvoSpex is based on generating software runs from the implementation (valid runs), making modifications to the runs to build divergent behaviors (invalid runs), and executing a genetic algorithm that tries to evolve a specification to satisfy the valid runs, and leave out the invalid ones. Our tool supports a rich JML-like assertion language, that can capture complex specifications, including sophisticated object structural properties."
format Ponencias en Congresos
acceptedVersion
author Molina, Facundo
Ponzio, Pablo
Aguirre, Nazareno
Frías, Marcelo
author_facet Molina, Facundo
Ponzio, Pablo
Aguirre, Nazareno
Frías, Marcelo
author_sort Molina, Facundo
title EvoSpex: An evolutionary algorithm for learning postconditions (artifact)
title_short EvoSpex: An evolutionary algorithm for learning postconditions (artifact)
title_full EvoSpex: An evolutionary algorithm for learning postconditions (artifact)
title_fullStr EvoSpex: An evolutionary algorithm for learning postconditions (artifact)
title_full_unstemmed EvoSpex: An evolutionary algorithm for learning postconditions (artifact)
title_sort evospex: an evolutionary algorithm for learning postconditions (artifact)
publishDate 2022
url http://ri.itba.edu.ar/handle/123456789/3903
work_keys_str_mv AT molinafacundo evospexanevolutionaryalgorithmforlearningpostconditionsartifact
AT ponziopablo evospexanevolutionaryalgorithmforlearningpostconditionsartifact
AT aguirrenazareno evospexanevolutionaryalgorithmforlearningpostconditionsartifact
AT friasmarcelo evospexanevolutionaryalgorithmforlearningpostconditionsartifact
_version_ 1765660728692310016

Ejemplares similares