An evolutionary approach to translating operational specifications into declarative specifications

"Various tools for program analysis, including run-time assertion checkers and static analyzers such as verification and test generation tools, require formal specifications of the programs being analyzed. Moreover, many of these tools and techniques require such specifications to be written in...

Descripción completa

Detalles Bibliográficos
Autores principales: Molina, Facundo, Cornejo, César, Degiovanni, Renzo, Regis, Germán, Castro, Pablo, Aguirre, Nazareno, Frías, Marcelo
Formato: Artículos de Publicaciones Periódicas acceptedVersion
Lenguaje:Inglés
Publicado: 2020
Materias:
ESTRUCTURA DE DATOS
VERIFICACION DE SOFTWARE
TEORIA DE LA COMPUTACION
ALGORITMOS EVOLUTIVOS
Acceso en línea:http://ri.itba.edu.ar/handle/123456789/1853
Aporte de:
Repositorio Institucional Instituto Tecnológico de Buenos Aires (ITBA) de Instituto Tecnológico de Buenos Aires (ITBA)
id I32-R138-123456789-1853
record_format dspace
spelling I32-R138-123456789-18532022-12-07T13:06:22Z An evolutionary approach to translating operational specifications into declarative specifications Molina, Facundo Cornejo, César Degiovanni, Renzo Regis, Germán Castro, Pablo Aguirre, Nazareno Frías, Marcelo ESTRUCTURA DE DATOS VERIFICACION DE SOFTWARE TEORIA DE LA COMPUTACION ALGORITMOS EVOLUTIVOS "Various tools for program analysis, including run-time assertion checkers and static analyzers such as verification and test generation tools, require formal specifications of the programs being analyzed. Moreover, many of these tools and techniques require such specifications to be written in a particular style, or follow certain patterns, in order to obtain an acceptable performance from the corresponding analyses. Thus, having a formal specification sometimes is not enough for using a particular technique, since such specification may not be provided in the right formalism. In this paper, we deal with this problem in the increasingly common case of having an operational specification, while for analysis reasons requiring a declarative specification. We propose an evolutionary approach to translate an operational specification written in a sequential programming language, into a declarative specification, in relational logic. We perform experiments on a benchmark of data structure implementations, for which operational invariants are available, and show that our evolutionary computation based approach to translating specifications achieves very good precision in this context, and produces declarative specifications that are more amenable to analyses that demand specifications in this style. This is assessed in two contexts: bounded verification of data structure invariant preservation, and instance enumeration using symbolic execution aided by tight bounds." 2020-01-06T17:23:38Z 2020-01-06T17:23:38Z 2019-07 Artículos de Publicaciones Periódicas info:eu-repo/semantics/acceptedVersion 0167-6423 http://ri.itba.edu.ar/handle/123456789/1853 en info:eu-repo/semantics/altIdentifier/doi/10.1016/j.scico.2019.05.006 info:eu-repo/grantAgreement/ANPCyT /2015-0586/AR. Ciudad Autónoma de Buenos Aires info:eu-repo/grantAgreement/ANPCyT /2016-1384/AR. Ciudad Autónoma de Buenos Aires info:eu-repo/grantAgreement/ANPCyT /2017-1979/AR. Ciudad Autónoma de Buenos Aires info:eu-repo/grantAgreement/ANPCyT /2017-2622/AR. Ciudad Autónoma de Buenos Aires info:eu-repo/grantAgreement/ANR/INTER/18/12632675/FR. París/SATOCROSS 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 ESTRUCTURA DE DATOS
VERIFICACION DE SOFTWARE
TEORIA DE LA COMPUTACION
ALGORITMOS EVOLUTIVOS
spellingShingle ESTRUCTURA DE DATOS
VERIFICACION DE SOFTWARE
TEORIA DE LA COMPUTACION
ALGORITMOS EVOLUTIVOS
Molina, Facundo
Cornejo, César
Degiovanni, Renzo
Regis, Germán
Castro, Pablo
Aguirre, Nazareno
Frías, Marcelo
An evolutionary approach to translating operational specifications into declarative specifications
topic_facet ESTRUCTURA DE DATOS
VERIFICACION DE SOFTWARE
TEORIA DE LA COMPUTACION
ALGORITMOS EVOLUTIVOS
description "Various tools for program analysis, including run-time assertion checkers and static analyzers such as verification and test generation tools, require formal specifications of the programs being analyzed. Moreover, many of these tools and techniques require such specifications to be written in a particular style, or follow certain patterns, in order to obtain an acceptable performance from the corresponding analyses. Thus, having a formal specification sometimes is not enough for using a particular technique, since such specification may not be provided in the right formalism. In this paper, we deal with this problem in the increasingly common case of having an operational specification, while for analysis reasons requiring a declarative specification. We propose an evolutionary approach to translate an operational specification written in a sequential programming language, into a declarative specification, in relational logic. We perform experiments on a benchmark of data structure implementations, for which operational invariants are available, and show that our evolutionary computation based approach to translating specifications achieves very good precision in this context, and produces declarative specifications that are more amenable to analyses that demand specifications in this style. This is assessed in two contexts: bounded verification of data structure invariant preservation, and instance enumeration using symbolic execution aided by tight bounds."
format Artículos de Publicaciones Periódicas
acceptedVersion
author Molina, Facundo
Cornejo, César
Degiovanni, Renzo
Regis, Germán
Castro, Pablo
Aguirre, Nazareno
Frías, Marcelo
author_facet Molina, Facundo
Cornejo, César
Degiovanni, Renzo
Regis, Germán
Castro, Pablo
Aguirre, Nazareno
Frías, Marcelo
author_sort Molina, Facundo
title An evolutionary approach to translating operational specifications into declarative specifications
title_short An evolutionary approach to translating operational specifications into declarative specifications
title_full An evolutionary approach to translating operational specifications into declarative specifications
title_fullStr An evolutionary approach to translating operational specifications into declarative specifications
title_full_unstemmed An evolutionary approach to translating operational specifications into declarative specifications
title_sort evolutionary approach to translating operational specifications into declarative specifications
publishDate 2020
url http://ri.itba.edu.ar/handle/123456789/1853
work_keys_str_mv AT molinafacundo anevolutionaryapproachtotranslatingoperationalspecificationsintodeclarativespecifications
AT cornejocesar anevolutionaryapproachtotranslatingoperationalspecificationsintodeclarativespecifications
AT degiovannirenzo anevolutionaryapproachtotranslatingoperationalspecificationsintodeclarativespecifications
AT regisgerman anevolutionaryapproachtotranslatingoperationalspecificationsintodeclarativespecifications
AT castropablo anevolutionaryapproachtotranslatingoperationalspecificationsintodeclarativespecifications
AT aguirrenazareno anevolutionaryapproachtotranslatingoperationalspecificationsintodeclarativespecifications
AT friasmarcelo anevolutionaryapproachtotranslatingoperationalspecificationsintodeclarativespecifications
AT molinafacundo evolutionaryapproachtotranslatingoperationalspecificationsintodeclarativespecifications
AT cornejocesar evolutionaryapproachtotranslatingoperationalspecificationsintodeclarativespecifications
AT degiovannirenzo evolutionaryapproachtotranslatingoperationalspecificationsintodeclarativespecifications
AT regisgerman evolutionaryapproachtotranslatingoperationalspecificationsintodeclarativespecifications
AT castropablo evolutionaryapproachtotranslatingoperationalspecificationsintodeclarativespecifications
AT aguirrenazareno evolutionaryapproachtotranslatingoperationalspecificationsintodeclarativespecifications
AT friasmarcelo evolutionaryapproachtotranslatingoperationalspecificationsintodeclarativespecifications
_version_ 1765660818332975104

Ejemplares similares