Reference : An evolutionary approach to translating operational specifications into declarative s...
Scientific journals : Article
Engineering, computing & technology : Computer science
Computational Sciences
http://hdl.handle.net/10993/41038
An evolutionary approach to translating operational specifications into declarative specifications
English
Molina, Facundo [> >]
Cornejo, César [> >]
Degiovanni, Renzo Gaston mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) >]
Regis, Germán [> >]
Castro, Pablo F. [> >]
Aguirre, Nazareno [> >]
Frias, Marcelo F. [> >]
2019
Science of Computer Programming
181
47--63
Yes (verified by ORBilu)
International
0167-6423
[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.
Researchers ; Professionals ; Students ; General public
http://hdl.handle.net/10993/41038
10.1016/j.scico.2019.05.006
https://doi.org/10.1016/j.scico.2019.05.006
FnR ; FNR12632675 > Michail Papadakis > SATOCROSS > Support of Advanced Test cOverage Criteria for RObust and Secure Software > 01/01/2019 > 31/12/2021 > 2018

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
learning-alloy-specs.pdfAuthor preprint448.92 kBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.