Model checking through inductive partitioning of the state space

The field of Formal Verification has always strode to provide theoretically sound methods that can ascertain the correctness of mission critical programs and, given the computational complexity of this task, performance has been one of the most important issues during the development of verification tools. This thesis is aimed at integrating a novel transition system verification technique, called IC3, to the TRIO verification software of Politecnico di Milano, Zot. IC3 has been published in 2011 and has since been implemented and used in many verification tools, yielding promising results and outperforming, sometimes by far, its competitors. With IC3Zot a new Zot module is proposed, allowing the verification of TRIO formulae by using an incremental approach. These formulae undergo a series of translations to be then processed by an IC3-based core, producing either satisfiable traces or inductive proofs of language emptiness. In order to ascertain performance and correctness, this module has been benchmarked against similar tools, highlighting the use cases in which traditional BMC workflows are not as effective or are less efficient. This document first explores the literature available on IC3 and its derivatives, together with an overview of the current techniques that are used to perform model checking, providing a setting for this thesis. The algorithms that have been implemented are then discussed in detail, together with explanations on the main design choices and the structure of the Lisp Module. Finally the experimental results are reported and discussed, and conclusions are drawn. IC3Zot has shown potential, managing to compete with, and sometimes outperform substantially, the other more mature and developed modules of Zot. The module itself has been designed to be open to extension, both to richer logics and to performance improvements, and possible future developments are discussed in the final section.

Il campo della Verifica Formale ha sempre cercato di fornire metodi teoricamente solidi per verificare la correttezza di programmi critici e, a causa della difficoltà computazionale di queste tecniche, l'efficienza è sempre stata una degli aspetti fondamentali durante lo sviluppo di strumenti di verifica. Lo scopo di questa tesi è quello di integrare una tecnica innovativa per la verifica di sistemi di transizione, chiamata IC3, con il software di verifica di formule TRIO del Politecnico di Milano, Zot. IC3 è stato pubblicato nel 2011 e da allora è stato implementato in molti strumenti di verifica, dando ottimi risultati e sorpassando i propri competitor in numerosi test. Con IC3Zot si propone un nuovo modulo di Zot, permettendo di effettuare la verifica di formule TRIO usando un approccio incrementale. Queste formule vengono prima trasformate per poi essere processate da un componente basato su IC3, producendo alternativamente tracce soddisfacibili o prove induttive di insoddisfacibilità. Allo scopo di controllarne performance e correttezza, questo modulo è testato e paragonato ad altri strumenti simili, evidenziando in quali casi esso sia in grado di superare i tradizionali workflow BMC. Questo documento inizialmente esplora la letteratura in materia di IC3 e i suoi derivati, fornendo una panoramica delle alternative presenti per fare model checking e descrivendo il background della tesi. Successivamente vengono discussi in dettaglio gli algoritmi che sono stati implementati, spiegando le scelte implementative e quelle di design. Vengono infine riportati e discussi i risultati sperimentali, traendone le conclusioni. IC3Zot si è dimostrato promettente e in grado di competere con, e in alcuni casi sorpassare di molto, gli altri moduli di Zot, che sono molto più maturi. Questo modulo è stato progettato per essere aperto ad estensioni, sia da un punto di vista di performance che di espressività, e possibili migliorie e sviluppi sono discussi nella sezione finale.