Using static analysis to reduce the number of verification conditions generated for Reflex programs

Using static analysis to reduce the number of verification conditions generated for Reflex programs

Ishchenko A.D. (IA&E SB RAS, Novosibirsk, Russia)
Anureev I.S. (IA&E SB RAS, Novosibirsk, Russia)

Abstract

Control systems are widely used in safety-critical areas, which places high demands on software reliability and on proving that the software works correctly. To meet these demands, formal methods come into play – deductive verification in particular. That approach generates verification conditions based on the program’s axiomatic semantics and its specifications. The trouble is, automatic generation often produces formulas that are redundant or overly complex, making them harder to verify and reducing the effectiveness of automated theorem provers. Domain-specific languages like Reflex partially address this issue. Reflex uses a process-oriented paradigm that simplifies program structure. But the semantics of Reflex constructs can sometimes generate even more verification conditions, especially irrelevant ones that correspond to unreachable paths in the program. In this work we propose a static analysis method aimed at reducing the number of verification conditions generated for Reflex programs. The method annotates program statements with a set of attributes that capture their semantic properties. First, attributes are computed for elementary statements, then aggregated for composite constructs. During verification condition generation, attributes accumulate along the execution path taken, and their consistency is checked. Incompatible attribute combinations reveal irrelevant verification conditions, which can then be discarded. Experimental evaluation on a set of test programs shows that our approach cuts down the number of verification conditions significantly – up to 97% in some cases – and the improvement grows as the number of processes and states in the program increases.

Keywords

Reflex; process-oriented programming; verification conditions; static analysis; attributes.

Edition

Proceedings of the Institute for System Programming, vol. 38, issue 6, part 2, 2026, pp. 21-40

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2026-38(6)-23

For citation

Ishchenko A.D., Anureev I.S. Using static analysis to reduce the number of verification conditions generated for Reflex programs. Proceedings of the Institute for System Programming, vol. 38, issue 6, part 2, 2026, pp. 21-40 DOI: 10.15514/ISPRAS-2026-38(6)-23.

Full text of the paper in pdf (in Russian) Back to the contents of the volume