Motivation

While Formal Methods (FM) and Formal Verification (FV) have had an impact in specific areas, notably in hardware (HW) and protocol verification, they are far from realizing their promise and potential in practice, especially in software (SW) and embedded systems. But the need for techniques that can ensure correctness of systems with high degree of assurance/coverage is never greater, with the pervasiveness of embedded systems in practice, and the content of SW and HW in embedded systems ever growing. The main bottlenecks blocking wider application of FM/FV techniques are their lack of scalability and the lack of enough successful models using these techniques in a way that can be replicated.

The aim of this workshop is to bring together a group of experts from both industry and academia to share their experiences and exchange new ideas and solutions to this problem. The presentations and discussions at the workshop include (but are not limited to) the following topics.

  • State-of-art FV tools and techniques in use in industry
  • Technical challenges and bottlenecks for scalability and useability
  • New areas of applications and related correctness issues
  • New techniques and solutions for scaling FM/FV