Generating Specifications with Evolutionary Computation

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.

Relational properties
Temporal properties

So far, the following papers have been published: