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
 

Files


Full Text
learning-alloy-specs.pdf
Author preprint (459.69 kB)
Download

All documents in ORBilu are protected by a user license.

Send to



Details



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 :
yes
Language :
English
Title :
An evolutionary approach to translating operational specifications into declarative specifications
Publication date :
2019
Journal title :
Science of Computer Programming
ISSN :
0167-6423
Publisher :
Elsevier, Netherlands
Volume :
181
Pages :
47--63
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

Statistics


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

Scopus citations®
 
2
Scopus citations®
without self-citations
1
OpenCitations
 
3
WoS citations
 
1

Bibliography


Similar publications



Contact ORBilu