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.

The advent of microservice architecture has led to a significant shift in the development of service-oriented software. In particular, the use of Remote Procedure Call (RPC), a mode of Inter-Process Communication (IPC) prevalent in microservices, has noticeably increased. To figure out the relationships between services and obtain a high-level understanding of service-oriented software, a line of recent work focuses on the dynamic construction of service call graphs, which relies on the preliminary deployment of services and only captures the calling relationships within a specific time frame. Meanwhile, static methods avoid the need for pre-deployment and often provide a more stable and complete graph compared to dynamic techniques. However, research and practical applications of static call graph construction remain relatively unexplored. This paper introduces RPCover, a novel gRPC dependency recovery framework that facilitates the interconnection of services across various programming languages using their static gRPC calls. In addition, due to the lack of a multilingual microservice benchmark that uses gRPC, we build the first multilingual benchmark RPCoverBench that contains complex gRPC call relations. RPCover has been evaluated on a single language benchmark (DeathStarBench) and our multilingual benchmark (RPCoverBench). The results show that RPCover effectively recovers 99.33% of the use cases of gRPC calls with less than 200% of the overhead compared with a single-language semantic dependency analyzer.