Article (Scientific journals)
An evolutionary approach to translating operational specifications into declarative specifications
Molina, Facundo; Cornejo, César; Degiovanni, Renzo Gaston et al.
2019In Science of Computer Programming, 181, p. 47--63
Peer Reviewed verified by ORBi


Full Text
Author preprint (459.69 kB)

All documents in ORBilu are protected by a user license.

Send to


Abstract :
[en] 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 evolu- tionary approach to translate an operational specification written in a sequen- tial 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.
Disciplines :
Computer science
Author, co-author :
Molina, Facundo
Cornejo, César
Degiovanni, Renzo Gaston ;  University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT)
Regis, Germán
Castro, Pablo F.
Aguirre, Nazareno
Frias, Marcelo F.
External co-authors :
Language :
Title :
An evolutionary approach to translating operational specifications into declarative specifications
Publication date :
Journal title :
Science of Computer Programming
Publisher :
Elsevier, Netherlands
Volume :
Pages :
Peer reviewed :
Peer Reviewed verified by ORBi
Focus Area :
Computational Sciences
FnR Project :
FNR12632675 - Support Of Advanced Test Coverage Criteria For Robust And Secure Software, 2018 (01/01/2019-30/06/2022) - Michail Papadakis
Available on ORBilu :
since 26 November 2019


Number of views
97 (3 by Unilu)
Number of downloads
132 (2 by Unilu)

Scopus citations®
Scopus citations®
without self-citations
WoS citations


Similar publications

Contact ORBilu