Single-assignment program verification

Abstract

No contexto da verificação de programas, são várias as ferramentas que assentam na tradução de programas numa forma single-assignment (umas implicitamente e outras explicitamente), e depois num algoritmo que gera condições de verificação. Nesta tese, revisitamos dois grandes métodos tipicamente utilizados para a geração de condições de verificação a partir de programas single-assignment: predicate transformers (utilizados maioritariamente por ferramentas dedutivas) e a transformação baseada em conditional normal form (utilizados em bounded model checking de software). Com isto, identificamos vários aspetos nos quais estes métodos diferem e mostramos como estes podem ser combinados para produzir novos geradores de condições de verificação. Os métodos resultantes, juntamente com os iniciais, formam aquilo que designamos por VCGen cube e que propomos como uma framework para sintetizar e comparar a geração de condições de verificação. A nível teórico, propomos duas abordagens para a verificação baseada na tradução de programas em single-assignment e subsequente geração de condições de verificação. Por um lado, formalizamos uma técnica assente na tradução de programas While, anotados com invariantes de ciclo, em programas single-assignment contendo um comando especial para captar os respetivos ciclos e invariantes. Provas sobre a soundness e completeness do fluxo completo da técnica são apresentadas. A formalização da técnica é baseada numa lógica de programas que é adaptation-complete. Numa segunda abordagem, definimos formalmente a noção de programa single-assignment (sem ciclos) contendo os comandos assume e assert, e também exceções, e introduzimos uma lógica para estes programas que nos permite mostrar que o VCGen cube é sound e complete. Uma técnica de verificação que assenta na tradução de programas em single-assignment é então proposta e mais uma vez, o fluxo completo da framework é provado como sendo sound e complete. Em particular, a tradução concreta (esta também provada correta) traduz programas contendo ciclos em programas sem ciclos. Para a avaliação empírica dos geradores de condições de verificação, recorremos a duas abordagens, uma no contexto da linguagem intermédia LLVM, e outra no contexto da ferramenta de verificação dedutiva Why3. Embora os resultados não indiquem superioridade absoluta de nenhum método, estes revelam tendências interessantes.

Many program veri cation tools rely on the translation of code annotated with properties into an intermediate single-assignment form (in a more or less explicit way), and then on an algorithm that generates veri cation conditions from it. In this thesis, we revisit two major methods that are widely used to produce veri cation conditions for single-assignment programs: predicate transformers (used mostly by deductive veri cation tools) and the conditional normal form transformation (used in bounded model checking of software). We identify different aspects in which the methods differ and show that they can be combined to produce new hybrid veri cation condition generators; together with the initial algorithms they form what we call the VCGen cube, which we propose as a framework for synthesizing and comparing veri cation condition generators. Optimizations implemented by veri cation tools are then integrated into the cube. At the theoretical level we propose two fully proved veri cation frameworks based on the translation into single-assignment and subsequent generation of veri cation conditions. On one hand we formalize program veri cation based on the translation of While programs annotated with loop invariants into an iterating single-assignment language with a dedicated iterating construct. Soundness and completeness proofs are given for the entire workflow, including the translation of annotated programs into iterating single-assignment form. The formalization is based on a program logic that we show to be adaptation-complete. On the other hand we formally de fine an iteration-free single-assignment language with assume, assert, and exceptions, and introduce a program logic for this language which allows us to prove the soundness and completeness of the VCGen cube. A veri cation framework based on the translation of programs into (iteration-free) single-assignment form is then proposed, and the entire workflow is proved to be sound and complete. We also suggest a concrete singleassignment translation that transforms annotated loops into assumes and asserts to check that the annotated invariants are valid and preserved during the iterations. Finally, we compare the veri cation condition generators empirically, both for programs of the LLVM intermediate representation (a concrete popular intermediate language that is based on SA form), and in the context of the Why3 deductive veri cation tool. Although the results do not indicate absolute superiority of any given method, they do allow us to identify interesting trends.