Counterexample extraction in a context-free model checker

POMC (Precedence Oriented Model Checker) is a software developed within Politecnico di Milano which allows the formal verification of certain properties expressed in POTL logic (Precedence Oriented Temporal Logic) on simple procedural programs. To model programs we use particular stack automatons called OPA (Operator Precedence Automaton) capable of recognizing words of a context-free class of languages called OPL (Operator Precedence Language). POMC checks that the required specifications are universally valid for each execution of the program to be tested. If positive, it returns a positive response, if not, it returns a counterexample: a word expressed in OPL corresponding to a program execution that refutes the requested property. The returned counterexample, due to POMC's implementation choices, may not be complete, may contain gaps. This thesis first explains how POMC uses OPL and POTL to model programs and properties, then how POMC works in practice, and finally presents the procedure for completing counterexamples together with evaluations and comparison between original POMC and POMC with counterexamples resolution.

POMC (Precedence Oriented Model Checker) è un software sviluppato all'interno del Politecnico di Milano che permette la verifica formale di determinate proprietà espresse nella logica POTL (Precedence Oriented Temporal Logic) su semplici programmi procedurali. Per modellizzare i programmi ci si serve di particolari automi a pila detti OPA (Operator Precedence Automaton) in grado di riconoscere parole di una classe di linguaggi libera dal contesto detta OPL (Operator Precedence Language). POMC controlla che le specifiche richieste siano universalmente valide per ogni esecuzione del programma da verificare. In caso positivo restituisce risposta positiva, in caso negativo restituisce un controesempio: una parola espressa in OPL corrispondente ad un'esecuzione del programma che confuta la proprietà richiesta. Il controesempio restituito, per via delle scelte d'implementazione di POMC, può non essere completo, contenere delle lacune. In questa tesi viene dapprima spiegato come POMC utilizza OPL e POTL per modellare programmi e proprietà, successivamente come funziona POMC nella pratica e infine viene presentata la procedura per completare i controesempi assieme alle valutazioni e al confronto tra POMC originale e POMC con risoluzione di controesempi.