Partial Automation of Verification Condition Proving for Reflex Programs (Draft)
2026-06-22 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors discuss a way to make sure complex industrial control systems work safely by checking their programs with logical rules. They focus on Process-Oriented Programming, which models control systems as real processes. Previously, they had a tool that created too many checking tasks, making it hard to prove everything by hand. In this paper, they improved the tool by adding a way to write clearer requirements, generating helpful conditions automatically, and using smart software to solve some checks without human help.
Process-Oriented Programmingcontrol systemsformal verificationdeductive verificationverification conditionsverification condition generatorinvariantsannotation languageSMT solvers
Authors
Artyom Ishchenko, Igor Anureev
Abstract
Process-Oriented Programming is a software development approach that emphasizes the management of control systems through abstractions of processes and their states, enabling these systems to be described in terms of real physical processes. This native description of control is particularly important for industrial systems consisting of hundreds or thousands of processes. For such systems, safety is critical. To ensure the reliability and safety of these systems, formal verification methods must be applied. One such method is deductive verification, which involves formalizing programs and their requirements as logical formulas, known as verification conditions. Proving these conditions confirms that the program meets its requirements. The automatic generation of verification conditions is performed by a specialized software tool called a verification condition generator. We previously proposed a verification condition generator for the Reflex language. However, it generates too many verification conditions, making their manual proof impossible. This paper proposes modifications to the verification condition generator aimed at automating the proof of some of these conditions. These modifications include introducing an annotation language to describe requirements in a structured form, generating invariants based on the program structure, and using SMT solvers for the preliminary attempt to solve the verification conditions.