28 citations · 54 across the 9 of their papers we have counts for
9 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, with applications in the verification of recursive probabilistic programs.…
Cyclic Operator Precedence Grammars for Parallel Parsing
Michele Chiari, Dino Mandrioli, Matteo Pradella
Operator precedence languages (OPL) enjoy the local parsability property, which essentially means that a code fragment enclosed within a pair of markers -- playing the role of pare…
Static Analysis of Infrastructure as Code: a Survey
Michele Chiari, Michele De Pascalis, Matteo Pradella
The increasing use of Infrastructure as Code (IaC) in DevOps leads to benefits in speed and reliability of deployment operation, but extends to infrastructure challenges typical of…
A First-Order Complete Temporal Logic for Structured Context-Free 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…
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…
Correct Approximation of IEEE 754 Floating-Point Arithmetic for Program Verification
Roberto Bagnara, Abramo Bagnara, Fabio Biselli +2
Verification of programs using floating-point arithmetic is challenging on several accounts. One of the difficulties of reasoning about such programs is due to the peculiarities 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…
A Practical Approach to Interval Refinement for math.h/cmath Functions
Roberto Bagnara, Michele Chiari, Roberta Gori +1
Verification of C++ programs has seen considerable progress in several areas, but not for programs that use these languages' mathematical libraries. The reason is that all librarie…