Blogs (1) >>
ICSE 2019
Sat 25 - Fri 31 May 2019 Montreal, QC, Canada
Mon 27 May 2019 15:05 - 15:30 at Foyer - Session 3 Chair(s): Eunsuk Kang

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 May

Formalise-2019-papers
14:00 - 15:30: FormaliSE 2019 - Session 3 at Foyer
Chair(s): Eunsuk KangCarnegie Mellon University
Formalise-2019-papers14:00 - 14:25
Full-paper
Hoang-Dung TranVanderbilt University, Patrick MusauVanderbilt University, Diego Manzanas LopezVanderbilt University, Xiao Dong YangVanderbilt University, Luan NguyenUniversity of Pennsylvania, Weiming XiangVanderbilt University, Taylor T JohnsonVanderbilt University
Formalise-2019-papers14:25 - 14:40
Short-paper
Maxime CordySnT, University of Luxembourg, Axel Legay, Sami LazregVisteon Electronics and Universite Cote d Azur, Philippe ColletUniversity of Nice
Formalise-2019-papers14:40 - 15:05
Full-paper
Jan PedersenUniversity of Nevada Las Vegas, Kevin ChalmersEdinburgh Napier University
Formalise-2019-papers15:05 - 15:30
Full-paper
Cláudio Belo LourençoLRI, Université Paris-Sud & INRIA Saclay, Maria João FradeHASLab/INESC TEC & Universidade do Minho, Portugal, Jorge Sousa PintoHASLab/INESC TEC & Universidade do Minho, Portugal