Download Slides (pdf)

By Cláudio Belo Lourenço, HASLab/INESC TEC & University of Minho.

Abstract. Deductive verification tools typically rely on the conversion of code to a single-assignment (SA) form. In this paper we formalize program verification based on the translation of While programs annotated with loop invariants into a dynamic single-assignment language with a dedicated iterating construct, and the subsequent generation of compact, indeed linear-size, verification conditions. Soundness and completeness proofs are given for the entire workflow, including the translation of annotated programs to SA form. The formalization is based on a program logic that we show to be adaptation-complete. Although this important property has not, as far as we know, been established for any existing program verification tool, we believe that adaptation-completeness is one of the major motivations for the use of SA form as an intermediate language. Our results here show that indeed this allows for the tools to achieve the maximum degree of adaptation when handling subprograms.

Keywords. Software Engineering, deductive verification, single-assignment form, verification condition generation, Hoare logic, adaptation-completeness.

About the speaker. Cláudio is a third-year MAPi PhD student, affiliated with HASLab/INESC TEC & University of Minho, and working under supervision of Jorge Sousa Pinto. His area of interest and PhD thesis focuses on formal verification of programs. In particular, he has been working on the formalization of different approaches to generate efficiently-solved verification conditions. He has graduated in Computer Science from the University of Minho, in 2011, having attended one year at the University of Groningen, under the European Erasmus Program. In 2013, he completed his Master degree in Software Engineering at the University of Minho, where he studied mainly formal methods and distributed systems. His Master's thesis, "A bounded model checker for SPARK", focused on bounded verification of SPARK programs. In 2012 and 2013, he also participated, as a research fellow, in different projects supported by the Portuguese Foundation for Science and Technology. More recently he did an internship at the Japanese National Institute of Informatics under the supervision of Shin Nakajima where he explored and implemented different methods to generate verification conditions in the context of LLVM intermediate representation..

LOCATION AND TIME

Address:  University of Minho, Gualtar campus, Braga, Portugal.

Building. Departamento de Informatica, Building 07.

Coffee session: at 1:30PM-2PM, Sala de Estar, 4th floor.

Talks session: at 2PM-2:30PM, Auditório A2, 1st floor.