Home

Despite a lot of fruitful research on formal verification techniques in the last 40 years, formal verification has not become a mainstream tool in current development practice. Numerous case-studies and success stories about using verification to increase the reliability of software systems show that it has huge potential. However, a broad adoption of formal verification techniques is not in sight.

The inherent complexity of the systems being built, as well as the complexity of the analyses pose scalability challenges in real industrial projects. Other important reasons for their low adoption are related to pragmatic aspects such as usability or the cost of applying formal verification (e.g. specifying properties, running the analyses, interpreting the results). For a large majority of software engineers and developers, formal verification techniques are seen rather as expert tools and not as engineering tools that can be used on a daily basis. This is mostly the case in the context of main stream systems (e.g. automotive, medical, industrial automation) where pragmatics (e.g. personnel skills, cost structures, deadlines, existent processes, existent organization, legacy code) plays a major role.

Objectives:

This workshop aims to create a cohesive community interested in the application of formal verification techniques to increase reliability of software intensive systems, but in which pragmatic constraints such as usability or costs play a central role. We aim at bringing together researchers and practitioners to lower the adoption barrier of formal verification. We especially focus on the needs of main stream developers that do not (necessarily) work on highly safety critical systems but on more main stream systems that still need to be reliable. 

The workshop is co-located with the 27th International Symposium on Software Reliability Engineering in Ottawa, Canada.

Organizers:
  • Daniel Ratiu, Siemens, Germany
  • Bernhard Schätz, fortiss, Germany
  • Alan Wassyng, McMaster University, Canada