Automatic State Reaching for Debugging Reactive Programs

Reactive systems are made of programs that permanently interact with their environment. Debuggers generally provide support for data and state inspection, given a sequence of inputs. But, because the reactive programs and their environments are interdependent, a very useful feature is to be able to go the other way around; namely, given a state, obtain a sequence of inputs that leads to that state. This problem is equivalent to the general verification of safety properties, which is notoriously undecidable in presence of numeric variables. However, a lot of progress has been done in recent years through the development of model checking and abstract-interpretation-based techniques. In this article, we take advantage of those recent advances to implement a fully automatic state reaching capability inside a debugger of reactive programs. To achieve that, we connect a debugger, a verification tool, and a testing tool. One of the key contributions of our proposal is the proper handling of numeric variables