SMT-based Symbolic Model-Checking for Operator Precedence Languages

TL;DR

This work addresses the scalability limitations of explicit-state model checking for Operator Precedence Languages (OPL) and their POTL specifications by proposing a symbolic, SMT-based bounded model checking approach for the future fragment of POTL, $\mathsf{POTL_f}$. It encodes the POTL tableau into SMT with a bounded unraveling up to $k$ steps, and models both the program and the specification in SMT, enabling efficient trace search via SMT solvers. The authors demonstrate, through benchmarks involving Quicksort, a banks application, and stacks, that their SMT-based method outperforms a state-of-the-art explicit-state tool (POMC), particularly on larger bit-widths and more complex formulas. This approach advances scalable verification for stack-oriented programming constructs (including calls, returns, and exceptions) and lays groundwork for extending POTL to past modalities and infinite words, with potential impact on verification tooling for real-world software.

Abstract

Operator Precedence Languages (OPL) have been recently identified as a suitable formalism for model checking recursive procedural programs, thanks to their ability of modeling the program stack. OPL requirements can be expressed in the Precedence Oriented Temporal Logic (POTL), which features modalities to reason on the natural matching between function calls and returns, exceptions, and other advanced programming constructs that previous approaches, such as Visibly Pushdown Languages, cannot model effectively. Existing approaches for model checking of POTL have been designed following the explicit-state, automata-based approach, a feature that severely limits their scalability. In this paper, we give the first symbolic, SMT-based approach for model checking POTL properties. While previous approaches construct the automaton for both the POTL formula and the model of the program, we encode them into a (sequence of) SMT formulas. The search of a trace of the model witnessing a violation of the formula is then carried out by an SMT-solver, in a Bounded Model Checking fashion. We carried out an experimental evaluation, which shows the effectiveness of the proposed solution.

Figures (7)

• Figure 1: OPM $M_\mathbf{call}$ (left), a string with chains shown by brackets (bottom), and its parsing steps using the OP algorithm (right).
• Figure 2: An example OP word, with the $\chi$ relation depicted by arrows, and PRs. First, a procedure is called (pos. 1), which installs an exception handler in pos. 2. Then, another function throws an exception, which is caught by the handler. Another function is called and returns and, finally, the initial one also returns.
• Figure 3: Scatter plots
• Figure 4: Survival plot
• Figure 5: Survival plot for the Quicksort category.

Theorems & Definitions (15)

• definition thmcounterdefinition
• definition thmcounterdefinition
• definition thmcounterdefinition
• definition thmcounterdefinition
• definition thmcounterdefinition: Fulfillment of a chain next operator
• definition thmcounterdefinition: Pending node
• definition thmcounterdefinition: Equivalent nodes
• theorem thmcountertheorem: Soundness
• proof : Sketch
• definition thmcounterdefinition: Next Normal Form