Advancing Automated, Permission-Based Program Verification Using Symbolic Execution

Examiners:
Prof. Peter Müller, ETH Zurich (examiner)
Prof. Bart Jacobs, KU Leuven (co-examiner)
Prof. Viktor Kuncak, EPFL Lausanne (co-examiner)
Prof. Martin Vechev, ETH Zurich (co-examiner)
Downloads:
Thesis [PDF]
Defence talk slides [PPTX][PDF]

Abstract

Proving the correctness of programs by rigorously applying formal methods such as deductive verification has attracted substantial interest in the last two decades, from both the scientific community and industry. This has led to numerous important theoretical results and successful practical applications, benefiting greatly from two parallel developments: (1) the introduction and exploration of permission logics such as separation logic, which are particularly suitable for modularly reasoning about concurrent, heap-manipulating programs, and (2) the emergence of a de-facto standard architecture for reusable verification infrastructures, which significantly reduces the effort involved with developing automated verification tools. The existence of automated verification tools is a prerequisite for scaling verification to the size and complexity of real-world software, but it also makes verification more easily accessible and applicable in general: as a result, researchers are provided with valuable feedback, enabling them to identify remaining challenges. Existing verification infrastructures, however, are not well-suited for permission-based verification, which impedes the further development of the field. In particular, central aspects such as program heaps and permissions must be encoded, which substantially complicates the development of efficient and precise verification tools.

This thesis aims to remedy the situation by developing a verification infrastructure that facilitates the development of automated, permission-based verification tools for race-free, concurrent and heap-manipulating programs. To achieve this goal, we make the following three contributions: first, we design Viper, a novel intermediate verification language, carefully balanced to be sufficiently expressive to enable the encoding of different programming languages, program properties and specification languages, while also facilitating the development of efficient and precise verification tools. Second, we develop Silicon, an automated, symbolic-execution-based verifier for the Viper language that exhibits stable and good performance, and is more complete than comparable verifiers. Third, we extend Viper and Silicon with support for two challenging features of permission logics — iterated separating conjunctions and magic wands — that have shown to be useful in by-hand proofs of various properties, but for which no existing verifier provides comparably direct and automated support.

The Viper verification infrastructure, which includes the Viper language and the automated verifier Silicon, already had an impact on the field of automated, permission-based verification: it is actively being used at three different universities for building several verification tools, it won an award at a verification competition and it was used for teaching at a summer school.

Relevant Projects

ViperLogo The Viper verification infrastructure includes the Viper intermediate verification language and back-ends that process programs encoded in Viper, e.g. automated verifiers. The Viper language is one of the major contributions of my PhD thesis. An overview of the language can be found in my PhD thesis, or in parts in this VMCAI'16 paper. The source code of the Viper language is hosted on Bitbucket.
SiliconLogo Silicon is a state-of-the-art, symbolic-execution-based program verifier and another major contribution of my PhD thesis. It is the default back-end verifier for the Viper language; as such, it was used during the VerifyThis@ETAPS 2016 verification competition, were our team won the "Distinguished User-Assistance Tool Feature" award, and it was used at the Marktoberdorf Summer School 2016 in student exercises. Silicon is described in my PhD thesis, and it's source code is hosted on Bitbucket.
“If I had asked people what they wanted, they would have said faster horses.” — Henry Ford