OLA: Property Directed Outer Loop Abstraction for Efficient Verification of Reactive Systems

Reactive systems, designed for embedded applications, commonly feature an outer infinite loop that captures environmental input and according to the inputs decides the system’s response. The outer infinite loop implies that almost every reactive system contains nested loops. Existing verification techniques, such as model checking and loop abstraction methods, often struggle in terms of accuracy and efficiency in the presence of nested loops. This paper presents an abstraction approach called outer loop abstraction or OLA targeting nested loops. It selectively abstracts outer loops which infinitely read and process environmental input, transforms the input code, and passes it on to any existing industrial verifier to proceed with verification. Our proposed approach facilitates efficient and scalable verification of input properties through model checking. This technique complements existing slicing and abstraction techniques and has demonstrated promising results when applied to an industrial verifier.