Abstract This paper presents a novel symbolic algorithm for the Maximal End Component (MEC) decomposition of a Markov Decision Process (MDP) . The key idea behind our algorithm is to interleave the computation of Strongly Connected Components (SCCs) with eager elimination of redundant state-action pairs, rather than performing these computations sequentially as done by existing state-of-the-art algorithms. Even though our approach has the same complexity as prior works, an empirical evaluation of on the standardized Quantitative Verification Benchmark Set demonstrates that it solves $$\textbf{19}$$ 19 more benchmarks (out of 368) than the closest previous algorithm. On the 149 benchmarks that prior approaches can solve, we demonstrate a $$\mathbf {3.81 \times}$$ 3.81 × average speedup in runtime.

Many software systems are polyglot; that is, they comprise programs implemented in a combination of programming languages. Program verifiers, however, tend to be customized for individual languages. Verification by compiling to a common encoding requires supporting full language syntax and semantics which is prohibitive for modern languages. We present POLYVER, an alternative compositional approach to polyglot verification that bootstraps off-the-shelf language-specific verifiers with abstraction and synthesis. POLYVER uses contracts written in an intermediate language to abstract individual procedures in the system. Our verification approach uses language-specific verifiers (e.g., for C or Rust) to validate these contracts and the UCLID5 model checker for com- positionally verifying a temporal property on the overall system using the contracts. The intermediate language sidesteps the need for compiling implementation languages to a common encoding, a key obstacle with polyglot verification. Finally, POLYVER automates the generation of contracts using synthesis oracles such as large-language-models (LLMs). Overall POLYVER performs contract synthesis and verification in a counterexample-guided abstraction refinement and inductive synthesis (CEGIS-CEGAR) loop to verify the system-level property. We use POLYVER to verify programs in the Lingua Franca polyglot language. We are able to verify systems with C and Rust procedures, as well as C language fragments that were unsupported in previous work.