In the next decade the software industry will have to face the responsibilities imposed by a computer-dependent society. Since software is increasingly deployed in safety critical applications, correctness and reliability are becoming issues of utmost importance. Consequently, software verification will be a grand challenge for both academic world and computer industry.

Software verification techniques fall into three main categories: (1) software testing, (2) formal verification methods such as model checking and theorem proving, and (3) methods based on static program analysis. The goal of this track is to study the individual contribution of each of these methodologies in verifying software artifacts, as well as promote discussion on novel combinations of these methodologies.

This track will focus on theoretical foundations, practical methods as well as case studies for verification of conventional and embedded software. We welcome papers that describe work on combinations of formal verification and program analysis techniques. Tool papers and case studies which report on advances in verifying large software systems are particularly sought.