Towards Verification Modulo Theories of asynchronous systems via abstraction refinement

This paper introduces a new algorithm designedto verify safety properties for asynchronous compositions ofsymbolic transition systems. The approach combines under-approximation and over-approximation: on one side, it zooms inon a selected set of components, while forcing the remaining onesto stutter; on the other, the selected components are individuallyabstracted and re-composed. This strategy can be advantageousfor scenarios involving large numbers of components, whereonly a small subset of key components allows to produce theright invariants for the system. We detail the application of ouralgorithm to a class of parameterized symbolic transition systems,by using a form of slicing as an abstraction. Our experimentalresults, although preliminary, show the potential of the approach.