# EvoSpex: An Evolutionary Algorithm for Learning Postconditions

arXiv: https://arxiv.org/abs/2102.13569 · HTML: https://mlsanity.com/paper/2102.13569/

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 26 Feb 2021.

## Built on by (most cited first, 6 of 6)

- [Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?](https://mlsanity.com/paper/2310.01831/) (2023)
- [The Future of AI-Driven Software Engineering](https://mlsanity.com/paper/2406.07737/) (2024)
- [AutoReSpec: A Framework for Generating Specification using Large Language Models](https://mlsanity.com/paper/2604.03758/) (2026)
- [Teaching Code LLMs to Reason with Intermediate Formal Specifications](https://mlsanity.com/paper/2607.04232/) (2026)
- [SpecPylot: Python Specification Generation using Large Language Models](https://mlsanity.com/paper/2604.16560/) (2026)
- [Agentic Generation and Evolution of Knowledge Models](https://mlsanity.com/paper/2606.03662/) (2026)

## Abstract (arXiv)

Software reliability is a primary concern in the construction of software, and thus a fundamental component in the definition of software quality. Analyzing software reliability requires a specification of the intended behavior of the software under analysis, and at the source code level, such specifications typically take the form of assertions. Unfortunately, software many times lacks such specifications, or only provides them for scenario-specific behaviors, as assertions accompanying tests. This issue seriously diminishes the analyzability of software with respect to its reliability. In this paper, we tackle this problem by proposing a technique that, given a Java method, automatically produces a specification of the method's current behavior, in the form of postcondition assertions. This mechanism is based on generating executions of the method under analysis to obtain valid pre/post state pairs, mutating these pairs to obtain (allegedly) invalid ones, and then using a genetic algorithm to produce an assertion that is satisfied by the valid pre/post pairs, while leaving out the invalid ones. The technique, which targets in particular methods of reference-based class implementations, is assessed on a benchmark of open source Java projects, showing that our genetic algorithm is able to generate post-conditions that are stronger and more accurate, than those generated by related automated approaches, as evaluated by an automated oracle assessment tool. Moreover, our technique is also able to infer an important part of manually written rich postconditions in verified classes, and reproduce contracts for methods whose class implementations were automatically synthesized from specifications.