Sound and Precise Symbolic Automata Model for Stateful Software Systems

Abstract Verifying stateful software systems remains challenging due to complex control structures and intricate state interactions, often necessitating pre-existing behavioral models. We introduce , an abstract interpreter that automatically derives sound and precise symbolic finite automata models. In tests on real-world applications, generates sound and precise automata within minutes and, when employed in dynamic model checking, achieves 1.6 $\times$ × –3.4 $\times$ × code coverage compared to the state of the art. These findings demonstrate that can effectively connect code to model-based verification for stateful software systems.