一句话：提出并实现了首个开源模型检测器 POMC，用于验证运算符优先级语言程序上的 POTL 树结构性质。
将模型检测从有限状态机扩展到过程式程序，需要对上下文无关结构进行时序推理。已有 CaRet、NWTL 等嵌套词逻辑；新提出的 POTL 面向运算符优先级语言（OPL），在表达能力上强于 NWTL，并对与 OPL 等价的 MSO 逻辑的 FO 片段完备。本文实现了名为 POMC 的模型检测器，用于验证以 OPL 编码的程序是否满足 POTL 性质。作者称 POMC 是首个已实现并公开可用的、用于证明递归过程式程序树结构性质的模型检测器，并在一个非平凡基准上进行了实验评估。
The problem of extending model checking from finite state machines to procedural programs has fostered much research toward the definition of temporal logics for reasoning on context-free structures. The most notable of such results are temporal logics on Nested Words, such as CaRet and NWTL. Recently, Precedence Oriented Temporal Logic (POTL) has been introduced to specify and prove properties of programs coded trough an Operator Precedence Language (OPL). POTL is complete w.r.t. the FO restriction of the MSO logic previously defined as a logic fully equivalent to OPL. POTL increases NWTL’s expressive power in a perfectly parallel way as OPLs are more powerful that nested words. In this article, we produce a model checker, named POMC, for OPL programs to prove properties expressed in POTL. To the best of our knowledge, POMC is the first implemented and openly available model checker for proving tree-structured properties of recursive procedural programs. We also report on the experimental evaluation we performed on POMC on a nontrivial benchmark.
@article{paperbot2125,
title = {A Model Checker for Operator Precedence Languages},
author = {Michele Chiari and Dino Mandrioli and Francesco Pontiggia and Matteo Pradella},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {45},
number = {3},
year = {2023},
doi = {10.1145/3608443}
}