VerCors supports deductive verification of concurrent software, written in multiple programming languages, where the specifications are written in terms of pre-/postcondition contracts using permission-based separation logic. Work on the VerCors verifier has started more than a decade ago. In this decade, the focus of the work on VerCors has shifted from verification of (concurrent) Java programs only to the development of a verifier that can support different programming languages, by exploiting their commonalities for developing efficient verification support.

In this talk, I will first give an overview of the VerCors verifier:

• how it is set up as a program transformation tool that translates an annotated program into input for the Viper framework, which is then used as verification back-end
• how it supports different programming languages and features, and
• how it has been used on different case studies (and how this has further improved VerCors).

In the last part of my talk, I will sketch my ideas and plans to further increase the inclusiveness of VerCors, so that it becomes easier to support new programming languages and to reuse the existing verification infrastructure in new settings.