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.

翻译：算符优先语言（OPL）近期被证明是检验递归过程程序的有效形式化方法，这得益于其建模程序栈的能力。OPL需求可用面向优先级的时序逻辑（POTL）表达，该逻辑包含对函数调用与返回、异常处理及其他高级编程结构进行自然匹配推理的模态算子，而这些结构是先前方法（如可见下推语言）无法有效建模的。现有POTL模型检验方法均采用显式状态自动机方法，严重限制了其可扩展性。本文首次提出基于SMT的符号化方法用于POTL属性的模型检验：不同于传统方法需为POTL公式和程序模型分别构建自动机，我们将两者编码为（序列化的）SMT公式，并通过SMT求解器以有界模型检验方式搜索违反公式约束的模型执行轨迹。实验评估表明，该方法具有显著有效性。