SMT-based Symbolic Model-Checking for Operator Precedence Languages

TL;DR

This paper introduces a novel SMT-based symbolic model checking method for Operator Precedence Languages, enabling scalable verification of recursive programs with complex control flow using POTL logic.

Contribution

It presents the first SMT-based approach for model checking POTL properties, replacing automata-based methods with a more scalable SMT encoding.

Findings

Effective SMT-based verification demonstrated through experiments

Outperforms traditional automata-based approaches in scalability

Successfully models complex program constructs like exceptions and function calls

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.