Many software validation and verification activities require a description of the software under analysis, since many analyses typically consist in checking compliance of the software against some prescribed intended behavior. Formal specifications have gained an important relevance in such contexts, mainly due to their unambiguous interpretation and the increasing availability of technologies for their automated analysis, which are making them part of effective software analysis approaches.

In this context, this project focuses on the use of evolutionary computation in two particular tasks. On the one side, a technique based on genetic algorithms was implemented to search for declarative specifications (in relational logic) equivalent to provided operational ones. On the other side, this kind of algorihtms were also used to search for formulas (in temporal logic) that capture obstacles in formal requirements specifications.

So far, the following papers have been published:

• An evolutionary approach to translating operational specifications into declarative specifications, Science of Computer Programming, 2019. Replication package.

• A genetic algorithm for goal-conflict identification, Automated Software Engineering, 2018. Replication package.

• An Evolutionary Approach to Translate Operational Specifications into Declarative Specifications