Incremental reachability checking of KernelC programs using matching logic

Verification is an important activity in the software development process. Although testing can help in finding errors in programs, formal software verification techniques have proved to assure the development of applications that dependably satisfy their requirements. Nevertheless, these formal verification techniques are often characterized by high performance requirements, which negatively impact on the application of these techniques in the context of software that is continuously subjected to changes. In this scenario, the possibility to reuse - when verifying a new version of an already verified program - the intermediate results related to the unchanged parts in the original program, could save time and resources; incremental verification could contribute to the effectiveness of the application of formal verification techniques. In this work we explore the application of incremental verification in the context of reachability checking of KernelC programs using matching logic. KernelC is a subset of the C programming language that supports important features like the heap; matching logic consists of a language-independent proof system to reason about programs in any language that has a rewrite-based operational semantics. We achieve incrementality by using a syntactic-semantic approach: the reachability checking procedure is encoded as semantic attributes of a grammar in operator-precedence form; this specific class of grammars guarantee the support for incremental parsing and hence incremental evaluation of semantic attributes.

La verifica è una fase importante dello sviluppo del software. Sebbene il testing possa trovare diversi errori nei programmi, le tecniche di verifica formale possono ragionevolmente assicurare che le applicazioni sviluppate soddisferanno i requisiti. Tuttavia, queste tecniche sono spesso caratterizzate dalla richiesta di alte prestazioni, che ne impediscono l'applicazione su software continuamente soggetto a cambiamenti. In questo scenario, la possibilità di riutilizzare, nella verifica di una nuova versione di un programma già verificato, i risultati intermedi della parti immutate del programma originario, possono risparmiare tempo e risorse; la verifica incrementale può contribuire all'efficacia di tali tecniche formali. In questo lavoro tratteremo l'applicazione di verifica incrementale nel contesto del controllo di raggiungibilità operato su programmi in linguaggio KernelC attraverso matching logic. KernelC è un sottoinsieme del linguaggio C che supporta importanti caratteristiche come la gestione della memoria; matching logic è un sistema di dimostrazione indipendente dal linguaggio che può trattare programmi scritti in qualunque linguaggio che abbia una semantica operazionale basata su riscritture. L'approccio utilizzato per ottenere l'incrementalità è di tipo sintattico-semantico: la verifica di raggiungibilità è espressa attraverso attributi semantici di una grammatica in forma a precedenza di operatori; questa particolare classe di grammatiche può operare in maniera incrementale e quindi consente una valutazione incrementale degli attributi semantici.