Views provided by UsageCounts
This is the artifact related to the article M. Chiari, D. Mandrioli, M. Pradella: "Model-Checking Structured Context-Free Languages" accepted at CAV 2021. Abstract: The problem of model checking procedural programs has fostered much research towards 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, the logic OPTL was introduced, based on the class of Operator Precedence Languages (OPL), more powerful than Nested Words. We define the new OPL-based logic POTL, and provide a model checking procedure for it. POTL improves on NWTL by enabling the formulation of requirements involving pre/post-conditions, stack inspection, and others in the presence of exception-like constructs. It improves on OPTL by being FO-complete, and by expressing more easily stack inspection and function-local properties. We developed a model checking tool for POTL, which we experimentally evaluate on some interesting use-cases. This artifact contains POMC, an explicit-state model checking tool for POTL written in Haskell, and the input files needed to run all experiments in the main paper (and more). This artifact contains POMC v1.0.1, a model checker for Precedence-Oriented Temporal Logic (POTL). POMC is an explicit-state model checker: given a POTL formula, it builds an automaton equivalent to it, and checks the emptiness of its intersection with the input model. POMC accepts two kinds of input: - A POTL formula + an Operator Precedence Automaton (OPA) to be checked (OPA are the class of pushdown automata that characterize Operator Precedence Languages) - A POTL formula + a MiniProc program to be checked. MiniProc is a simple user-friendly input language for modeling procedural programs with exceptions.
temporal logic, software verification, model checking
temporal logic, software verification, model checking
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 1 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
| views | 10 |

Views provided by UsageCounts