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

artículo de publicación periódica.page.titleprefix
An evolutionary approach to translating operational specifications into declarative specifications

dc.contributor.author	Molina, Facundo
dc.contributor.author	Cornejo, César
dc.contributor.author	Degiovanni, Renzo
dc.contributor.author	Regis, Germán
dc.contributor.author	Castro, Pablo
dc.contributor.author	Aguirre, Nazareno
dc.contributor.author	Frías, Marcelo
dc.date.accessioned	2020-01-06T17:23:38Z
dc.date.available	2020-01-06T17:23:38Z
dc.date.issued	2019-07
dc.description.abstract	"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."	en
dc.identifier.issn	0167-6423
dc.identifier.uri	http://ri.itba.edu.ar/handle/123456789/1853
dc.language.iso	en	en
dc.relation	info:eu-repo/semantics/altIdentifier/doi/10.1016/j.scico.2019.05.006
dc.relation	info:eu-repo/grantAgreement/ANPCyT /2015-0586/AR. Ciudad Autónoma de Buenos Aires
dc.relation	info:eu-repo/grantAgreement/ANPCyT /2016-1384/AR. Ciudad Autónoma de Buenos Aires
dc.relation	info:eu-repo/grantAgreement/ANPCyT /2017-1979/AR. Ciudad Autónoma de Buenos Aires
dc.relation	info:eu-repo/grantAgreement/ANPCyT /2017-2622/AR. Ciudad Autónoma de Buenos Aires
dc.relation	info:eu-repo/grantAgreement/ANR/INTER/18/12632675/FR. París/SATOCROSS
dc.subject	ESTRUCTURA DE DATOS	es
dc.subject	VERIFICACION DE SOFTWARE	es
dc.subject	TEORIA DE LA COMPUTACION	es
dc.subject	ALGORITMOS EVOLUTIVOS	es
dc.title	An evolutionary approach to translating operational specifications into declarative specifications	en
dc.type	Artículos de Publicaciones Periódicas	es
dc.type	info:eu-repo/semantics/acceptedVersion
dspace.entity.type	Artículo de Publicación Periódica
itba.description.filiation	Fil: Molina, Facundo. Universidad Nacional de Río Cuarto. Facultad de Ciencias Exactas, Físico-Químicas y Naturales; Argentina.
itba.description.filiation	Fil: Molina, Facundo. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina.
itba.description.filiation	Fil: Cornejo, César. Universidad Nacional de Río Cuarto. Facultad de Ciencias Exactas, Físico-Químicas y Naturales; Argentina.
itba.description.filiation	Fil: Cornejo, César. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina.
itba.description.filiation	Fil: Degiovanni, Renzo. Université du Luxembourg; Luxemburgo.
itba.description.filiation	Fil: Castro, Pablo. Universidad Nacional de Río Cuarto. Facultad de Ciencias Exactas, Físico-Químicas y Naturales; Argentina.
itba.description.filiation	Fil: Castro, Pablo. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina.
itba.description.filiation	Fil: Aguirre, Nazareno. Universidad Nacional de Río Cuarto. Facultad de Ciencias Exactas, Físico-Químicas y Naturales; Argentina.
itba.description.filiation	Fil: Aguirre, Nazareno. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina.
itba.description.filiation	Fil: Frías, Marcelo. Instituto Tecnológico de Buenos Aires; Argentina.
itba.description.filiation	Fil: Frías, Marcelo. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina.
itba.description.filiation	Fil: Regis, Germán. Universidad Nacional de Río Cuarto. Facultad de Ciencias Exactas, Físico-Químicas y Naturales; Argentina.