A Generalized Program Verification Workflow Based on Loop Elimination and SA Form
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 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.
Mon 27 MayDisplayed time zone: Eastern Time (US & Canada) change
14:00 - 15:30
Session 3FormaliSE at Foyer
Chair(s): Eunsuk Kang Carnegie Mellon University
|Parallelizable Reachability Analysis Algorithms for Feed-Forward Neural Networks|
Hoang-Dung Tran Vanderbilt University, Patrick Musau Vanderbilt University, Diego Manzanas Lopez Vanderbilt University, Xiao Dong Yang Vanderbilt University, Luan Nguyen University of Pennsylvania, Weiming Xiang Vanderbilt University, Taylor T Johnson Vanderbilt University
|Towards Sampling and Simulation-Based Analysis of Featured Weighted Automata|
Maxime Cordy SnT, University of Luxembourg, Axel Legay , Sami Lazreg Visteon Electronics and Universite Cote d Azur, Philippe Collet University of Nice
|Verifying Channel Communication Correctness for a Multi-Core Cooperatively Scheduled Runtime Using CSP|
Jan Pedersen University of Nevada Las Vegas, Kevin Chalmers Edinburgh Napier University
|A Generalized Program Verification Workflow Based on Loop Elimination and SA Form|
Cláudio Belo Lourenço LRI, Université Paris-Sud & INRIA Saclay, Maria João Frade HASLab/INESC TEC & Universidade do Minho, Portugal, Jorge Sousa Pinto HASLab/INESC TEC & Universidade do Minho, Portugal