A syntactic-semantic approach for incremental program verification of matching logic properties

Software is not built monolithically; instead, its construction requires a sequence of small steps. In fact, software is continuously subjected to changes; either in the specification and requirements, due to changes in the environment or in user needs; either in the implementation, in order to fix a software fault or to implement a missing functionality. In both cases, change is a distinctive feature of software systems, affecting almost every phase of its life-cycle. On the other hand, formal software verification techniques are becoming more and more effective in helping the developer of software systems. However, formal verification technology is still not widely adopted for ensuring software correctness. One of the main reason for this is the high demand of computation resource which affects every formal verification techniques due to the high computational complexity of the problems involved. In our opinion, it is possible to exploits the incremental nature of software systems to develop more efficient verification techniques. Many of the existing formal verification approaches do not exploit the fact of having a sequence of different software versions which change relatively little one to another; instead they reapply the verification process from scratch to each version. We address this problem by developing formal verification techniques capable of incrementality: techniques which are able to reuse the intermediate results obtained with the verification of an early version of a software system to the verification of the new versions. Our goal is to provide formal verification as a feasible and practical way of assessing quality in software products. Nowadays, the most applied verification technique is testing which has gained popularity with the introduction of Agile methodologies. It is applied to evolving software systems in the form of continuous testing: software quality is assessed by automatically applying a set of tests to each version of a product. Our ultimate goal is to provide an incremental formal verification approach which can complement testing, as a practical and reliable verification technique still providing strong formal guarantees of correctness. We target incremental verification techniques based on the syntactical structure of the software artifact being verified. The formal language which defines the software artifact can discover the changes occurred at a syntactical level: Software artifacts are expressed by operator-precedence grammars, which, thanks to properties such as locality, provide ways to efficiently reparse only the parts affected by the change. This incrementality obtained at the syntactic level is then translated to semantics by means of the attribute grammar formalism. In particular, by using synthesized-only attribute grammars, the semantic effect of a change is limited to a portion of the abstract syntax tree defined by the program. This idea has been developed in the SiDECAR framework, a system for defining a incremental verification techniques on a given programming language. In this work, this general technique is applied to matching logic properties verification. Matching logic is a Hoare-like verification system rooted on a formal definition of programming language semantics. We have analyzed the case of KernelC language. KernelC is a subset of the C language having interesting features as heap, loops, function calls and recursion. In this work, we have developed a matching logic verification framework expressed as an evaluation of semantic attributes. Upon this approach we have built our incremental verification technique. This approach has been implemented using the framework SiDECAR, for the incremental matching logic verification of KernelC programs. We experimentally evaluated our incremental verification approach over a large suite of programs, containing many versions of each program; along with the state-of-the-art, non-incremental tool MATCHC for the verification of KernelC programs annotated with matching logic properties. In particular we first evaluate the non-incremental performance of our tool, comparing it with MATCHC over the examples MATCHC is provided with. Then, we evaluate the approach with incrementality over programs either constructed applying random mutation to MATCHC examples, or considering well known benchmarks, such as the Siemens test suite and classic literature data structures, as red-black trees. The obtained results show that our incremental approach can effectively speedup software verification process, in the case of matching logic verification of KernelC programs.

Il processo di sviluppo software non è monolitico, ma si compone di una sequenza di passaggi intermedi. In pratica, il software è continuamente sottoposto a modifiche; sia relativamente a specifiche e requisiti, a causa di cambiamenti nell'ambiente circostante o nei bisogni dell'utente; sia nell'implementazione, per la correzione di errori esistenti o per l'aggiunta di nuove funzionalità. In entrambi i casi, il cambiamento è una caratteristica peculiare del software, presente in quasi ogni fase del ciclo di sviluppo. D'altro canto, le tecniche di verifica formale diventano man mano più efficaci nell'aiutare lo sviluppatore software. Tuttavia a questo miglioramento tecnologico non corrisponde un eguale diffusione dell'uso di tali tecniche nel controllo della correttezza del software. Un motivo di ciò è da ricercare nell'elevata richiesta di risorse computazionali delle tecniche di verifica formali, dovute alle complessità computazionali presenti. Riteniamo che la natura essenzialmente incrementale del software possa essere sfruttata per sviluppare tecniche di verifica più efficienti. Molti approcci di verifica formale esistenti, infatti, non sfruttano il fatto di essere applicati ad una sequenza di versioni del software, che differiscono poco tra loro; verificando da zero ogni nuova versione. Una soluzione efficiente è data da tecniche di verifica formale incrementali: approcci che sono capaci di riutilizzare i risultati delle computazioni intermedie ottenute durante la verifica di una versione precedente del software, per velocizzare la verifica delle versioni successive. L'obiettivo è di rendere la verifica formale un modo usabile e pratico per garantire la qualità dei prodotti software. Ad oggi, la tecnica di verifica più utilizzata è il testing, che si è largamente diffusa con l'avvento delle tecniche di sviluppo Agile. L'applicazione a sistemi software in continua evoluzione ha prodotto il testing continuo: ad ogni nuova versione del prodotto sofware vengono applicate automaticamente un insieme di casi di test. Il fine ultimo è quindi quello di ottenere un approccio di verifica formale incrementale, che possa complementare il testing, risultando allo stesso modo conveniente e pratico da usare, fornendo però, nel contempo, solide garanzie sulla correttezza del software verificato. Le tecniche analizzate si basano sulla struttura sintattica del prodotto software verificato. Il linguaggio formale utilizzato per definire il sofware viene sfruttato per identificare i cambiamenti ad un livello sintattico: il software viene descritto da grammatiche a precedenza di operatori, che grazie e proprietà quali la località, permettono di effettuare il parsing solo delle parti toccate dal cambiamento. L'incrementalità ottenuta a livello sintattico viene poi riportata a livello semantico attraverso l'uso di grammatiche ad attributi: utilizzando grammatiche composte da soli attributi sintetizzati, l'effetto semantico delle modifiche apportate è ristretto a una parte dell'albero sintattico. Quest'intuizione è stata sviluppata nel framework SiDECAR, che consente di definire una tecnica di verifica incrementale su un dato linguaggio di programmazione. In questo lavoro, tale tecnica generale viene applicata al caso della verifica di proprietà specificate in matching logic. La matching logic è un sistema di verifica alla Hoare fondato sulla semantica formale del linguaggio. In particolare abbiamo analizzato il caso del linguaggio KernelC, un sottoinsieme del C che mantiene caratteristiche interessanti quali la gestione della memoria, i cicli, le chiamate a funzione e la ricorsione. Abbiamo sviluppato un framework per la verifica della matching logic condotta attraverso la valutazione di attributi semantici. Su questo approccio abbiamo sviluppato la nostra tecnica di verifica incrementale. Abbiamo poi implementato questo approccio all'interno del framework SiDECAR, consentendo la verifica incrementale di programmi KernelC specificati tramite matching logic. Abbiamo condotto una valutazione sperimentale sul nostro approccio di verifica incrementale utilizzato un grande insieme di programmi, contenenti diverse versioni ciascuno; abbiamo poi confrontato il nostro approccio col tool MATCHC, che definisce lo stato dell'arte nella verifica matching logic non incrementale di programmi KernelC. Più precisamente, abbiamo prima confrontato il nostro tool con MATCHC sugli esempi forniti da MATCHC. Abbiamo poi valutato l'approccio incrementale su programmi o ottenuti tramite mutazioni casuali sugli esempi MATCHC, o tratti da benchmark noti, come la suite di test Siemens, o da strutture classiche note in letteratura, come gli alberi rosso-neri. I risultati ottenuti mostrano che il nostro approccio incrementale è effettivamente più efficiente, nella verifica di proprietà matching logic su programmi KernelC, rispetto alla verifica non-incrementale.