A correctness/incorrectness program logic on Kleene Algebra

A fundamental problem in software development consists in the reduction or somehow limitation of the presence of bugs. To address this problem, various strategies have been proposed: on one side we have dynamic analysis (e.g., fuzzing or testing) that allows to verify the presence of bugs at runtime, on the other hand we have static analysis which analyzes the software without executing it. The latter is typically based on formal methods, i.e., mathematical proofs of some specification of absence of bugs. An import step in this sense was the introduction of Hoare's logic, a program logic that allows to reason about the validity of some predicates concerning the semantic of some program. In particular, the predicates proved by this logic represent over-approximations of the concrete program semantics. Recently, Peter W. O'Hearn introduced a program logic which computes in the opposite way, i.e, it proves predicates that under-approximate the concrete semantics of a program. The former can be used to prove the correctness of a program with respect to its specification, the latter instead allows to prove the incorrectness of a program, i.e., the violation of its specification. Later, it was shown that the technique of abstract interpretation (in particular the concept of local completeness) can be used to merge those two logics in a single logic with analyzes both correctness and incorrectness at the same time. Traditionally, program logics were described using a set-theoretic formulation, meaning that predicates are represented as set of states satisfying themselves. A different approach is the one of Kleene Algebra with tests (KAT): in this alternative formulation programs and predicates are elements of an algebra and they can be composed by the means of algebra's operators. It was shown that Hoare's and O'Hearn's logic can be transposed using this formulation and the same results hold. This thesis studies a KAT formulation of the correctness/incorrectness logic. In particular it shows that the main results (namely: logical soundness and correctness) still hold also in this KAT version.

Un problema fondamentale nello sviluppo del software consiste nel minimizzare la presenza, o quanto meno a rendere più difficile l'introduzione, di bug. Per affrontare questo problema si sono elaborate diverse strategie: da un lato vi sono le tecniche di analisi dinamica (ad esempio fuzzing o testing) che permettono di verificare la presenza di bug a runtime, dall'altro vi è l'analisi statica che si occupa invece di analizzare il software senza che questo venga eseguito. Questo avviene solitamente mediante metodi formali, cioè atti a dimostrare matematicamente che certe specifiche di assenza di bug siano soddisfatte. Un'importante impulso in questo senso è stato dato dall'introduzione della logica di Hoare, una particolare logica che permette di ragionare sulla veridicità di predicati che riguardano la semantica di un programma. In particolare, i predicati dedotti mediante questa logica rappresentano sovrapprosimazioni della semantica del programma. Recentemente, è stata introdotta da Peter W. O'Hearn una logica che ragiona nel modo opposto, cioè che deduce predicati che sottoapprossimano la semantica del programma. Mentre la prima può essere usata per dedurre la correttezza di un programma rispetto alle sue specifiche, la seconda permette invece di stabilire l'incorrettezza di un programma, cioè che le sue specifiche vengono violate. Successivamente, è stato dimostrato che, utilizzando la tecnica dell'interpretazione astratta (e in particolare il concetto di completezza locale), questi due approcci possono essere unificati in un'unica logica che analizza sia correttezza che incorrettezza di un programma. Tradizionalmente, queste logiche vengono formulate in modo insiemistico, rappresentando cioè i predicati mediante insiemi di stati che soddisfano appunto il predicato stesso. Un approccio alternativo è quello proposto dalle algebre di Kleene con i test (KAT): in questa formulazione programmi e predicati sono elementi di un'algebra e possono essere composti utilizzando gli operatori dell'algebra stessa. È stato osservato che le logiche di Hoare e di O'Hearn possono essere trasposte in questa seconda formulazione ottenendo gli stessi risultati. In questa tesi si è studiata una formulazione alternativa della logica della correttezza/incorrettezza mediante KAT e si è osservato che anche in questa veste i risultati (in particolare correttezza e completezza logica) possono essere dimostrati.