A Generalized Program Verification Workflow Based on Loop Elimination and SA Form - Laboratoire de Recherche en Informatique. Équipe: Vérification d'Algorithmes, Langages et Systèmes Accéder directement au contenu
Communication Dans Un Congrès Année : 2019

A Generalized Program Verification Workflow Based on Loop Elimination and SA Form

Résumé

This paper presents a minimal model of the functioning of program verification and property checking tools based on (i) the encoding of loops as non-iterating programs, either conservatively, making use of invariants and assume/assert commands, or in a bounded way; and (ii) the use of an intermediate single-assignment (SA) form. The model captures the basic workflow of tools like Boogie, Why3, or CBMC, building on a clear distinction between operational and axiomatic semantics. This allows us to consider separately the soundness of program annotation, loop encoding, translation into SA form, and verification condition (VC) generation, as well as appropriate notions of completeness for each of these processes. To the best of our knowledge, this is the first formalization of a bounded model checking of software technique, including soundness and completeness proofs using Hoare logic; we also give the first completeness proof of a deductive verification technique based on a conservative encoding of invariant-annotated loops with assume/assert in SA form, as well as the first soundness proof based on a program logic.
Fichier principal
Vignette du fichier
main.pdf (383.14 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02431769 , version 1 (08-01-2020)

Identifiants

  • HAL Id : hal-02431769 , version 1

Citer

Cláudio Belo Lourenço, Maria João Frade, Jorge Sousa Pinto. A Generalized Program Verification Workflow Based on Loop Elimination and SA Form. FormaliSE 2019 - 7th International Conference on Formal Methods in Software Engineering, May 2019, Montreal, Canada. ⟨hal-02431769⟩
117 Consultations
198 Téléchargements

Partager

Gmail Facebook X LinkedIn More