Sound and Precise Symbolic Automata Model for Stateful Software Systems

Abstract

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.