4 papers
SMT-based Symbolic Model-Checking for Operator Precedence Languages
Michele Chiari, Luca Geatti, Nicola Gigante +1
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…
Model Checking Probabilistic Operator Precedence Automata
Francesco Pontiggia, Ezio Bartocci, Michele Chiari
We address the problem of model checking context-free specifications for probabilistic pushdown automata, which has relevant applications in the verification of recursive probabili…
POTL: A First-Order Complete Temporal Logic for Operator Precedence Languages
Michele Chiari, Dino Mandrioli, Matteo Pradella
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…
Temporal Logic and Model Checking for Operator Precedence Languages
Michele Chiari, Dino Mandrioli, Matteo Pradella
In the last decades much research effort has been devoted to extending the success of model checking from the traditional field of finite state machines and various versions of tem…